First-order predicate calculus : Predicate logic 

First-order predicate calculus or first-order logic is a theory in symbolic logic that formalizes quantified statements such as "there exists an object such that..." or "for all objects, it is the case that...".

First-order logic is distinguished from higher-order logic[?] in that it doesn't allow statements such as "for every property, it is the case that..." or "there exists a set of objects such that...".

Nevertheless, first-order logic is strong enough to formalize all of set theory and thereby virtually all of mathematics. It is the classical logical theory underlying mathematics. It is a stronger theory than sentential logic[?], but a weaker theory than arithmetic, set theory, or second-order logic[?].

Like any logical theory, first-order calculus consists of

• a specification of how to construct syntactically correct statements (the well-formed formulas)
• a set of axioms, each axiom being a well-formed formula itself
• a set of inference rules which allow one to prove theorems from axioms or earlier proven theorems.

There are two types of axioms: the logical axioms which embody the general truths about proper reasoning involving quantified statements, and the axioms describing the subject matter at hand, for instance axioms describing sets in set theory or axioms describing numbers in arithmetic.

While the set of inference rules in first-order calculus is finite, the set of axioms may very well be and often is infinite. However we require that there is a general algorithm which can decide for a given well-formed formula whether it is an axiom or not. Furthermore, there should be an algorithm which can decide whether a given application of an inference rule is correct or not.

The well-formed formulas contain

• variables such as x, y, ... which are place holders for objects of the domain under consideration
• object constants such as 0, 1 or the empty set ø which stand for fixed individual objects in our domain
• predicate constants such < (lessThan), ∈ (isIn), '=' (equals) which stand for fixed relations between or properties of our objects. These are also called first-order predicates to distinguish them from predicates that talk about predicates.
• function constants such as +, * which stand for fixed functions taking objects as arguments and returning objects as values
• logical connectives such as ∧ (and), ∨ (or), ⇒ (implies), ¬ (not), ∃ (thereExists existential quantifier) and ∀ (forAll or universal quantifier). All of these except for the last two are also used in propositional logic.

The object, predicate and function constants will typically depend on the particular domain we are talking about.

Instead of giving the lengthy definition of well-formed formulas, we will simply look at some examples from arithmetic together with their ordinary interpretation. Our domain here is the set of natural numbers:

∀ x ∃ y : y > x

(ie: forAll x thereExists y suchThat y greaterThan x )

∃ y ∀ x : y > x

(ie: thereExists y forAll x suchThat y greaterThan x )

There exists a number y which is bigger than every number x. That's not true.

∀ x ( (∃ y : 6 * y=x ) ⇒ (∃ y : 3 * y=x ) )

(ie: forAll x ( thereExists y suchThat 6*y=x) implies (thereExists y suchThat 3*y=x) )

If a number x is divisible by 6, then it is also divisible by 3. True.

∃ x : ¬ ∃ y : y < x

(ie: thereExists x suchThat (not ThereExists y suchThat y < x ) )

There exists a number x such that there doesn't exist a smaller number y. True (take x=0).

Now one would have to write down 15 logical axioms and 2 inference rules to completely specify the first-order calculus. How can one be sure that those axioms and rules are enough? This is the subject of Gödel's completeness theorem: if you start out with some subject matter axioms and you look at a certain statement, then it is possible to prove that statement using only the subject matter axioms, the 15 logical axioms and the two inference rules if and only if the statement is true in every domain in which the subject matter axioms are true.

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 isn't 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:

1. ∀ x : ¬ (0 = x + 1)
   • i.e.: forAll x suchThat not (0 = x + 1)
   • i.e.: no number has 0 as its sucessor
2. ∀ x ∀ y : ¬ (x = y) ⇒ ¬ (x + 1 = y + 1)
   • i.e.: forAll x forAll y suchThat not(x=y) implies not(x + 1 = y + 1)
   • i.e.: if x ≠ y, then x+1 ≠ y+1
3. ∀ x : x + 0 = x
   • i.e.: forAll x suchThat x + 0 = x
   • i.e.: for all x, x + 0 = x
4. ∀ x ∀ y : (x + y) + 1 = x + (y + 1)
   • i.e.: forAll x forAll y suchThat (x + y) + 1 = x + (y + 1)
   • i.e.: for all x and y, (x + y) + 1 = x + (y + 1)
5. ∀ x : x * 0 = 0
   • i.e.: forAll x suchThat x * 0 = 0
   • i.e.: for all x, x * 0 = 0
6. ∀ x ∀ y : x * (y + 1) = x * y + x
   • i.e.: forAll x forAll y suchThat x * (y + 1) = x * y + x
   • i.e.: for all x and y, x * (y + 1) = x * y + x
7. 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:   ( P(0) ∧ ∀ x : P(x) ⇒ P(x + 1) ) ⇒ ∀ x : P(x)
   • i.e.: ( P(0) and (forAll x suchThat ( P(x) implies P(x + 1) ) ) ) implies (forAll x suchThat 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.

• Introduction to mathematical logic (http://www.ltn.lv/~podnieks/)
• Metamath (http://us.metamath.org/index.html): a project to construct mathematics using an axiomatic system based on propositional calculus, predicate calculus, and set theory