Logiweb(TM)

8.5.3 Axioms

Prev Up Next Page 328 of 800 Search internet


One of the things an argumentation can contain is a reference to an axiom. As an example, Line L03 below uses Axiom A1 to prove #x imply ( #y imply #x ) imply #x:

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

prepare proof indentation,proof of M1.8c : line L01 : Premise >> Prop ; line L02 : A2 >> ( #x imply ( #y imply #x ) imply #x ) imply newline ( #x imply #y imply #x ) imply #x imply #x ; line L03 : A1 >> #x imply ( #y imply #x ) imply #x ; line L04 : MP ponens L02 ponens L03 >> ( #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

Patience, please

Line L03 may seem trivial. It just proves #x imply ( #y imply #x ) imply #x as an instance of Axiom A1. But verifying Line L03 is not completely trivial.

The complexity is due to generality. The Logiweb proof checker can handle a wide spectrum of theories. That has a cost in the form of some complexity.

The description in the following explains how Line L03 is verified in all its glory. When you are done with that explanation you have the general picture and know most there is to know about tactic expansion.

To understand what happens at code level you have to read the check page. If you do so, you will still benefit from having read the present documentation first. The present documentation explains the system top down. The check page describes the system bottom up.

Definitions

Axiom A1 says:

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

That statement macro expands into two definitions:

define statement of A1 as All #x ,, #y : #x imply #y imply #x end define

unitac define A1 as \ u . unitac-rule ( u ) end define

Furthermore, Prop contains A1:

theory Prop : A1 oplus A2 oplus A3 oplus MP oplus Def end theory

Thus, A1 states All #x ,, #y : #x imply #y imply #x, it behaves as defined by unitac-rule ( u ) inside argumentations, and it belongs to the theory Prop which we work inside.

Accumulation

During tactic expansion of the proof of M1.8c, the conclusions of proof lines are accumulated in s [[ !"pre" ]] of the tactic state s. The value of s [[ !"pre" ]] is a list of items of form l :: p :: x where l is the line number, p is the conclusion of the given line, and x can be used by individual tactics for their own purposes. The elements of s [[ !"pre" ]] can be used as premises for reasoning later in the proof ('pre' for 'premise').

Thus, when Line L03 is tactic expanded, the expander knows that we have 'proved' Prop ('proved' it by assuming it) and the expander knows that L01 stands for Prop. The expander also knows that we have proved the conclusion of Line L02 and that L02 stands for that conclusion. So in Line L03 we can use Prop and the conclusion of L02 as premises.

The value x above which individual tactics can use for their own purposes typically has form << a >> where a is a proof of the given line expressed in the Logiweb sequent calculus.

Invocation of the unification tactic

Line L03 is an argumentation line, so it is tactic expanded by invoking the unification tactic on it. The unification tactic in turn does unitac expansion of the argumentation A1 with the goal of proving the conclusion #x imply ( #y imply #x ) imply #x.

Note that the proof is expanded by two, distinct expansion machineries: tactic expansion and unitac expansion. Each time the tactic expander meets an argumentation line, it invokes the unitac expander on the argumentation of that line. Thus, the tactic expander does overall expansion of the proof whereas the unitac expander expands individual argumentations.

Unitac expansion

Now the unitac expander expands the argumentation A1 with the goal of proving #x imply ( #y imply #x ) imply #x. Since the unitac aspect of A1 is defined to be \ u . unitac-rule ( u ), the unitac expander invokes unitac-rule ( u ) on a structure u which contains everything a unitac needs.

Among other, the structure u above contains the tactic state s. unitac-rule ( u ) looks up s [[ !"unitac" ]] [[ !"rule" ]] to see how rules (i.e. axioms and inference rules) are handled in this, particular proof. The value of s [[ !"unitac" ]] [[ !"rule" ]] is \ u . unitac-rule-std ( u ) so unitac-rule ( u ) invokes unitac-rule-std ( u ). The unitac-rule-std ( u ) function defines the 'standard' way of treating rules.

Non-standard rule expansion

As an example of a proof which does not treat rules the standard way, consider the multzero proof whose source starts thus:

   PA proof of 3.2l : ...

The initial 'PA' causes the proof to be tactic expanded using the tactic definition of PA. The PA tactic installs a non-standard value in s [[ !"unitac" ]] [[ !"rule" ]] in order to handle hypotheses properly. In general, one needs a non-standard rule-unitac when using deduction. Furthermore, one will need different non-standard rule-unitacs for theories with different kinds of deduction theorems (like map theory versus first order logic).

Standard rule expansion

Now back to the proof of M1.8c above. The standard rule unitac unitac-rule-std ( u ) looks up the statement aspect of A1 and sees that A1 stands for All #x ,, #y : #x imply #y imply #x.

Then the unitac looks up s [[ !"pre" ]] in the tactic state s to see what it can use for proving A1 and finds that it can use the assumption Prop and the conclusion of Line L02. Then the unitac scans the assumptions and finds A1 in the statement aspect of Prop. Then the unitac constructs a proof expressed in the Logiweb sequent calculus which derives All #x ,, #y : #x imply #y imply #x from Prop.

The return value from the unitac is a new tactic state S for which S [[ !"arg" ]] is a sequent proof and S [[ !"con" ]] is the conclusion of the proof ('arg' for 'argumentation' and 'con' for 'conclusion').

The unitac sets the conclusion S [[ !"con" ]] to All #x ,, #y : #x imply #y imply #x since that is what the axiom says. Then the unitac sets s [[ !"arg" ]] to the sequent proof which derives All #x ,, #y : #x imply #y imply #x from Prop.

So now we have proved All #x ,, #y : #x imply #y imply #x but the goal was to prove #x imply ( #y imply #x ) imply #x.

Adaption

As mentioned, Line L03 is tactic expanded by the unification tactic. The unification tactic does unitac expansion of the argumentation A1 and then tries to adapt the outcome to the intended conclusion.

The unitac outcome is a proof of All #x ,, #y : #x imply #y imply #x and the goal is to prove the intended conclusion #x imply ( #y imply #x ) imply #x

Or, rather, since proof checking occurs after macro expansion, the unitac outcome is a proof of

All #x : All #y : #x imply #y imply #x

The unification tactic notes that the principal operator of the unitac outcome is a meta-quantifier and that the principal operator of the intended conclusion is no meta-quantifier. Thus, the unification tactic decides to instantiate the unitac outcome.

To instantiate the unitac outcome, the unification tactic constructs a fresh variable called something like unifresh ( #x , !"1" ). unifresh ( x , !"1" ) is an indexed meta-variable which the unification tactic thinks does not occur in the proof. Never use unifresh to construct your own variables or you may be in trouble.

Then the unification tactic adds a sequent operator to the unitac outcome which instantiates to unifresh ( #x , !"1" ). The result is a proof of

All #y : unifresh ( #x , !"1" ) imply #y imply unifresh ( #x , !"1" ).

Again, the unification tactic notes that the principal operator of the unitac outcome is a meta-quantifier and that the principal operator of the intended conclusion is no meta-quantifier, so it instantiates again to get a proof of

unifresh ( #x , !"1" ) imply unifresh ( #y , !"2" ) imply unifresh ( #x , !"1" ).

Note how the fresh variables have two indexes: one which shows the variable name before freshening and one which makes the fresh variable unique. Fresh variables often occur in error messages where the name before freshening is nice to have.

So now we have proved

unifresh ( #x , !"1" ) imply unifresh ( #y , !"2" ) imply unifresh ( #x , !"1" )

but the goal was to prove

#x imply ( #y imply #x ) imply #x.

Unification

After adaption, the unification tactic tries to unify the unitac outcome to the intended conclusion. Unification of

unifresh ( #x , !"1" ) imply unifresh ( #y , !"2" ) imply unifresh ( #x , !"1" )

and

#x imply ( #y imply #x ) imply #x

has the following solution:

unifresh ( #x , !"1" ) == #x

unifresh ( #y , !"2" ) == #y imply #x

Thus, the unification tactic adds sequent operators to the unitac outcome which replaces unifresh ( #x , !"1" ) with #x and unifresh ( #y , !"2" ) with #y imply #x, yielding a proof of the intended conclusion #x imply ( #y imply #x ) imply #x.

When unification is impossible

If you write e.g. A1 conclude #x imply #x imply #y in a proof then the unification tactic will try to unify

unifresh ( #x , !"1" ) imply unifresh ( #y , !"2" ) imply unifresh ( #x , !"1" )

and

#x imply #x imply #y

which is impossible since #x and #y are distinct meta-variables. In this case you will get an Unable to unify x with y error message. In general, when unification is impossible you will get an error message telling you that you cannot unify some term with some other term.

Quite often, it is difficult the spot the error based on the two terms which cannot be unified. Typically, it is much faster just to look at the proof line which is in error. Normally, the error is obvious.

When unification is incomplete

In some cases, unification is not enough to see how all variables should be instantiated. In such cases you get an error message like Incomplete unification. Uninstantiated variable: x. We shall see examples of that later.

What adaption can do

In the example above, adaption removed meta-quantifiers from the root of the unitac outcome. In general, adaption can remove meta-quantifiers All x : A, inferences A infer B, and endorsements A endorse B. In practice, adaption removes lots of quantifiers and endorsements and few inferences. At least that is what happens for the proofs I write.

Adaption removes quantifiers by instantiating them and removes endorsements by verifying them. An endorsement A endorse B is removed by evaluating the side condition A and checking that it evaluates to true.

Adaption does not do instantiation and verification itself. Rather, it adds sequent operators for doing so and leaves it to the sequent calculus to do the actual instantiations and verifications.

As long as you do not violate side conditions, adaption will make side conditions go away. If you accidentally do violate a side condition, you will get a Verify-seqop used on false condition message from the sequent calculus.

Adaption will be covered in more detail various places in the following.

Prev Up Next Page 328 of 800 Search logiweb.eu

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