|Page 347 of 800||Search internet|
The Peano page defines Peano arithmetic on top of First Order Predicate Calculus and defines on top of Propositional Calculus :
We refer to and theories like which include as first order theories. The Peano page assigns the FOL tactic to and . In general, the FOL tactic can be used with arbitrary first order theories.
Theories which build on but not on can use 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.
|Page 347 of 800||Search logiweb.eu|