Logiweb(TM)

6.7.16 First order predicate calculus

Prev Up Next Page 102 of 800 Search internet


The Peano page defines FOL thus:

rule A4 : All #t ,, #x ,, #a ,, #b : sub ( #b , #a , #x , #t ) endorse all #x : #a imply #b end rule

rule AP4 : All #a ,, #b : inst ( #a , #b ) endorse #a imply #b end rule

rule A5 : All #x ,, #a ,, #b : #x avoid #a endorse all #x : ( #a imply #b ) imply #a imply all #x : #b end rule

rule Gen : All #u ,, #x : #x infer all #u : #x end rule

theory FOL : Prop oplus A4 oplus AP4 oplus A5 oplus Gen end theory

tactic define FOL as \ u . tactic-FOL ( u ) end define

For the sake of efficiency, the Peano page includes an axiom AP4 of parallel instantiation which allows to do multiple variable instantiations in parallel. A4 and AP4 can substitute each other. If one omits AP4 then proofs may become longer and more complicated. AP4 can directly replace A4. On the other hand, if one adds axioms for meta-reasoning about side conditions, the side condition of A4 may be easier to reason about than the side condition of AP4. In FOL, both A4 and AP4 are included.

In the definition of FOL note that Prop is included as an axiom. That makes all axioms of Prop available because of the way the rule tactic \ u . unitac-rule ( u ) works. It is the tactic which defines how to prove an axiom: Look it up in all presently assumed theories and see it is there. If yes, generate a sequent term which extracts the axiom from the theory in which it is found.

If the rule tactic is asked to prove e.g. A1 in FOL it will look up the definition of FOL in the cache. The tactic sees that FOL is a meta-conjunction. Then it looks into each conjunct. First conjunct of FOL is Prop, then the tactic looks up the definition of Prop and sees it is a meta-conjunction. Then it looks into each conjunction and finds A1 as first conjunct. Then the tactic generates a sequent term which says FOL is true because it is assumed, then dereferences FOL into the definition of FOL, then takes the head of that to get Prop, then dereferences Prop into the definition of Prop, then takes the head of that to get A1, and finally dereferences A1 into the definition of A1.

Prev Up Next Page 102 of 800 Search logiweb.eu

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