Constructive semantics

The collection of methods for understanding statements in constructive mathematics. The need for a special semantics is caused by the difference in the general principles underlying traditional (classical) and constructive mathematics (in what follows the latter term refers mainly to the approach developed in the Soviet school of constructive mathematics). The main attention of constructive semantics is given to statements concerning constructive objects (cf. Constructive object) in first-order languages; i.e., essentially arithmetic statements (see Arithmetic, formal). The principal difference from traditional semantics in the understanding of the disjunction $ A _ {0} \lor A _ {1} $( and of statements concerning the existence $ \exists x A ( x) $) were stated by L.E.J. Brouwer. The constructive justification of such statements requires a solution of the problem: Find a number $ i \leq 1 $ such that $ A _ {1} $ is true (or: Find a number $ n $ such that $ A ( n) $). The general principles of description of problems corresponding to more complex formulas were outlined by A. Heyting and A.N. Kolmogorov. A precise formulation (which became possible after the appearance of the mathematical definition of an algorithm) was given by S.C. Kleene in the form of the notion of realization of a closed arithmetic formula (see Recursive realizability). A realization of a true equality $ t = r $ is a fixed constant; for example, the number $ 0 $, while a false equation has no realization. A realization of a conjunction $ A \& B $ is a pair $ \langle a , b \rangle $ where $ a $ is a realization of $ A $ and $ b $ is a realization of $ B $. A realization of a disjunction $ A _ {0} \lor A _ {1} $ is a pair $ \langle i , a \rangle $, where $ i = 0 , 1 $ and $ a $ is a realization of $ A _ {i} $. A realization of the statement $ \exists x A ( x) $ is a pair $ \langle n , a \rangle $, where $ n $ is a number and $ a $ is a realization of $ A ( n) $. A realization of $ \forall x A ( x) $ is a general method $ f $ that gives for each natural number $ n $ a realization $ f ( n) $ of $ A ( n) $. A realization of $ A \supset B $ is a general method $ f $ that, for each realization $ a $ of $ A $, gives a realization $ f ( a) $ of $ B $( and which need not be defined for arguments $ a $ that are not realizations of $ A $). Here, a general method is understood to be an algorithm (a partial recursive function). By using an encoding of algorithms by numbers, one can write the condition "the number e is a realization of the formula A" in the form of an arithmetic formula $ ( e r A ) $ that does not contain the disjunction $ \lor $ and contains the existence quantifier $ \exists $ only in a natural way, in front of equalities. Such formulas are called almost normal or almost negative. The statement $ \exists e ( e r A ) $( read "A is realizable" ) may serve as a constructive interpretation of $ A $. Under this interpretation the law of the excluded middle, $ \forall x ( A ( x) \lor \neg A ( x) ) $, is refuted, for example, for $ A ( x) = \exists y T ( x , x , y ) $, where $ T ( e , x , y ) $ means that the (encoded) algorithm $ e $ completes its processing on the argument $ x $ after $ y $ steps. The law of double negation, $ \forall x ( \neg \neg B ( x) \supset B ( x) ) $, is also refuted, for example, for $ B ( x) = A ( x) \lor \neg A ( x) $. The above definition associates to each statement $ A $ a constructive interpretation (to find a realization), even if $ A $ does not contain $ \lor , \exists $. The algorithm giving this constructive interpretation, put forward by N.A. Shanin, does not change formulas without $ \lor , \exists $( normal formulas) and is equivalent to realizability in formal intuitionistic arithmetic with quantifier-free induction. Arbitrary formulas can be reduced to almost-normal ones, since a justification of $ \exists x A ( x) $ consists in producing a number $ n $ and a justification of $ A ( n) $. Constructive semantics for almost-normal formulas is defined in different ways by different authors; however, in no case does one obtain such a significant departure from the classical concept as for formulas containing $ \lor $ and a non-trivial $ \exists $.

A.A. Markov defines truth for almost-normal formulas by means of derivability according to the usual laws for the logical connectives plus the effective $ \omega $- rule: If there is a general method enabling one to establish for any $ n $ the derivability of $ A ( n) $ from a statement $ K $, then $ \forall x A ( x) $ is derivable from $ K $. Truth is defined step by step. The language $ L _ \omega $ consisting of all almost-normal formulas is divided into layers $ L _ {1} , L _ {2} ,\dots $; the language $ L _ {1} $ consists of formulas without $ \supset , \forall $; the language $ L _ {n+} 1 $, $ n \geq 1 $, includes $ L _ {n} $ and the formulas that can be obtained from $ L _ {n} $ by a single application of implication and any number of applications of $ \forall , \& $. Truth for formulas in $ L _ {1} $ is defined as derivability according to the usual rules for $ \& $, $ \exists $, $ \lor $. Truth for formulas in $ L _ {2} $ is defined in terms of admissibility of the appropriate rule. For example, the truth of $ \exists x R ( x) \supset \exists y T ( y) $ means the existence of an algorithm $ \phi $ such that $ R ( n) \supset T ( \phi ( n) ) $ for any number $ n $. For formulas in $ L _ {n+} 1 $ for $ n > 1 $, truth of conjunctions and $ \forall $- formulas is defined in the ordinary way in terms of truth of their components, while truth of an implication $ A \supset B $ means derivability of $ B $ from $ A $ according to certain rules $ S _ {n} $ about which it has already been proved that they preserve the truth of formulas in $ L _ {n} $. The systems $ S _ {n} $ contain the $ \omega $- rule and, as axioms, all true formulas in $ L _ {n} $. The notion of derivability in $ S _ {n} $ is introduced by a generalized inductive definition, and a corresponding induction principle is applied for the proof of meta-theorems. The admissibility of the rule $ A \supset \neg \neg \exists x R \vdash A \supset \exists x R $ is proved by induction over $ S _ {2} $- derivation. It is included in $ S _ {3} $ and gives Markov's principle $ \neg \neg \exists x R \supset \exists x R $. The systems $ S _ {n+} 3 $, $ n \geq 1 $, consist of the ordinary rules for the connectives, including the $ \omega $- rule. It turns out that an almost-normal formula $ A $ is true in the sense of Markov if and only if the primitive recursive cut-free proof search tree $ T _ {A} $ for $ A $( with the $ \omega $- rule and the Markov principle) is a derivation in the sense of the inductive definition. This is equivalent (in the framework of classical mathematics) to the classical truth of $ A $.

