Logical calculus

A formalization of a meaningful logical theory. The derivable objects of a logical calculus are interpreted as statements, formed from the simplest ones (generally speaking, having subject-predicate structure) by means of propositional connectives and quantifiers. The most frequently used connectives are "not", "and", "or", "if …, then …", and the existential and universal quantifiers. Logical calculi are distinguished from arbitrary calculi (cf. Calculus) by the purely logical character of interpretations and derivation rules, and from logico-mathematical calculi (cf. Logico-mathematical calculus) by the absence in the language of symbols for specific mathematical predicates and functions (except for the symbol "=", the addition of which is interpreted as the introduction of equality and is usually supposed not to violate the logical character of the calculus). These differences have a relative character, since logical calculi remain pure formal systems, and the semantics of any possible interpretation of them must be regarded as something external, having heuristic but not conclusive value in the study of properties of the calculus.

One of the most important logical calculi is the classical predicate calculus with function symbols. The language of this calculus, apart from parentheses and the logical symbols $\neg$, $\&$, $\lor$, $\supset$, $\exists$, $\forall$, contains three potentially infinite lists: lists of object variables, predicate variables and function variables. (Each of the predicate and function variables is endowed with information about its dimension, where for predicate variables the least dimension is 1 and for function variables the least dimension is 0.) Terms are defined as follows: 1) any object variable and any function variable of dimension 0 is a term; 2) if $T_1,\ldots,T_l$ are terms and $f$ is a function variable of dimension $l$, then $f(T_1,\ldots,T_l)$ is also a term. If $T_1,\ldots,T_k$ are terms and $P$ is a predicate variable of dimension $k$, then $P(T_1,\ldots,T_k)$ is called an atomic formula. Formulas are defined as follows: 1) any atomic formula is a formula; 2) if $F$ and $G$ are formulas and $x$ is an object variable, then the expressions

$$\neg F,\quad(F\mathbin{\&}G),\quad(F\lor G),\quad(F\supset G),\quad\exists xF,\quad\forall xF$$

are also formulas. In the last two formulas all occurrences of the variable $x$ are said to be bound; occurrences of variables that are not associated with quantifiers in the process of constructing a formula are called free. A term $T$ is said to be free for $x$ in $F$ if no free occurrence of $x$ in $F$ is in a subformula of the form $\exists yG$ or $\forall yG$, where $y$ is one of the variables that occurs in $T$; $[F]_T^x$ denotes the result of substituting $T$ for all free occurrences of $x$ in $F$.

Let $x$ be an arbitrary object variable, let $A,B,C,D$ be arbitrary formulas, where $D$ does not contain $x$ freely, and let $T$ be an arbitrary term, free for $x$ in $A$. The axioms of the calculus in question are all formulas of the following 10 kinds (each of which is called an axiom scheme):

1) $(A\supset(B\supset A))$,

2) $((A\supset B)\supset((A\supset(B\supset C))\supset(A\supset C)))$,

3) $(A\supset(B\supset(A\mathbin{\&}B)))$,

4a) $((A\mathbin{\&}B)\supset A)$,

4b) $((A\mathbin{\&}B)\supset B)$,

5a) $(A\supset(A\lor B))$,

5b) $(B\supset(A\lor B))$,

6) $((A\supset C)\supset((B\supset C)\supset((A\lor B)\supset C)))$,

7) $((A\supset B)\supset((A\supset\neg B)\supset\neg A))$,

8) $(\neg\neg A\supset A)$,

9) $(\forall xA\supset[A]_T^x)$,

10) $([A]_T^x\supset\exists xA)$.

In addition, this calculus has three derivation rules: "from A and A B one can obtain B"; "from D A one can obtain D x A"; and "from A D one can obtain x A D". Provable formulas (or theorems) of the calculus in question are any formulas that can be obtained from the axioms of the calculus as a result of applying (possibly repeatedly) the given rules (see Derivation, logical).

A basic interpretation of the predicate calculus. The domain of values of object variables is a non-empty set of objects $M$, that of function variables consists of functions from $M^l$ into $M$, and that of predicate variables consists of functions from $M^k$ into $\{0,1\}$ (one of the values is interpreted as "truth", the other as "falsehood"), where the number $k$ corresponds to the dimension of the predicate variable. Now for any atomic formula, fixing the value of the predicate variables in it and the values of the object and function variables that occur in it, one can talk of the truth or falsehood of this formula. Similarly, using truth tables for propositional connectives and the usual interpretation of quantifiers (as infinite conjunctions and disjunctions), one can judge the truth of an arbitrary formula of the language in question for the chosen $M$ and the chosen values of the predicate, function and free object variables that occur in it. A formula is said to be universally valid (generally valid) if it is true for any such choice. Thus, whatever the values of a two-place predicate variable $P$ and one-place function variable $f$, from the fact that for some $x$ and any $y$ the formula $P(f(x),f(y))$ is true it follows that there is a $z$ for which $P(z,f(z))$ is true. Consequently, the formula

