Axioms in KIF

Cut and paste these into Tau, as premises or conclusions. It will help if this is done in a way to form valid arguments.

See Axiom, Axiomatic System (Wikipedia), Axioms (MetaMath) and A Primer for Logic and Proof, (Hirst and Hirst).

• Peano Arithmetic (PA)
• Presburger Arithmetic (PrA), a subtheory of PA -- it lacks multiplication
• Extensions and subtheories of PA and PrA
  • Theory of the successor function (Succ)
  • PA + < (PALT)
  • PrA + < (PrALT)
  • PA + Odd/Even (PAOE)
  • PrA + Odd/Even (PrAOE)
• Theory of Commutative Ordered Fields (COF)

See, too, the Wikipedia articles, Peano arithmetic, Presburger arithmetic, and decision problem. In print, see also:

Enderton, Herbert B.
A Mathematical Introduction to Logic, 2nd Ed.
Harcourt Academic Press, New York, 2001

Note that some proofs in Peano arithmetic and Presburger arithmetic require that Tau apply mathematical induction (see the checkbox) or use previously proved results, while others do not. We leave it as an exercise for the reader to determine which.

Peano axioms (the theory PA, which Gödel's incompleteness theorem showed to be undecidable):

(forall ?X (not (= 0 (succ ?X))))
(forall ?X (forall ?Y (=> (= (succ ?X) (succ ?Y)) (= ?X ?Y))))
(forall ?X (= (+ ?X 0) ?X))
(forall ?X (forall ?Y (= (+ ?X (succ ?Y)) (succ (+ ?X ?Y)))))
(forall ?X (forall ?Y (= (* 0 ?X) 0)))
(forall ?X (forall ?Y (= (* ?X (succ ?Y)) (+ (* ?X ?Y) ?X))))

Additionally, mathematical induction may be used (all instances of):

(=> (and (F 0) (forall ?X (=> (F ?X) (F (succ ?X)))) (forall ?X (F ?X)))), where F represents any formula with one free variable.

Some theorems of PA:

PAThm01="(forall (?X ?Y ?Z) (=> (and (not (= ?X 0)) (= (* ?X ?Y) (* ?X ?Z))) (= ?Y ?Z)))"
PAThm02="(forall (?X ?Y ?Z) (=> (and (not (= ?X 0)) (= (* ?Y ?X) (* ?Z ?X))) (= ?Y ?Z)))"
PAThm03="(forall (?X ?Y ?Z) (= (* ?X (+ ?Y ?Z)) (+ (* ?X ?Y) (* ?X ?Z))))"
PAThm03V="(forall (?X ?Y ?Z) (= (* (+ ?Y ?Z) ?X) (+ (* ?Y ?X) (* ?Z ?X))))"
PAThm04="(forall ?X (= ?X (* (succ 0) ?X)))"
PAThm04V="(forall ?X (= ?X (* ?X (succ 0))))"
PAThm05="(forall ?X (= (* 0 ?X) 0))"
PAThm06="(forall (?X ?Y) (= (* (succ ?X) ?Y) (+ (* ?X ?Y) ?Y)))"

Presburger Arithmetic axioms (the theory PrA), is a subtheory of Peano arithmetic -- it lacks multiplication; it is decidable, but already has difficult computational complexity.

(forall ?X (not (= 0 (succ ?X))))
(forall ?X (forall ?Y (=> (= (succ ?X) (succ ?Y)) (= ?X ?Y))))
(forall ?X (= (+ ?X 0) ?X))
(forall ?X (forall ?Y (= (+ ?X (succ ?Y)) (succ (+ ?X ?Y)))))

Induction (all instances of):

(=> (and (F 0) (forall ?X (=> (F ?X) (F (succ ?X)))) (forall ?X (F ?X)))) , where F represents any formula with one free variable.

Some theorems of PrA:

(forall (?X ?Y) (= (+ ?X ?Y) (+ ?Y ?X)))

More PA and PrA theorems:

PAThm01="(forall (?X ?Y ?Z) (=> (and (not (= ?X 0)) (= (* ?X ?Y) (* ?X ?Z))) (= ?Y ?Z)))"
PAThm02="(forall (?X ?Y ?Z) (=> (and (not (= ?X 0)) (= (* ?Y ?X) (* ?Z ?X))) (= ?Y ?Z)))"
PAThm03="(forall (?X ?Y ?Z) (= (* ?X (+ ?Y ?Z)) (+ (* ?X ?Y) (* ?X ?Z))))"
PAThm03V="(forall (?X ?Y ?Z) (= (* (+ ?Y ?Z) ?X) (+ (* ?Y ?X) (* ?Z ?X))))"
PAThm04="(forall ?X (= ?X (* (succ 0) ?X)))"
PAThm04V="(forall ?X (= ?X (* ?X (succ 0))))"
PAThm05="(forall ?X (= (* 0 ?X) 0))"
PAThm06="(forall (?X ?Y) (= (* (succ ?X) ?Y) (+ (* ?X ?Y) ?Y)))"

PrA01="(forall ?X (= (+ 0 ?X) ?X))"
PrA02="(forall ?X (= (+ ?X 0) (+ 0 ?X)))"
PrA03="(forall ?X (= (succ ?X) (+ ?X (succ 0))))"
PrA04="(forall ?X (= (succ ?X) (+ (succ 0) ?X)))"
PrA05="(forall ?Y (= (succ (succ (+ 0 ?Y))) (+ (succ 0) (succ ?Y))))"
PrA06="(forall ?X (=> (not (exists ?Y (= ?X (+ ?Y ?Y)))) (exists ?Y (= (succ ?X) (+ ?Y ?Y)))))"
PrA07="(forall (?Y ?X) (= (+ (succ ?X) ?Y) (succ (+ ?X ?Y))))"
PrA08="(forall (?X ?Y) (=> (= (succ ?X) ?Y) (= ?Y (+ ?X (succ 0)))))"
PrA09="(forall ?X (= (+ (succ ?X) 0) (succ (+ ?X 0))))"
PrA10="(forall (?X ?Y) (forall ?Z (=> (and (= ?X (+ ?Y ?Y)) (= ?X (+ ?Z ?Z))) (= ?Y ?Z))))"
PrA11="(forall (?X ?Y ?Z) (=> (= (succ ?X) (+ (succ ?Y) (succ ?Z))) (= ?X (succ (+ ?Y ?Z)))))"
PrA12="(forall ?X (= (+ (succ ?X) 0) (succ (+ ?X 0))))"
PrA13="(forall (?X ?Y) (=> (= ?X ?Y) (= (succ ?X) (succ ?Y))))"
PrA14="(= (+ 0 0) 0)"
PrA15="(not (exists ?X (= 0 (+ (succ ?X) (succ ?X)))))"
PrA16="(forall (?X ?Y) (= (succ (succ (+ ?X ?Y))) (+ (succ ?X) (succ ?Y))))"
PrA17="(forall (?X ?Y) (= (+ (succ 0) (+ ?X ?Y)) (succ (+ ?X ?Y))))"
PrA18="(forall (?X ?Y) (=> (= 0 (+ ?X ?Y)) (and (= 0 ?X) (= 0 ?Y))))"
PrA19="(forall (?X ?Y) (=> (= (+ ?X ?X) (+ ?Y ?Y)) (= ?X ?Y)))"
PrA20="(forall (?X ?Y ?Z) (=> (= (+ ?X ?Y) (+ ?X ?Z)) (= ?Y ?Z)))"
PrA21="(forall (?X ?Y ?Z) (=> (= (+ ?Z ?X) (+ ?Y ?X)) (= ?Z ?Y)))"
PrA22="(forall (?X ?Y ?Z) (=> (= (+ ?X ?Y) (+ ?X ?Z)) (= (succ ?Y) (succ ?Z))))"
PrA24="(= 0 (+ 0 0))"
PrA25="(forall (?X ?Y) (=> (= (+ 0 ?X) (+ 0 ?Y)) (= ?X ?Y)))"
PrA26="(forall (?X ?Y ?Z) (=> (= (succ (+ ?X ?Y)) (succ (+ ?X ?Z))) (= ?Y ?Z)))"
PrA27="(forall (?X ?Y) (= (succ (+ ?X ?Y)) (succ (+ ?Y ?X))))"
PrA28="(forall (?X ?Y ?Z) (=> (= (+ (succ ?X) ?Y) (+ (succ ?X) ?Z)) (= ?Y ?Z)))"
PrA29="(forall (?X ?Y) (= (+ (succ ?X) ?Y) (+ ?X (succ ?Y))))"
PrA30="(forall (?X ?Y ?Z ?W) (<=> (= (+ ?X ?Y) (+ ?Z ?W)) (= (+ (succ ?X) (succ ?Y)) (+ (succ ?Z) (succ ?W)))))"
PrA31="(forall (?X ?Y) (= (succ (succ (+ ?X ?Y))) (+ (succ ?X) (succ ?Y))))"
PrA32="(forall (?X ?Y ?Z) (<=> (= (+ ?X ?Y) ?Z) (= (+ ?X (succ ?Y)) (succ ?Z))))"
PrA33="(forall (?X ?Y ?Z) (<=> (= (+ ?X ?Y) ?Z) (= (+ (succ ?X) ?Y) (succ ?Z))))"
PrA34="(forall (?X ?Y) (=> (= (succ (succ ?X)) (succ (succ ?Y))) (= ?X ?Y)))"
PrA35="(forall (?X ?Y) (= (succ (+ ?X ?Y)) (succ (+ ?Y ?X))))"
# PrA36=""
PrA37="(forall (?X ?Y ?Z ?W) (<=> (= (+ ?X ?Y) (+ ?Z ?W)) (= (succ (+ ?X ?Y)) (succ (+ ?Z ?W)))))"
PrA38="(forall (?X ?Y ?Z) (<=> (= (+ ?X ?Y) ?Z) (= (succ (+ ?X ?Y)) (succ ?Z))))"
PrA39="(forall (?X ?Y ?Z) (=> (= (succ (+ ?X ?Y)) (succ (+ ?X ?Z))) (= ?Y ?Z)))"
PrA40="(forall (?X ?Y ?Z) (<=> (= (+ ?X ?Y) (+ ?X ?Z)) (= (+ ?X (succ ?Y)) (+ ?X (succ ?Z)))))"
PrA41="(forall (?X ?Y ?Z) (<=> (= (+ ?Y ?X) (+ ?Z ?X)) (= (+ (succ ?Y) ?X) (+ (succ ?Z) ?X))))"
PrA42="(forall (?X ?Y) (= (+ (succ ?X) ?Y) (succ (+ ?X ?Y))))"
PrA43="(forall (?X ?Y ?Z) (=> (= (+ ?X ?Y) ?Z) (= (+ (succ ?X) ?Y) (succ ?Z))))"
PrA44="(forall (?X ?Y ?Z) (=> (= (+ (succ ?X) ?Y) (succ ?Z)) (= (+ ?X ?Y) ?Z)))"
PrA45="(forall (?X ?Y ?Z) (=> (= (+ ?X ?Y) ?Z) (= (+ ?X (succ ?Y)) (succ ?Z))))"
PrA46="(forall (?X ?Y ?Z) (=> (= (+ ?X (succ ?Y)) (succ ?Z)) (= (+ ?X ?Y) ?Z)))"
PrA47="(forall (?X ?Y ?Z) (=> (= (+ (succ ?X) (succ ?Y)) (succ (succ ?Z))) (= (+ ?X ?Y) ?Z)))"
PrA48="(forall (?X ?Y ?Z) (=> (= (+ ?X ?Y) ?Z) (= (+ (succ ?X) (succ ?Y)) (succ (succ ?Z)))))"
PrA51="(forall (?X ?Y) (<=> (= (+ 0 0) (+ ?X ?X)) (= 0 ?X)))"
PrA52="(forall (?X ?Y ?Z) (=> (= ?X ?Y) (= (+ ?X ?Z) (+ ?Y ?Z))))"
PrA53="(forall (?X ?Y ?Z) (=> (= ?X ?Y) (= (+ ?Z ?X) (+ ?Z ?Y))))"
PrA54="(forall (?X ?Y) (=> (= (+ ?X ?Y) ?X) (= ?Y 0)))"
PrA55="(forall ?X (not (= ?X (succ ?X))))"
PrA56="(forall (?X ?Y ?Z) (=> (= (succ (+ ?X ?Y)) (+ ?X ?Z)) (= (succ ?Y) ?Z)))"
PrA57="(forall (?X ?Y ?Z) (=> (= (+ ?X (succ ?Y)) (+ ?X ?Z)) (= (succ ?Y) ?Z)))"
PrA59="(forall (?X ?Y ?Z) (<=> (= (+ (succ ?X) ?Y) (+ (succ ?X) ?Z)) (= (+ ?X ?Y) (+ ?X ?Z))))"
PrA60="(forall (?X ?Y ?Z) (<=> (= (+ ?Y (succ ?X)) (+ ?Z (succ ?X))) (= (+ ?Y ?X) (+ ?Z ?X))))"
PrA61="(forall (?X ?Y ?Z) (<=> (= (+ (succ ?X) ?Y) ?Z) (= (+ ?X ?Y) (succ ?Z))))"

We may also consider simply the theory of the successor function (Succ), with the axioms:

(forall ?X (not (= 0 (succ ?X))))
(forall ?X (forall ?Y (=> (= (succ ?X) (succ ?Y)) (= ?X ?Y))))

And with Induction (all instances of):

(=> (and (F 0) (forall ?X (=> (F ?X) (F (succ ?X)))) (forall ?X (F ?X)))) , where F represents any formula with one free variable.

Some theorems of Succ:

(forall (?X ?Y) (=> (= (succ ?X) (succ ?Y)) (= ?X ?Y)))
(forall ?X (exists ?Y (= ?Y (succ ?X))))

Combinations and reductions of these sets of axioms (PA, PrA, and Succ), together with the introduction of definitions give us other theories. which we will denote below, while presenting some sample axioms of each theory. Each of these theories may also be extended by the use of induction. Some of the theories involve only 'succ', some involve addition and multiplication also. There are various courses possible with extension by definition and with axiomatization by primitives. For example, '<' may be defined axiomatically in an extension of the theory Succ; alternatively, it may be defined in PrA.

PrA + < (PrALT)

PrALT01="(< 0 (succ 0))"
PrALT02="(=< 0 (succ 0))"
PrALT03="(< (succ 0) (succ (succ 0)))"
PrALT04="(=< (succ 0) (succ (succ 0)))"
PrALT05="(forall ?X (=> (< 0 ?X) (< ?X (+ ?X ?X))))"
PrALT06="(forall ?X (< ?X (succ ?X)))"
PrALT07="(forall ?X (=< ?X (succ ?X)))"
PrALT08="(forall ?X (not (< ?X ?X)))"
PrALT09="(forall ?X (=< ?X ?X))"
PrALT10="(forall (?X ?Y) (or (=< ?X ?Y) (=< ?Y ?X)))"
PrALT11="(forall (?X ?Y) (=> (< ?X ?Y) (=< ?X ?Y)))"
PrALT12="(forall (?X ?Y) (<=> (=< ?X ?Y) (or (= ?X ?Y) (< ?X ?Y))))"
PrALT13="(forall (?X ?Y) (<=> (=< ?X ?Y) (or (= ?X ?Y) (not (< ?Y ?X)))))"
PrALT14="(forall (?X ?Y) (=> (and (=< ?X ?Y) (not (= ?X ?Y))) (< ?X ?Y)))"
PrALT15="(forall (?X ?Y) (=< ?X (+ ?X ?Y)))"
PrALT16="(forall (?X ?Y) (=> (not (= ?Y 0)) (< ?X (+ ?X ?Y))))"
PrALT17="(forall (?X ?Y) (=> (< 0 ?Y) (< ?X (+ ?X ?Y))))"
PrALT18="(forall (?Y ?X ?Z) (=> (and (< ?X ?Y) (< ?Y ?Z)) (< ?X ?Z)))"
PrALT19="(forall (?Y ?X) (forall ?Z (=> (and (=< ?X ?Y) (=< ?Y ?Z)) (=< ?X ?Z))))"
PrALT20="(forall ?X (exists ?Y (< ?X ?Y)))"
PrALT21="(forall ?X (exists ?Y (=< ?X ?Y)))"
PrALT22="(forall (?X ?Y) (=> (and (=< ?X ?Y) (=< ?Y ?X)) (= ?X ?Y)))"
PrALT23="(forall (?X ?Y) (=> (= ?X ?Y) (=< ?X ?Y)))"
PrALT24="(forall ?X (not (=< (succ ?X) ?X)))"
PrALT25="(forall ?X (=< 0 ?X))"
PrALT26="(forall (?X ?Y) (<=> (=< ?X ?Y) (=< (succ ?X) (succ ?Y))))"
PrALT27="(forall ?X (not (< (succ ?X) ?X)))"
PrALT28="(forall (?X ?Y) (<=> (< ?X ?Y) (< (succ ?X) (succ ?Y))))"
PrALT29="(forall (?X ?Y) (<=> (< ?X ?Y) (=< (succ ?X) ?Y)))"
PrALT30="(forall (?X ?Y) (=> (=< (succ ?X) ?Y) (=< ?X ?Y)))"
PrALT31="(forall (?X ?Y) (=> (=< (succ ?X) ?Y) (< ?X ?Y)))"
PrALT32="(forall (?X ?Y) (=> (< (succ ?X) ?Y) (< ?X ?Y)))"
PrALT33="(forall ?X (not (= ?X (succ ?X))))"
PrALT34="(forall (?X ?Y) (<=> (= ?X ?Y) (= (succ ?X) (succ ?Y))))"
PrALT35="(forall (?X ?Y ?Z ?W ?T) (=> (and (= (+ ?X ?Y) ?Z) (= (+ ?Z ?W) ?T)) (= (+ ?X (+ ?Y ?W)) ?T)))"
PrALT36="(forall (?X ?Y) (<=> (= ?X ?Y) (= (+ ?X 0) ?Y)))"
PrALT37="(forall (?X ?Y ?Z) (= (+ (+ ?X ?Y) (+ ?Y ?Z)) (+ (+ ?X (+ ?Y ?Y)) ?Z)))"
PrALT38="(forall (?X ?Y) (=> (or (not (= 0 ?X)) (not (= 0 ?Y))) (not (= 0 (+ ?X ?Y)))))"
PrALT39="(forall (?X ?Y) (=> (< 0 ?Y) (< ?X (+ ?X ?Y))))"
PrALT40="(forall ?X (not (< ?X 0)))"
PrALT41="(forall (?X ?Y) (<=> (< ?X (succ ?Y)) (or (= ?X ?Y) (< ?X ?Y))))"
PrALT42="(forall (?X ?Y) (or (< ?X ?Y) (< ?Y ?X) (= ?X ?Y)))"
PrALT43="(forall (?X ?Y) (<=> (< ?X ?Y) (and (not (= ?X ?Y)) (not (< ?Y ?X)))))"
PrALT44="(forall (?X ?Y) (<=> (= ?X ?Y) (and (not (< ?X ?Y)) (not (< ?Y ?X)))))"
PrALT45="(forall (?X ?Y) (<=> (not (= ?X ?Y)) (or (< ?X ?Y) (< ?Y ?X))))"
PrALT46="(forall (?X ?Y) (=> (< ?X ?Y) (not (= ?X ?Y))))"
PrALT47="(forall (?X ?Y) (=> (< (succ ?X) ?Y) (< ?X ?Y)))"
PrALT48="(forall (?X ?Y) (<=> (not (= ?X ?Y)) (or (< ?X ?Y) (< ?Y ?X))))"
PrALT49="(forall (?X ?Y) (<=> (< ?X ?Y) (< (succ ?X) (succ ?Y))))"
PrALT50="(forall (?X ?Y) (<=> (=< ?X ?Y) (=< (succ ?X) (succ ?Y))))"

PA + < (PALT)

(forall (?X ?Y) (=> (< 0 ?Y) (=< ?X (* ?X ?Y))))

'(even ?X)' may be defined in PA or PrA as '(exists ?Y (= ?X (+ ?Y ?Y)))', and '(odd ?X)' as '(not (even ?X))'.

Some theorems of PALT:

PALT01="(forall (?X ?Y) (=> (and (< 0 ?X) (< 0 ?Y)) (=< (+ ?X ?Y) (* ?X ?Y))))"
PALT02="(forall (?X ?Y) (=> (and (< (succ 0) ?X) (< (succ 0) ?Y)) (< (+ ?X ?Y) (* ?X ?Y))))"
PALT03="(forall (?X ?Y) (=> (and (< (succ 0) ?X) (< (succ 0) ?Y)) (< (succ ?X) (* ?X ?Y))))"
PALT04="(forall (?X ?Y) (=> (and (< (succ 0) ?X) (< (succ 0) ?Y)) (< (succ (+ ?X ?Y)) (* ?X ?Y))))"
PALT05="(forall (?X ?Y) (=> (< 0 ?Y) (< (* ?X ?Y) (* (succ ?X) ?Y))))"
PALT06="(forall (?X ?Y) (=> (< 0 ?X) (< (* ?X ?Y) (* ?X (succ ?Y)))))"
PALT07="(forall (?X ?Y) (=> (and (< 0 ?X) (< 0 ?Y)) (< (succ (+ ?X ?Y)) (succ (* ?X ?Y)))))"
PALT08="(forall (?X ?Y ?Z) (=> (and (< (succ 0) ?Z) (< 0 ?X) (< 0 ?Y)) (< (* ?X ?Y) (* ?X (* ?Y ?Z)))))"

PA + Odd/Even (PAOE)

PAOE01="(odd (* (succ 0) (succ 0)))"
PAOE02="(even (* 0 0))"
PAOE03="(forall ?X (even (* 0 ?X)))"
PAOE04="(forall ?X (=> (even ?X) (even (* ?X ?X))))"
PAOE05="(forall (?X ?Y) (=> (even ?X) (even (* ?X ?Y))))"
PAOE06="(forall (?X ?Y) (=> (and (even ?X) (odd ?Y)) (even (* ?X ?Y))))"
PAOE07="(forall (?X ?Y) (=> (and (odd ?X) (odd ?Y)) (odd (* ?X ?Y))))"
PAOE08="(forall (?X ?Y) (=> (even (* ?X ?Y)) (even (* ?Y ?X))))"
PAOE09="(forall (?X ?Y) (<=> (even (* ?X ?Y)) (even (* (succ ?X) (succ ?Y)))))"
PAOE10="(forall (?X ?Y) (=> (odd (* ?X ?Y)) (even (* (succ ?X) ?Y))))"
PAOE11="(forall (?X ?Y) (=> (odd (* ?X ?Y)) (even (* ?X (succ ?Y)))))"
PAOE12="(forall (?X ?Y) (=> (even (* ?X ?Y)) (or (even ?X) (even ?Y))))"

PrA + Odd/Even (PrAOE)PrAOE Theorems, Lemmas

PrAOE01="(even 0)"
PrAOE02="(even (+ 0 0))"
PrAOE03="(not (even (succ 0)))"
PrAOE04="(even (succ (succ 0)))"
PrAOE05="(odd (succ 0))"
PrAOE06="(not (odd 0))"
PrAOE07="(even (succ (succ (succ (succ (succ (succ (succ (succ 0)))))))))"
PrAOE08="(odd (succ (succ (succ (succ (succ (succ (succ 0))))))))"
PrAOE09="(forall ?X (=> (even ?X) (even (+ 0 ?X))))"
PrAOE10="(forall ?X (even (+ ?X ?X)))"
PrAOE11="(forall ?X (<=> (even ?X) (not (odd ?X))))"
PrAOE12="(forall ?X (=> (even ?X) (even (+ ?X ?X))))"
PrAOE13="(forall ?X (or (even ?X) (odd ?X)))"
PrAOE14="(forall ?X (=> (even ?X) (even (succ (succ ?X)))))"
PrAOE15="(forall ?X (=> (even ?X) (even (+ (succ (succ 0)) ?X))))"
PrAOE16="(forall ?X (=> (even ?X) (odd (succ ?X))))"
PrAOE17="(forall ?X (<=> (even ?X) (not (odd ?X))))"
PrAOE18="(forall ?X (=> (odd ?X) (even (succ ?X))))"
PrAOE19="(forall ?X (=> (odd ?X) (odd (succ (succ ?X)))))"
PrAOE20="(forall ?X (<=> (odd ?X) (not (even ?X))))"
PrAOE21="(forall (?X ?Y) (=> (and (even ?X) (even ?Y)) (even (+ ?X ?Y))))"
PrAOE22="(forall (?X ?Y) (=> (even (+ ?X ?Y)) (even (+ (succ ?X) (succ ?Y)))))"
PrAOE23="(forall (?X ?Y) (=> (and (odd ?X) (odd ?Y)) (even (+ ?X ?Y))))"
PrAOE24="(forall (?X ?Y) (=> (and (odd ?X) (even ?Y)) (odd (+ ?X ?Y))))"
PrAOE25="(forall (?X ?Y) (=> (odd (+ ?X ?Y)) (or (odd ?X) (odd ?Y))))"
PrAOE26="(forall (?X ?Y) (= (succ (succ (+ ?X ?Y))) (+ (succ ?X) (succ ?Y))))"
PrAOE27="(forall ?X (=> (even (succ (succ ?X))) (even ?X)))"
PrAOE28="(forall ?X(or (not (odd ?X)) (not (even ?X))))"
PrAOE30="(forall ?X (<= (even (succ (succ ?X))) (even ?X)))"
PrAOE31="(forall (?X ?Y) (<=> (= ?Y (+ (+ ?X ?X) (succ 0))) (odd ?Y)))"
PrAOE32="(forall (?X ?Y) (=> (even (+ ?X ?Y)) (even (+ ?Y ?X))))"

Theory of Commutative Ordered Fields (COF)

From Kalish & Montague, 1st. ed. Chapter VIII page 280
See also Field Axioms

Constants
0 Zero / Identity Element for Addition
1 One / Identity Element for Multiplication Function symbols
+ Addition
* Multiplication
neg Negation / Additive Inverse
recip Reciprocal / Multiplicative Inverse Predicate symbols
< Less Than
=< Less Than or Equal To

Axioms

A1
x + (y + z) = (x + y) + z
COF_A01="(forall (?X ?Y ?Z) (= (+ ?X (+ ?Y ?Z)) (+ (+ ?X ?Y) ?Z)))" Axiom A2
x + y = y + x
COF_A02="(forall (?X ?Y) (= (+ ?X ?Y) (+ ?Y ?X)))" Axiom A3
x + 0 = x
COF_A03="(forall ?X (= (+ ?X 0) ?X))" Axiom A4
x + neg(x) = 0
COF_A04="(forall ?X (= (+ ?X (neg ?X)) 0))" Axiom A5
x * (y * z) = (x * y) * z
COF_A05="(forall (?X ?Y ?Z) (= (* ?X (* ?Y ?Z)) (* (* ?X ?Y) ?Z)))" Axiom A6
x * y = y * x
COF_A06="(forall (?X ?Y) (= (* ?X ?Y) (* ?Y ?X)))" Axiom A7
x * 1 = x
COF_A07="(forall ?X (= (* ?X 1) ?X))" Axiom A8
~(x = 0) => x * recip(x) = 1
COF_A08="(forall ?X (=> (not (= ?X 0)) (= (* ?X (recip ?X)) 1)))" Axiom A9
x * (y + z) = (x * y) + (x * z)
COF_A09="(forall (?X ?Y ?Z) (= (* ?X (+ ?Y ?Z)) (+ (* ?X ?Y) (* ?X ?Z))))" Axiom A10
~(0 = 1)
COF_A10=" (not (= 0 1))" Axiom A11
0 =< x | 0 =< -x
COF_A11="(forall ?X (or (=< 0 ?X) (=< 0 (neg ?X))))" Axiom A12
~(x = 0) => ~(0 =< x) | ~(0 =< neg(x))
COF_A12="(forall ?X (=> (not (= ?X 0)) (or (not (=< 0 ?X)) (not (=< 0 (neg ?X))))))" Axiom A13
(0 =< x) & (0 =< y) => 0 =< (x + y)
COF_A13="(forall (?X ?Y) (=> (and (=< 0 ?X) (=< 0 ?Y)) (=< 0 (+ ?X ?Y))))" Axiom A14
(0 =< x) & (0 =< y) => 0 =< (x * y)
COF_A14="(forall (?X ?Y) (=> (and (=< 0 ?X) (=< 0 ?Y)) (=< 0 (* ?X ?Y))))" Axiom A15
(x =< y) <=> (0 =< (y + neg(x)))
COF_A15="(forall (?X ?Y) (<=> (=< ?X ?Y) (=< 0 (+ ?Y (neg ?X)))))"

The Theory of Commutative Ordered Fields:

COF="
$COF_A01
$COF_A02
$COF_A03
$COF_A04
$COF_A05
$COF_A06
$COF_A07
$COF_A08
$COF_A09
$COF_A10
$COF_A11
$COF_A12
$COF_A13
$COF_A14
$COF_A15"

Axioms of the Theory of Commutative Ordered Fields that exclude those axioms that apply multiplication:

COF_NM="
$COF_A01
$COF_A02
$COF_A03
$COF_A04
$COF_A10
$COF_A11
$COF_A12
$COF_A13
$COF_A15
"

Axioms of the Theory of Commutative Ordered Fields whose use of function symbols is limited to addition:

COF_A="
$COF_A01
$COF_A02
$COF_A03
$COF_A13
"

Axioms of the Theory of Commutative Ordered Fields whose use of function symbols is limited to addition and negation:

COF_AN="
$COF_A01
$COF_A02
$COF_A03
$COF_A04
$COF_A11
$COF_A12
$COF_A13
$COF_A15
"

Axioms of the Theory of Commutative Ordered Fields that exclude those axioms that apply less-than-or-equal-to:

COF_NLT="
$COF_A01
$COF_A02
$COF_A03
$COF_A04
$COF_A05
$COF_A06
$COF_A07
$COF_A08
$COF_A09
$COF_A10
"

Axioms of the Theory of Commutative Ordered Fields that include those axioms that apply less-than-or-equal-to:

COF_LT="
$COF_A01
$COF_A02
$COF_A03
$COF_A04
$COF_A05
$COF_A06
$COF_A07
$COF_A08
$COF_A09
$COF_A10
$COF_A11
$COF_A12
$COF_A13
$COF_A14
$COF_A15
"

Theorems of the Theory of Commutative Ordered Fields:

COF_T01="(forall (?X ?Y ?Z) (=> (= (+ ?X ?Z) (+ ?Y ?Z)) (= ?X ?Y)))"
COF_T02="(forall (?X ?Y ?Z) (=> (= (+ ?Z ?X) (+ ?Z ?Y)) (= ?X ?Y)))"
COF_T03="(forall (?X ?Y ?Z) (=> (and (not (= ?Z 0)) (= (* ?X ?Z) (* ?Y ?Z))) (= ?X ?Y)))"
COF_T04="(forall (?X ?Y ?Z) (=> (and (not (= ?Z 0)) (= (* ?Z ?X) (* ?Z ?Y))) (= ?X ?Y)))"
COF_T05=" (= (neg 0) 0)"
COF_T06="(forall ?X (= (* ?X 0) 0))"
COF_T07="(forall (?X ?Y) (<=> (= (+ ?X (neg ?Y)) 0) (= ?X ?Y)))"
COF_T08="(forall (?X ?Y) (<=> (= ?X (neg ?Y)) (= ?Y (neg ?X))))"
COF_T09="(forall ?X (<=> (= ?X 0) (= ?X (neg 0))))"
COF_T10="(forall ?X (= (neg (neg ?X)) ?X))"
COF_T11="(forall (?X ?Y) (= (neg (+ ?X ?Y)) (+ (neg ?X) (neg ?Y))))"
COF_T12="(forall (?X ?Y) (= (* (neg ?X) ?Y) (neg (* ?X ?Y))))"
COF_T13="(forall (?X ?Y) (= (* ?X (neg ?Y)) (neg (* ?X ?Y))))"
COF_T14="(forall (?X ?Y) (= (* (neg ?X) (neg ?Y)) (* ?X ?Y)))"
COF_T15="(forall ?X (=> (not (= ?X 0)) (= (recip (neg ?X)) (neg (recip ?X)))))"
COF_T16="(forall (?X ?Y) (<=> (= (* ?X ?Y) 0) (or (= ?X 0) (= ?Y 0))))"
COF_T17="(forall (?X ?Y) (=> (not (= (* ?X ?Y) 0)) (= (recip (* ?X ?Y)) (* (recip ?X) (recip ?Y)))))"
COF_T18="(forall ?X (=< ?X ?X))"
COF_T19="(forall (?X ?Y) (=> (and (=< ?X ?Y) (=< ?Y ?X)) (= ?X ?Y)))"
COF_T20="(forall (?X ?Y ?Z) (=> (and (=< ?X ?Y) (=< ?Y ?Z)) (=< ?X ?Z)))"
COF_T21="(forall (?X ?Y) (or (=< ?X ?Y) (=< ?Y ?X)))"
COF_T22="(forall ?X (=< 0 (* ?X ?X)))"
COF_T23=" (=< 0 1)"
COF_T24="(forall (?X ?Y ?Z) (=> (=< ?X ?Y) (=< (+ ?X ?Z) (+ ?Y ?Z))))"
COF_T25="(forall (?X ?Y ?Z) (=> (=< (+ ?X ?Z) (+ ?Y ?Z)) (=< ?X ?Y)))"
COF_T26="(forall (?X ?Y ?Z ?W) (=> (and (=< ?X ?Y) (=< ?Z ?W)) (=< (+ ?X ?Z) (+ ?Y ?W))))"
COF_T27="(forall ?Y (not (=< (+ ?Y 1) ?Y)))"
COF_T28="(forall ?Y (not (=< ?Y (+ ?Y (neg 1)))))"
COF_T29="(forall (?X ?Y) (=> (=< ?X ?Y) (=< (neg ?Y) (neg ?X))))"
COF_T30="(forall (?X ?Y) (=> (=< (neg ?Y) (neg ?X)) (=< ?X ?Y)))"
COF_T31="(forall ?X (<=> (=< ?X 0) (=< 0 (neg ?X))))"
COF_T32="(forall (?X ?Y) (=> (and (=< 0 ?X) (=< ?Y 0)) (=< (* ?X ?Y) 0)))"
COF_T33="(forall (?X ?Y ?Z) (=> (and (=< ?X ?Y) (=< 0 ?Z)) (=< (* ?X ?Z) (* ?Y ?Z))))"
COF_T34="(forall (?X ?Y ?Z) (=> (and (=< ?X ?Y) (=< ?Z 0)) (=< (* ?Y ?Z) (* ?X ?Z))))"
COF_T35="(forall ?Z (=> (and (=< 0 ?Z) (not (= ?Z 0))) (=< 0 (recip ?Z))))"
COF_T36="(forall (?X ?Y ?Z) (=> (and (=< (* ?X ?Z) (* ?Y ?Z)) (=< 0 ?Z) (not (= ?Z 0))) (=< ?X ?Y)))"
COF_T37="(forall (?X ?Y ?Z) (=> (and (=< (* ?Y ?Z) (* ?X ?Z)) (=< ?Z 0) (not (= ?Z 0))) (=< ?X ?Y)))"
COF_T38="(forall (?X ?Y) (=> (= ?X ?Y) (=< ?X ?Y)))" Theorems of the Theory of Commutative Ordered Fields
COF_t01=" (=> (= (+ a c) (+ b c)) (= a b))"
COF_t02=" (=> (= (+ c a) (+ c b)) (= a b))"
COF_t03=" (=> (and (not (= c 0)) (= (* a c) (* b c))) (= a b))"
COF_t04=" (=> (and (not (= c 0)) (= (* c a) (* c b))) (= a b))"
COF_t05=" (= (neg 0) 0)"
COF_t06=" (= (* a 0) 0)"
COF_t07=" (<=> (= (+ a (neg b)) 0) (= a b))"
COF_t08=" (<=> (= a (neg b)) (= b (neg a)))"
COF_t09=" (<=> (= a 0) (= a (neg 0)))"
COF_t10=" (= (neg (neg a)) a)"
COF_t11=" (= (neg (+ a b)) (+ (neg a) (neg b)))"
COF_t12=" (= (* (neg a) b) (neg (* a b)))"
COF_t13=" (= (* a (neg b)) (neg (* a b)))"
COF_t14=" (= (* (neg a) (neg b)) (* a b))"
COF_t15=" (=> (not (= a 0)) (= (recip (neg a)) (neg (recip a))))"
COF_t16=" (<=> (= (* a b) 0) (or (= a 0) (= b 0)))"
COF_t17=" (=> (not (= (* a b) 0)) (= (recip (* a b)) (* (recip a) (recip b))))"
COF_t18=" (=< a a)"
COF_t19=" (=> (and (=< a b) (=< b a)) (= a b))"
COF_t20=" (=> (and (=< a b) (=< b c)) (=< a c))"
COF_t21=" (or (=< a b) (=< b a))"
COF_t22=" (=< 0 (* a a))"
COF_t23=" (=< 0 1)"
COF_t24=" (=> (=< a b) (=< (+ a c) (+ b c)))"
COF_t25=" (=> (=< (+ a c) (+ b c)) (=< a b))"
COF_t26=" (=> (and (=< a b) (=< c d)) (=< (+ a c) (+ b d)))"
COF_t27=" (not (=< (+ b 1) b))"
COF_t28=" (not (=< b (+ b (neg 1))))"
COF_t29=" (=> (=< a b) (=< (neg b) (neg a)))"
COF_t30=" (=> (=< (neg b) (neg a)) (=< a b))"
COF_t31=" (<=> (=< a 0) (=< 0 (neg a)))"
COF_t32=" (=> (and (=< 0 a) (=< b 0)) (=< (* a b) 0))"
COF_t33=" (=> (and (=< a b) (=< 0 c)) (=< (* a c) (* b c)))"
COF_t34=" (=> (and (=< a b) (=< c 0)) (=< (* b c) (* a c)))"
COF_t35=" (=> (and (=< 0 c) (not (= c 0))) (=< 0 (recip c)))"
COF_t36=" (=> (and (=< (* a c) (* b c)) (=< 0 c) (not (= c 0))) (=< a b))"
COF_t37=" (=> (and (=< (* b c) (* a c)) (=< c 0) (not (= c 0))) (=< a b))"
COF_t38=" (=> (= a b) (=< a b)))"