Predicate calculus

A formal axiomatic theory; a calculus intended for the description of logical laws (cf. Logical law) that are true for any non-empty domain of objects with arbitrary predicates (i.e. properties and relations) given on these objects.

In order to formulate the predicate calculus one must first fix an exact logico-mathematical language $\Omega$. In the most common case of single-sorted first-order languages, such a language contains predicate variables $x,y,z,\dots,$ function symbols $f,g,h,\dots$ with a varying number of argument places, and predicate symbols (predicate letters) $P,Q,R,\dots,$ also with a varying number of argument places. From the variables and function symbols one constructs the terms of the language, which are names of objects of the theory to be studied. Further, if $P$ is an $n$-place predicate symbol of $\Omega$, $n\geq0$, and if $t_1,\dots,t_n$ are terms, then $P(t_1,\dots,t_n)$ is, by definition, an atomic (elementary) formula of $\Omega$. The content of $P(t_1,\dots,t_n)$ is that the statement according to which $t_1,\dots,t_n$ are related through the relation $P$ is true.

By means of propositional connectives (cf. Propositional connective) and quantifiers (cf. Quantifier) one constructs formulas of the language from the atomic formulas. The common choice of connectives and quantifiers in classical and intuitionistic predicate calculus is: $\&$ or $\land$ (conjunction, "and"), $\lor$ (disjunction, non-exclusive "or"), $\to$ or $\supset$ (implication, "implies" , "if … then"), $\neg$ (negation, "not"), $\forall$ (the universal quantifier, "for all"), and $\exists$ (the existential quantifier, "there exists"). The corresponding non-atomic formulas of these calculi have the form $(\phi\land\psi)$, $(\phi\lor\psi)$, $(\phi\supset\psi)$, $\neg\phi$, $\forall x\phi$, $\exists x\phi$. An occurrence of a variable $x$ in a formula $\phi$ is called bound if $x$ occurs in a part of $\phi$ of the form $\exists x\psi$ or $\forall x\psi$. All other occurrences of $x$ in $\phi$ are called free. A variable $x$ is called a parameter of $\phi$ if there is at least one free occurrence of $x$ in $\phi$. Intuitively speaking, a formula with parameters expresses a condition that is turned into a concrete statement if a model of the calculus is given, i.e. some non-empty domain of objects of study is chosen and predicates (i.e. relations on the domains of the objects) are ascribed to the predicate symbols, while the parameters are ascribed definite objects as values.

A predicate calculus is specified by means of axioms and derivation rules. E.g., one of the usual formulations of classical predicate calculus contains the axioms

1) $(\phi\supset(\psi\supset\phi))$;

2) $((\phi\supset(\psi\supset\eta))\supset((\phi\supset\psi)\supset(\phi\supset\eta)))$;

3) $((\phi\land\psi)\supset\phi)$;

4) $((\phi\land\psi)\supset\psi)$;

5) $(\phi\supset(\psi\supset(\phi\land\psi)))$;

6) $((\phi\supset\eta)\supset((\psi\supset\eta)\supset((\phi\lor\psi)\supset\eta)))$;

7) $(\phi\supset(\phi\lor\psi))$;

8) $(\psi\supset(\phi\lor\psi))$;

9) $(\neg\phi\supset(\phi\supset\psi))$;

10) $((\phi\supset\psi)\supset((\phi\supset\neg\psi)\supset\neg\phi))$;

11) $(\phi\lor\neg\phi)$;

12) $(\forall x\phi\supset\phi(x|t))$;

13) $(\phi(x|t)\supset\exists x\phi)$;

14) $(\forall x(\phi\supset\psi)\supset(\phi\supset\forall x\psi))$;