$$(\exists x\forall yP(f(x),f(y))\supset\exists z(P(z,f(z)))$$

is universally valid. One can prove that a formula is derivable in the calculus thus constructed if and only if it is universally valid (the so-called Gödel completeness theorem). This interpretation relies on rather complicated set-theoretic abstractions and is therefore inadmissible from the point of view of certain philosophies of mathematics and meta-mathematical theories (for example, intuitionism; finitism; constructive mathematics). In the framework of these theories one can obtain a completeness theorem by changing the semantics of the logical calculus.

Numerous logical calculi are obtained by modification of the logical calculus constructed above. Thus, the addition to the language of the symbol "=" together with the schemes

11) $(T=T)$,

12) $((T_1=T_2)\supset([A]_{T_1}^x=[A]_{T_2}^x))$

(here $A$ and $T$ are arbitrary, and $T_1$ and $T_2$ are free for $x$ in $A$) leads to the classical predicate calculus with equality. Exclusion from the language of function variables leads to the pure (or narrow or restricted) predicate calculus. The axiom schemes 1)–8) in conjunction with the first derivation rule give the classical propositional calculus; since the subject-predicate structure of inferences cannot be analyzed by the tools of predicate calculi, instead of various types of variables in the language of these calculi one usually needs only one type — propositional variables, each of which acts as an atomic formula. The rejection of scheme 8 from all the calculi mentioned above leads to minimal logical calculi, and the rejection of schemes 7 and 8 leads to positive logical calculi. Other partial logical calculi are possible, for example those obtained by fixing part of the logical symbols or part of the variables of the language (in combination with a possible reconstruction of the system of axioms) while preserving all classically-derivable formulas consisting of these symbols and variables; these are the implicative propositional calculus (the only symbol is $\supset$), the pure one-place (monadic) predicate calculus (in the language there are only object variables and one-place predicate variables), etc. More meaningful examples of partial logical calculi are the intuitionistic (constructive) calculi, which are obtained from the classical calculi mentioned above by replacing scheme 8 by the scheme

$8'$. $(A\supset(\neg A\supset B))$.

The names of logical calculi are naturally formed from the terms mentioned; thus, the schemes 1–7, $8'$, 11, 12 define intuitionistic propositional calculus with equality.

One also considers many-sorted logical calculi (and terms), where the substitution of terms of one kind for those of another is not allowed. In simple cases the domains of values of terms of different kinds are interpreted as different sets of objects (thus, convenient formalizations of plane geometry can be based on logical calculi with object variables of two kinds — "points" and "straight lines"). But one can successively consider first a calculus with a unique domain of objects, then a calculus with an additional domain of objects, namely predicates over the first domain (that is, in the second calculus one admits quantifiers with respect to the predicate variables of the first), etc. Thus there arise higher-order logical calculi (the logical calculus mentioned earlier is of the first order). The tendency to formalize logical theories with a more powerful supply of concepts leads to a number of generalizations of logical calculi. The consideration, together with "truth" and "falsehood", of various degrees of indeterminacy leads to various formalizations of many-valued logics (cf. Many-valued logic) and calculi of partial predicates. The latter are closely related to calculi of logical consequences and the strict implication calculus, which arose as a result of attempts to formalize the common use of the expression "A implies B" by removing the paradoxes of material implication and rejecting its definition in the form of a table. Modal logical calculi serve to formalize the distinction, studied in modal logic, between "necessary", "possible" and "contingent" assertions.

Together with the specification of a logical calculus in terms of axiom schemes, one often meets formulations with finitely many specific axioms, but with the addition of various rules of substitution for variables. Reformulations of a logical calculus in the form of a Gentzen formal system are convenient in many questions of proof theory.

A calculus is a completely adequately formalized theory if derivability of a formula in it is equivalent to its identical truth in the basic interpretation. The truth of derivable formulas is connected with the consistency (soundness, cf. Sound rule) of the calculus, and the derivability of all true formulas is connected with its completeness. All logical calculi mentioned above are sound, and many of them are complete in one sense or another (see Gödel completeness theorem). An important property of logical calculi is decidability (see Decision problem): almost-all propositional calculi that have been constructed are decidable; on the other hand, all the predicate calculi mentioned above (except the monadic one) are undecidable. Nevertheless, there are algorithms for undecidable logical calculi that for each derivable formula establish its derivability, but for certain underivable formulas they need not terminate.

References

[1]	D. Hilbert, P. Bernays, "Grundlagen der Mathematik" , 1 , Springer (1968)
[2]	S.C. Kleene, "Introduction to metamathematics" , North-Holland (1951)
[3]	P.S. Novikov, "Elements of mathematical logic" , Oliver & Boyd and Acad. Press (1964) (Translated from Russian)
[4]	A. Church, "Introduction to mathematical logic" , 1 , Princeton Univ. Press (1956)
[5]	, Mathematical theory of logical deduction , Moscow (1967) (In Russian; translated from English) (Collection of translations)
[a1]	S.C. Kleene, "Mathematical logic" , Wiley (1967)
[a2]	G. Kreisel, J.L. Krivine, "Elements of mathematical logic" , North-Holland (1967) (Translated from French)
[a3]	R. Wójcicki, "Theory of logical calculi" , Kluwer (1988) pp. 12