Constructive logic

A branch of mathematical logic studying arguments concerning constructive objects (cf. Constructive object) and constructions. In this sense constructive logic is broader than the logic of constructive mathematics. The most prominent difference from traditional (classical) logic consists in the absence of the law of the excluded middle $A\lor\neg A$ and the law of double negation $\neg\neg A\to A$ (cf. Double negation, law of).

When describing pure logical systems (propositional and predicate calculus), the terms "constructive", "intuitionistic", "Heyting" are often considered to be synonymous (see Heyting formal system). Constructive arithmetic sometimes refers to Heyting arithmetic and sometimes to its extension obtained by adding Markov's principle (see Constructive selection principle) and the scheme $A\leftrightarrow\exists e(erA)$, expressing the equivalence of a formula and the assertion of its realizability (see Constructive semantics). This extended system, which is sufficient for the proof of the fundamental results of constructive mathematical analysis, is not, in contrast to the Heyting one, a subsystem of classical arithmetic: The law of the excluded middle, $\forall x(A(x)\lor\neg A(x))$ is refutable in it. Systems of intuitionistic logic, including means of describing specific intuitionistic concepts, are sometimes also taken to belong to constructive logic. The general manner in which most of the systems of constructive logic reflect the specific constructive understanding of the disjunction sign $\lor$ and the existential quantifier $\exists$ is by giving an explicit realization of these connectives. The derivability of $A\lor B$ (or of $\exists xA(x)$) implies that of one of the formulas $A,B$ (or of $A(t)$ for some term $t$). In the case of applied systems (arithmetic, analysis) it is required that the formulas under consideration be closed. The majority of systems of constructive logic (including all Heyting systems) are sound with respect to the various notions of realizability, including the Kleene realizability and Gödel interpretation: All derivable formulas are realizable, and as a consequence they are true in constructive semantics. On the other hand, formal systems of constructive logic are usually incomplete with respect to natural constructive semantics. For systems containing arithmetic this follows from the Gödel incompleteness theorem.

The set of realizable predicate formulas is not recursively enumerable, therefore constructive predicate calculus is incomplete with respect to realizability, while its completeness with respect to "naive" constructive semantics would imply the intuitionistic truth of the constructive selection principle. Constructive propositional calculus is also incomplete with respect to realizability, but is complete under a certain interpretation in terms of Post systems. The arithmetic semi-formal system, which is complete with respect to the constructive semantics of Markov–Shanin, is obtained by adding to formal constructive arithmetic with the scheme $A\leftrightarrow\exists e(erA)$ and the constructive selection principle, the effective $\omega$-rule: From $A(0),A(1),\ldots,$ one can infer $\forall xA(x)$. For Heyting systems, completeness theorems have been established with respect to the model-theoretic semantics of Kripke and Beth which use "possible worlds" (these semantics are related to set-theoretic forcing), and also with respect to algebraic and topological models.

Classical formal systems usually can be embedded in the corresponding systems of constructive logic (with preservation of derivability from hypotheses) by means of the Gödel double negation (translation), defined by putting the double negation sign $\neg\neg$ in front of all subformulas. Therefore systems of arithmetic, analysis and the theory of types (cf. Types, theory of) based on classical logic can be isomorphically embedded in the corresponding systems based on constructive logic. There are systems of set theory based on constructive logic in which classical systems can be embedded. The Heyting systems are embedded in modal extensions of the classical ones by means of $\Box$-translation, that is, by putting the necessity sign $\Box$ in front of all subformulas. Here $\Box$ can be read as "provable", or, better, as "provable and true".

In certain systems of constructive logic, statements that are false in the classical interpretation, for example, the negation of the law of the excluded middle, or specific intuitionistic statements concerning choice sequences, are valid. Such systems $S$ reduce to classical systems $S^0$ by means of a suitable notion of realizability $\rho$. One has proved that $S\vdash A$ implies the existence of a $t$ such that $S^0\vdash(t\rho A)$. Moreover, if $A$ is numerical equality, then $S^0\vdash(A\leftrightarrow t\rho A)$. This implies the consistency of $S$ relative to $S^0$.