In the majorizing semantics of Shanin a transfinite hierarchy $ \{ A ^ \alpha \} $ of formulas of simple structure is defined for every almost-normal formula $ A $, such that $ A ^ \alpha \supset A $ is provable in a suitable formal system. The formula $ A ^ \alpha $ is called a majorant for $ A $, and $ A $ is called a true formula of rank $ \alpha $, if $ A ^ \alpha $ is true. The accuracy of the approximation increases with increasing $ \alpha $: $ \alpha < \beta \supset ( A ^ \alpha \supset A ^ \beta ) $. Up to technical details, a formula $ A ^ \alpha $ is constructed by $ \alpha $- fold moving quantifiers forward according to the equivalence

$$ \neg \neg ( B \lor \neg \neg \exists u \ \forall v C ( u , v ) ) \aHB $$

$$ \aHB \ \exists \overline{u}\; \ \forall \overline{v}\; \neg \neg ( B \lor \neg \neg \exists u \forall v C ( u , v ) \lor C ( \overline{u}\; , \overline{v}\; ) ) , $$

and by fusing the string of quantifiers according to the algorithm for constructive interpretation. This gives the equivalence

$$ A \aHB \exists u \ \forall v \neg \neg ( \neg \neg \exists w \ C _ \alpha \lor D _ \alpha ) , $$

which is provable in an arithmetic with transfinite induction up to $ \alpha $, containing a quantifier-free formula $ C _ \alpha $, so that

$$ A ^ \alpha = \exists u \forall v \exists w \ C _ \alpha ( u , v , w ) $$

turns out to be a majorant for $ A $. The statement $ A ^ \alpha $ turns out to be equivalent, up to some technical details, to the assertion of the existence of a derivation of height less that $ \alpha $ for the original formula using the $ \omega $- rule. In this sense, the majorizing semantics is equivalent to the stepwise semantics of Markov. After fixing some class $ \Theta $ of general recursive functions (for example, the class of all functions defined by recursion up to $ \alpha $), majorants of even simpler structure are defined:

$$ \exists u \forall v \ C _ \alpha ( u , v ,\ \phi ( v) ) \ \ \textrm{ for } \phi \in \Theta . $$

If $ K $ is a quantifier-free calculus for the class $ \Theta $, then $ K $- truth of the formula $ \exists u \forall v C ( u , v ) $ is defined as derivability of $ C ( t , v ) $ with variable $ v $ and a constant term $ t $. If $ K $ is the standard equation calculus for functions defined by recursion up to $ \alpha $, then the $ K $- true formulas turns out to be those that are derivable in formal intuitionistic arithmetic supplemented by Markov's principle, the equivalences defining the algorithm for constructive interpretation, and the rule of induction up to ordinal numbers $ \beta $ for which $ \epsilon ( \beta ) \leq \alpha $, where $ \epsilon ( \beta ) $ is the first $ \epsilon $- number greater than $ \beta $. In particular, $ \alpha = \epsilon _ {0} $ for $ \beta = \omega $, that is, for ordinary induction.

The justification at the quantifier-free level ( $ K $- truth) relates to the desire to remain as far as possible within the realms of finitism, that is, quantifier-free language and the corresponding logical means. Related to this is the aim of restricting the value of $ \alpha $. For the greater part of constructive analysis "in practice" finite $ \alpha $' s suffice (including in the theorem on the continuity of effective operators).

References

[1]	A.A. Markov, "An attempt to construct the logic of constructive mathematics" , Investigations on the theory of algorithms and mathematical logic , 2 , Moscow (1976) pp. 3–31 (In Russian)
[2]	N.A. Shanin, "A hierarchy of ways of understanding judgements in constructive mathematics" Trudy Mat. Inst. Steklov. , 129 (1973) pp. 203–266 (In Russian)
[3]	S.C. Kleene, "Introduction to metamathematics" , North-Holland (1951)

Comments

Realizability is just one of the many semantics for constructive or intuitionistic logic and mathematics. An introductory account is given in [a1]; more on realizability can found in [a2]. Other semantics include those using sheaf theory and topos theory (cf. Topos, [a3]).

References

[a1]	M.A.E. Dummett, "Elements of intuitionism" , Oxford Univ. Press (1977)
[a2]	A.S. Troelstra (ed.) , Mathematical investigations of intuitionistic arithmetic and analysis , Lect. notes in math. , 344 , Springer (1973)
[a3]	P.T. Johnstone, "Topos theory" , Acad. Press (1977)