15) $(\forall x(\psi\supset\phi)\supset(\exists x\psi\supset\phi))$. Here, $\phi$, $\psi$ and $\eta$ denote arbitrary formulas of $\Omega$, so that each of 1)–15) represents an axiom scheme generating a concrete axiom of the calculus for a concrete choice of $\phi$, $\psi$ and $\eta$. Further, in 14) and 15) it is assumed that $x$ is not a parameter of $\phi$; in 12) and 13) $\phi(x|t)$ denotes the result of simultaneous substitution of all free occurrences of $x$ in $\phi$ by the term $t$. (Moreover, if $t$ shows up instead of $x$ in a part of $\phi$ of the form $\exists y\psi$ or $\forall y\psi$, where $y$ occurs in $t$, then one must additionally replace all bound occurrences of $y$ in this part by a variable not occurring in $\phi$; this is done in order not to distort the meaning of $\phi$ when replacing $x$ with $t$; such a distortion of meaning is called collision of variables.)

Further, predicate calculus contains two derivation rules: a) if formulas $\phi$ and $(\phi\supset\psi)$ have been derived, then a derivation for $\psi$ exists (the rule of modus ponens); and b) if a formula $\phi$ has been derived and if $x$ is a variable, then a derivation for $\forall x\phi$ exists (the rule of generalization).

The interpretation of the logical connectives in predicate calculus is the same as in propositional calculus. In connection with the interpretation of quantifiers, it should be noted that in classical predicate calculus they are treated with the use of the actual infinity. If an interpretation of the language is given, then every formula not containing parameters receives the value "true" or "false". A formula is called classically (universally) valid if in any interpretation and for all values ascribed to the parameters, it has the value "true". By virtue of the Gödel completeness theorem, the classically-valid formulas are exactly those which can be derived in classical predicate calculus. This theorem is an exact expression of the idea of a formalization of classical logic: In classical predicate calculus all logical laws that are true in all models can be derived.

Intuitionistic predicate calculus differs from classical predicate calculus in that axiom scheme 11) does not occur in its list of axiom schemes. The difference between the two calculi is reflected in the way the logical connectives and quantifiers are understood. In intuitionistic predicate calculus this understanding is within the framework of intuitionism. The question of the completeness of intuitionistic predicate calculus is much more complicated and admits different solutions, depending on the particular semantics; but here too one can develop a very substantial theory of models, analogous to classical model theory (cf. Kripke models; Realizability).

One also uses other formulations of predicate calculus, the most important of which, from the point of view of proof theory, are the calculus of natural deduction (cf. Natural logical deduction) and the sequent calculi (cf. Sequent calculus).

Predicate calculus is a very common basis for the construction of logical calculi intended for the description of fragments of some concrete mathematical theory. E.g., if one wishes to describe some class of true statements of set theory, then one can construct logical calculi in terms of set theory in which, apart from the axioms and derivation rules of classical predicate calculus (the logical postulates), additional non-logical axioms will figure, describing properties of sets. The axiom of choice is a typical example of a non-logical axiom in set theory.

Predicate calculus is sometimes called narrow predicate calculus, first-order predicate calculus or first-order functional calculus, as distinct from calculi containing quantifiers over predicates and corresponding convolution axioms, expressing the existence of the respective predicates. Such a kind of calculus, which already does not have a pure logical character, is often called a higher-order predicate calculus. The theory of types is an example of such a calculus (cf. Types, theory of). Besides classical and intuitionistic predicate calculus there are other types of logical systems describing logical laws which can be expressed by other logical tools or from other methodological positions. Amongst these are modal predicate calculus, inductive logic, etc.

References

[1]	D. Hilbert, P. Bernays, "Grundlagen der Mathematik" , 1–2 , Springer (1934–1939)
[2]	S.C. Kleene, "Introduction to metamathematics" , North-Holland (1951)
[3]	P.S. Novikov, "Elements of mathematical logic" , Oliver & Boyd (1964) (Translated from Russian)
[4]	G. Takeuti, "Proof theory" , North-Holland (1975)

References

[a1]	J.L. Bell, M. Machover, "A course in mathematical logic" , North-Holland (1977)
[a2]	W.S. Hatcher, "Foundations of mathematics" , Saunders (1968)