Constructive logic also studies the validity of statements in non-traditional languages that differ from the languages of predicate logic, arithmetic, analysis, etc. Along with the traditional negation $\neg$, the strong negation $\sim$ is studied, which provides the construction of a counterexample. For $\sim$ many of the laws of classical logic are valid, for example,

$$\sim(p\& q)\leftrightarrow p\lor q,\quad\sim\sim p\leftrightarrow p,$$

but the theorem on substitution of equivalents is true only in the form

$$((p\leftrightarrow q)\&(\sim p\leftrightarrow\sim q))\supset((A(p)\leftrightarrow A(q)).$$

Close to the system of strong negation are systems based on a symmetric treatment of truth and falsehood. The semantics for these specify not only the form of the constructions justifying truth but also the form of the constructions justifying falsity of the statements under consideration.

The negation-free Griss–Nelson logic seeks to avoid the use of negation and tends to consider only non-empty properties. The language of such a logic contains the connective $\to_\kappa$, where $A\to_\kappa B$ means roughly that

$$\forall x(A\supset B)\&\exists xA.$$

In the theory of constructions one studies the very rules of construction and proof that lie at the foundation of constructive mathematics. Constructions are built from primitive ones by means of a fixed collection of combinators and the operation of applying a function to an argument. Formulas are built from equalities by means of the connectives of propositional logic and the provability predicate $\pi$, where $\pi(a,x,\alpha(x))$ is to be read as "a is a proof of the fact that ax is true for all x". All classical tautologies (including the law of the excluded middle) are taken to be axioms, that is, the relation of "being a proof" is assumed to be decidable. There is a sound and faithful (complete) interpretation of the Heyting systems in the theory of constructions.

Quantifier-free systems are used in constructive logic to obtain finitistic proofs (in some sense or other) of statements or majorants of them (see Constructive semantics). Many traditional systems $S$ of constructive logic can be embedded in quantifier-free systems $S^-$ in such a way that the derivability in $S$ of $\forall x\exists yR(x,y)$, with a quantifier-free formula $R$, implies derivability in $S^-$ of the formula $R(x,\phi(x))$ for suitable $\phi$. If $S$ is the first-order arithmetic without induction, then $S^-$ is a primitive-recursive arithmetic; if $S$ is a Heyting arithmetic, then $S^-$ is a system of Gödel primitive-recursive functionals.

For formal systems of constructive logic normalization theorems have been proved: Any derivation can, by a finite number of standard transformations (reductions), be reduced to a normal form containing no "superfluous" parts (see Gentzen formal system). Normal derivations possess (fully, or in the case arithmetic or stronger systems, partially), the subformula property.

There is a connection between constructive logic and category theory. E.g., the notion of a "Cartesian-closed category" corresponds to the Gentzen propositional calculus.

Sometimes constructive logic is understood to include all logical arguments in which it is required that all objects under study be constructive, independently of the logic used.

References

[1]	S.C. Kleene, "Introduction to metamathematics" , North-Holland (1951)
[2]	A.S. Troelstra (ed.) , Metamathematical investigation of intuitionistic arithmetic and analysis , Lect. notes in math. , 344 , Springer (1973)
[3]	P.S. Novikov, "Constructive mathematical logic from a classical point of view" , Moscow (1977) (In Russian)
[4]	G. Kreisel, "Mathematical logic" , Lectures on modern mathematics , 3 , Wiley (1965) pp. 95–195

Comments

The Gödel interpretation is also called the "dialectica interpretation".

For the relation with category theory see [a1], [a2] and the references cited therein.

References

[a1]	J. Lambek, P. Scott, "Higher order categorical logic" , Cambridge Univ. Press (1986)
[a2]	P.T. Johnstone, "Topos theory" , Acad. Press (1977)