Home > First-order predicate calculus
6.2 Inference rule
The inference rule called Generalization is characteristic of predicate calculus. It can be stated as
-
where Z(x) is supposed to stand for an already-proven theorem of predicate calculus. The predicate letter Z can be replaced by any other predicate letter.
Notice that Generalization is analogous to the Necessitation Rule of modal logic, which is
- .
7 Case study: first-order Peano axioms
The Peano axioms for the natural numbers are sometimes formulated as second-order statements (the induction axiom talks about all "properties" or all "sets of numbers"), but this is not necessary if one is willing to allow infinitely many first-order axioms. A first-order version of the Peano axioms follows.
We are using the object constants 0 and 1, the function constants + and *, and the predicate constant =. Here are the axioms:
-
- i.e.: forAll x, not (0 = x + 1)
- i.e.: no number has 0 as its successor
-
- i.e.: forAll x, forAll y, not(x=y) implies not(x + 1 = y + 1)
- i.e.: if x ≠ y, then x+1 ≠ y+1
-
- i.e.: forAll x, x + 0 = x
-
- i.e.: forAll x, forAll y, x + (y + 1) = (x + y) + 1
- i.e.: for all x and y, x + (y + 1) = (x + y) + 1
-
- i.e.: forAll x, x * 0 = 0
-
- i.e.: forAll x, forAll y, x * (y + 1) = x * y + x
- i.e.: for all x and y, x * (y + 1) = x * y + x
- This is an axiom scheme consisting of infinitely many axioms. If P(x) is any formula involving the constants 0, 1, +, *, = and a single free variable x, then the following formula is an axiom:
- i.e.: ( P(0) and (forAll x, ( P(x) implies P(x + 1) ) ) ) implies (forAll x, P(x) )
- i.e.: if something is true for 0, and from its being true for x it follows that it is also true for x + 1, then it is true for all x (induction)
Axioms 1, 2 and 7 are the traditional Peano axioms while axioms 3-6 serve to define addition and multiplication. If one omits the function constant * and axioms 5 and 6 and allows in scheme 7 only formulas without *, then one gets the very interesting Presburger arithmetic.
8 References
