6.7.17 Peano arithmetic

Page 103 of 800

Search internet

The Peano page defines Peano arithmetic thus:

theory PA : FOL oplus S1 oplus S2 oplus S3 oplus S4 oplus S5 oplus S6 oplus S7 oplus S8 oplus S9 end theory

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

Proofs in are tactic evaluated by $\ u . tactic-FOL ( u )$ . This FOL tactic constantly needs Prop and FOL as premisses. It would take too much cpu time if the tactic should prove Prop and FOL each time they are needed. For that reason, the FOL tactic generates sequent operators which prove FOL in the beginning of the proof. That is trivial when working in FOL itself, but requires a couple of sequent operations when working e.g. in .

There is only one difference between $\ u . tactic-Prop ( u )$ and $\ u . tactic-FOL ( u )$ . The latter starts out proving both Prop and FOL . The former only proves Prop .

For completeness, here are the axioms of Peano .

rule S1 : all x ,, y ,, z : ( x = y imply x = z imply y = z ) end rule

rule S2 : all x ,, y : ( x = y imply x suc = y suc ) end rule

rule S3 : all x : not 0 = x suc end rule

rule S4 : all x : x suc = y suc imply x = y end rule

rule S5 : all x : x + 0 = x end rule

rule S6 : all x ,, y : x + y suc = ( x + y ) suc end rule

rule S7 : all x : x * 0 = 0 end rule

rule S8 : all x ,, y : x * y suc = x * y + x end rule

rule S9 : All #x ,, #a ,, #z ,, #i : sub ( #z , #a , #x , 0 ) endorse sub ( #i , #a , #x , #x suc ) endorse #z imply all #x : ( #a imply #i ) imply #a end rule

Page 103 of 800

Search logiweb.eu