The next development of the propositional calculus is the predicate calculus. This considers the logical relationships that hold between predicate expressions, along with the quantifiers ∃x (“there is at least one x, such that …”) and ∀x (“for all x, it is the case that …”). The language of the predicate calculus consists of proper names of the form n, m, o, …; arbitrary names of the form a, b, c, …; variables of the form x, y, z, …; and predicates of the form Fn , Gn , Hn , … where n is the number of terms the predicate takes. An atomic predicate sentence consists of an n-place predicate followed by n-terms; complex, molecular formulas are then built-up compositionally via the usual logical connectives ¬, &, ∨, ⊃, ≡, along with the quantifiers ∃ and ∀. In addition to the formation rules of the propositional calculus, the predicate calculus therefore also has the following rules for the quantifiers:
If P is a wff, then ∀xP is a wff;
If P is a wff, then ∃xP is a wff.
An atomic predicate sentence is said to be closed if every variable is bound by a quantifier (otherwise the sentence is said to be open); truth for atomic predicate sentences is only defined for closed sentences.
Semantics
In the propositional calculus, truth values can be assigned directly to atomic propositions. By contrast, in the predicate calculus, an atomic sentence consists of an n-place predicate followed by the appropriate number of terms. The most basic semantic concept in the predicate calculus is therefore one of satisfaction: in the simplest case, an object a is said to satisfy an atomic sentence Fa just in case the predicate F applies to a. More formally, a model M for the predicate calculus is of the form , where D is the domain of quantification, and val is a function that maps names onto single elements of D and n-place predicates onto ordered n-tuples of D. A model M is then said to satisfy an atomic predicate sentence φ just in case it is mapped to an ordered n-tuple within the domain for which the predicate in φ holds; that is, if φ is an atomic predicate sentence of the form P(t1 , t2 , … t n ), then M ⊨ φ iff (t1 , t2 , … t n ) ∈ val[P]. Satisfaction for complex, molecular sentences can then be built up recursively via the truth tables for the logical connectives in the usual way—for example, M ⊨ (φ & ψ) iff M ⊨ φ and M ⊨ ψ. A model M satisfies an existential quantifier expression of the form ∀xφ provided there is some n-tuple within the domain for which φ holds; a model M satisfies a universal quantifier expression of the form ∃xφ just in case φ holds for every n-tuple within the domain. The two quantifiers can therefore be seen to be inter-definable: ∀xφ is equivalent to ¬∃x¬φ.
Proof Theory
The predicate calculus does not admit of proof by inspection in the way allowed by the propositional calculus; however, the system of natural deduction introduced for the propositional calculus can be easily extended with introduction and elimination rules for the two quantifiers:
Existential Quantifier Introduction and Elimination: Given φm, we can derive ∃xφx; given ∃xφx, we can derive φm (but only provided that m is a new name).
Universal Quantifier Introduction and Elimination: Given φm for every m∈D, we can derive ∃xφx; given ∃xφx, we can derive φm (but only provided that m is an old name).
The restrictions on existential quantifier elimination follow from the fact that while we know that there is some object in the domain that is φ, we don’t know which one. The restrictions on universal quantifier elimination follow from the fact that the domain of quantification might be empty.
Meta-Logical Results
As with the propositional calculus, the predicate calculus is both sound and complete. In the case of soundness, this can again be intuitively seen by the way in which the rules of derivation are constructed to fit the possible models of the language. The completeness of the predicate calculus is, however, technically demanding and was first proved in 1929 by Kurt Gödel (1906-1978).
