Logiweb(TM)

8.5.9 Unary instantiation

Prev Up Next Page 334 of 800 Search internet


Unary instantiation A At allows to instantiate a meta-variable without telling how. Thus, the operator requests adaption of A 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:

Prop lemma M1.8g : #x imply #x end lemma

prepare proof indentation,proof of M1.8g : line L01 : Premise >> Prop ; line L04 : MP ponens A2 At At At ponens A1 At At >> ( #x imply #y imply #x ) imply #x imply #x ; line L05 : A1 >> #x imply #y imply #x ; line L06 : MP ponens L04 ponens L05 >> #x imply #x qed

The axioms say:

axiom A1 : All #x ,, #y : #x imply #y imply #x end axiom

axiom A2 : All #x ,, #y ,, #z : ( #x imply #y imply #z ) imply ( #x imply #y ) imply #x imply #z end axiom

Since adaption is not applied to the second argument of ponens operator, we must instantiate A1 explicitly twice to get rid of two meta-quantifiers and A2 trice to get rid of three meta-quantifiers.

One may go further and have second arguments with structure:

Prop lemma M1.8h : #x imply #x end lemma

prepare proof indentation,proof of M1.8h : line L01 : Premise >> Prop ; line L05 : A1 >> #x imply #y imply #x ; line L06 : MP ponens ( MP ponens A2 At At At ponens A1 At At ) ponens L05 >> #x imply #x qed

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 A1 At At we get an Incomplete unification. Uninstantiated variable: y error message. However, we can still do this:

Prop lemma M1.8i : #x imply #x end lemma

prepare proof indentation,proof of M1.8i : line L01 : Premise >> Prop ; line L06 : MP ponens ( MP ponens A2 At At At ponens A1 At At ) ponens ( A1 At at #y ) >> #x imply #x qed

A1 At at #y instantiates #x without telling how and instantiates #y to #y. 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 A2 Conclude in place of A2 At At At.

Prev Up Next Page 334 of 800 Search logiweb.eu

Copyright © 2010 Klaus Grue, GRD-2010-01-05