8.6.1 The FOL tactic

Prev Up Next Page 347 of 800 Search internet

The Peano page defines Peano arithmetic PA on top of First Order Predicate Calculus FOL and defines FOL on top of Propositional Calculus Prop:

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

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

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

We refer to FOL and theories like PA which include FOL as first order theories. The Peano page assigns the FOL tactic \ u . tactic-FOL ( u ) to PA and FOL. In general, the FOL tactic can be used with arbitrary first order theories.

Theories which build on Prop but not on FOL can use \ u . tactic-Prop ( u ) instead. The Prop tactic is like the FOL tactic but cannot handle quantifiers.

The FOL tactic allows to state proofs in a style which is convenient in connection with first order theories. The tactic translates FOL proofs into sequent proofs and may be seen as an implementation of a high level proof language on top of the low level sequent proof language.

Prev Up Next Page 347 of 800 Search logiweb.eu

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