|Page 334 of 800||Search internet|
Unary instantiation allows to instantiate a meta-variable without telling how. Thus, the operator requests adaption of such that its principal operator is a meta-quantifier and forces instantiation of that meta-quantifier but leaves it to unification to find out how the operator should be instantiated.
In the proofs of M1.8 stated previously, all second arguments of ponens operators are line numbers. That enhances readability for human readers, but the proof checker allows arbitrarily complex arguments of the ponens operator. Here is an example where axioms are used as second arguments:
The axioms say:
Since adaption is not applied to the second argument of ponens operator, we must instantiate explicitly twice to get rid of two meta-quantifiers and trice to get rid of three meta-quantifiers.
One may go further and have second arguments with structure:
That is terse and unreadable. At least human readers will need to slow down their pace of reading if they want to understand a proof like the one above. The proof checker, however, does not care.
If we go further and replace Line L05 by we get an Incomplete unification. Uninstantiated variable: y error message. However, we can still do this:
instantiates without telling how and instantiates to . That way the unification tactic has enough information to produce a sequent proof.
The result is an even more unreadable proof, but the point is that unary instantiation can be used for gaining tight control over the unification tactic.
As noted later, one can write in place of .
|Page 334 of 800||Search logiweb.eu|