Namespaces
Variants
Actions

Difference between revisions of "Constructive semantics"

From Encyclopedia of Mathematics
Jump to: navigation, search
(Importing text file)
 
m (tex encoded by computer)
Line 1: Line 1:
The collection of methods for understanding statements in [[Constructive mathematics|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|Constructive object]]) in first-order languages; i.e., essentially arithmetic statements (see [[Arithmetic, formal|Arithmetic, formal]]). The principal difference from traditional semantics in the understanding of the disjunction <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c0254201.png" /> (and of statements concerning the existence <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c0254202.png" />) were stated by L.E.J. Brouwer. The constructive justification of such statements requires a solution of the problem: Find a number <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c0254203.png" /> such that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c0254204.png" /> is true (or: Find a number <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c0254205.png" /> such that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c0254206.png" />). 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|algorithm]]) was given by S.C. Kleene in the form of the notion of realization of a closed arithmetic formula (see [[Recursive realizability|Recursive realizability]]). A realization of a true equality <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c0254207.png" /> is a fixed constant; for example, the number <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c0254208.png" />, while a false equation has no realization. A realization of a conjunction <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c0254209.png" /> is a pair <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542010.png" /> where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542011.png" /> is a realization of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542012.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542013.png" /> is a realization of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542014.png" />. A realization of a disjunction <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542015.png" /> is a pair <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542016.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542017.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542018.png" /> is a realization of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542019.png" />. A realization of the statement <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542020.png" /> is a pair <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542021.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542022.png" /> is a number and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542023.png" /> is a realization of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542024.png" />. A realization of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542025.png" /> is a general method <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542026.png" /> that gives for each natural number <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542027.png" /> a realization <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542028.png" /> of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542029.png" />. A realization of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542030.png" /> is a general method <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542031.png" /> that, for each realization <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542032.png" /> of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542033.png" />, gives a realization <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542034.png" /> of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542035.png" /> (and which need not be defined for arguments <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542036.png" /> that are not realizations of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542037.png" />). 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542038.png" /> that does not contain the disjunction <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542039.png" /> and contains the existence quantifier <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542040.png" /> only in a natural way, in front of equalities. Such formulas are called almost normal or almost negative. The statement <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542041.png" /> (read  "A is realizable" ) may serve as a constructive interpretation of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542042.png" />. Under this interpretation the law of the excluded middle, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542043.png" />, is refuted, for example, for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542044.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542045.png" /> means that the (encoded) algorithm <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542046.png" /> completes its processing on the argument <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542047.png" /> after <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542048.png" /> steps. The law of double negation, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542049.png" />, is also refuted, for example, for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542050.png" />. The above definition associates to each statement <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542051.png" /> a constructive interpretation (to find a realization), even if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542052.png" /> does not contain <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542053.png" />. The algorithm giving this constructive interpretation, put forward by N.A. Shanin, does not change formulas without <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542054.png" /> (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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542055.png" /> consists in producing a number <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542056.png" /> and a justification of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542057.png" />. 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542058.png" /> and a non-trivial <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542059.png" />.
+
<!--
 +
c0254201.png
 +
$#A+1 = 152 n = 0
 +
$#C+1 = 152 : ~/encyclopedia/old_files/data/C025/C.0205420 Constructive semantics
 +
Automatically converted into TeX, above some diagnostics.
 +
Please remove this comment and the {{TEX|auto}} line below,
 +
if TeX found to be correct.
 +
-->
  
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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542061.png" />-rule: If there is a general method enabling one to establish for any <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542062.png" /> the derivability of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542063.png" /> from a statement <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542064.png" />, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542065.png" /> is derivable from <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542066.png" />. Truth is defined step by step. The language <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542067.png" /> consisting of all almost-normal formulas is divided into layers <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542068.png" />; the language <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542069.png" /> consists of formulas without <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542070.png" />; the language <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542071.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542072.png" />, includes <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542073.png" /> and the formulas that can be obtained from <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542074.png" /> by a single application of implication and any number of applications of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542075.png" />. Truth for formulas in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542076.png" /> is defined as derivability according to the usual rules for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542077.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542078.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542079.png" />. Truth for formulas in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542080.png" /> is defined in terms of admissibility of the appropriate rule. For example, the truth of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542081.png" /> means the existence of an algorithm <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542082.png" /> such that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542083.png" /> for any number <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542084.png" />. For formulas in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542085.png" /> for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542086.png" />, truth of conjunctions and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542087.png" />-formulas is defined in the ordinary way in terms of truth of their components, while truth of an implication <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542088.png" /> means derivability of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542089.png" /> from <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542090.png" /> according to certain rules <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542091.png" /> about which it has already been proved that they preserve the truth of formulas in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542092.png" />. The systems <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542093.png" /> contain the <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542094.png" />-rule and, as axioms, all true formulas in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542095.png" />. The notion of derivability in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542096.png" /> 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542097.png" /> is proved by induction over <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542098.png" />-derivation. It is included in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c02542099.png" /> and gives Markov's principle <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c025420100.png" />. The systems <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c025420101.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c025420102.png" />, consist of the ordinary rules for the connectives, including the <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c025420103.png" />-rule. It turns out that an almost-normal formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c025420104.png" /> is true in the sense of Markov if and only if the primitive recursive cut-free proof search tree <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c025420105.png" /> for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c025420106.png" /> (with the <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c025420107.png" />-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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c025420108.png" />.
+
{{TEX|auto}}
 +
{{TEX|done}}
  
In the majorizing semantics of Shanin a transfinite hierarchy <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c025420109.png" /> of formulas of simple structure is defined for every almost-normal formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c025420110.png" />, such that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c025420111.png" /> is provable in a suitable formal system. The formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c025420112.png" /> is called a majorant for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c025420113.png" />, and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c025420114.png" /> is called a true formula of rank <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c025420116.png" />, if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c025420117.png" /> is true. The accuracy of the approximation increases with increasing <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c025420118.png" />: <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c025420119.png" />. Up to technical details, a formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c025420120.png" /> is constructed by <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c025420121.png" />-fold moving quantifiers forward according to the equivalence
+
The collection of methods for understanding statements in [[Constructive mathematics|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|Constructive object]]) in first-order languages; i.e., essentially arithmetic statements (see [[Arithmetic, formal|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|algorithm]]) was given by S.C. Kleene in the form of the notion of realization of a closed arithmetic formula (see [[Recursive realizability|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 $.
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c025420122.png" /></td> </tr></table>
+
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 $.
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c025420123.png" /></td> </tr></table>
+
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
 
and by fusing the string of quantifiers according to the algorithm for constructive interpretation. This gives the equivalence
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c025420124.png" /></td> </tr></table>
+
$$
 +
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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c025420125.png" />, containing a quantifier-free formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c025420126.png" />, so that
+
which is provable in an arithmetic with transfinite induction up to $  \alpha $,  
 +
containing a quantifier-free formula $  C _  \alpha  $,  
 +
so that
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c025420127.png" /></td> </tr></table>
+
$$
 +
A  ^  \alpha  = \exists
 +
u  \forall v  \exists w \
 +
C _  \alpha  ( u , v , w )
 +
$$
  
turns out to be a majorant for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c025420128.png" />. The statement <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c025420129.png" /> turns out to be equivalent, up to some technical details, to the assertion of the existence of a derivation of height less that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c025420130.png" /> for the original formula using the <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c025420131.png" />-rule. In this sense, the majorizing semantics is equivalent to the stepwise semantics of Markov. After fixing some class <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c025420132.png" /> of general recursive functions (for example, the class of all functions defined by recursion up to <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c025420133.png" />), majorants of even simpler structure are defined:
+
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:
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c025420134.png" /></td> </tr></table>
+
$$
 +
\exists u  \forall v \
 +
C _  \alpha  ( u , v ,\
 +
\phi ( v) ) \ \
 +
\textrm{ for }  \phi \in \Theta .
 +
$$
  
If <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c025420135.png" /> is a quantifier-free calculus for the class <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c025420136.png" />, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c025420137.png" />-truth of the formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c025420138.png" /> is defined as derivability of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c025420139.png" /> with variable <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c025420140.png" /> and a constant term <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c025420141.png" />. If <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c025420142.png" /> is the standard equation calculus for functions defined by recursion up to <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c025420143.png" />, then the <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c025420144.png" />-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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c025420145.png" /> for which <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c025420146.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c025420147.png" /> is the first <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c025420148.png" />-number greater than <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c025420149.png" />. In particular, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c025420150.png" /> for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c025420151.png" />, that is, for ordinary induction.
+
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 (<img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c025420152.png" />-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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c025420153.png" />. For the greater part of constructive analysis  "in practice"  finite <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/c/c025/c025420/c025420154.png" />'s suffice (including in the theorem on the continuity of effective operators).
+
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====
 
====References====
 
<table><TR><TD valign="top">[1]</TD> <TD valign="top">  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)</TD></TR><TR><TD valign="top">[2]</TD> <TD valign="top">  N.A. Shanin,  "A hierarchy of ways of understanding judgements in constructive mathematics"  ''Trudy Mat. Inst. Steklov.'' , '''129'''  (1973)  pp. 203–266  (In Russian)</TD></TR><TR><TD valign="top">[3]</TD> <TD valign="top">  S.C. Kleene,  "Introduction to metamathematics" , North-Holland  (1951)</TD></TR></table>
 
<table><TR><TD valign="top">[1]</TD> <TD valign="top">  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)</TD></TR><TR><TD valign="top">[2]</TD> <TD valign="top">  N.A. Shanin,  "A hierarchy of ways of understanding judgements in constructive mathematics"  ''Trudy Mat. Inst. Steklov.'' , '''129'''  (1973)  pp. 203–266  (In Russian)</TD></TR><TR><TD valign="top">[3]</TD> <TD valign="top">  S.C. Kleene,  "Introduction to metamathematics" , North-Holland  (1951)</TD></TR></table>
 
 
  
 
====Comments====
 
====Comments====

Revision as of 20:47, 4 June 2020


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)
How to Cite This Entry:
Constructive semantics. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Constructive_semantics&oldid=46489
This article was adapted from an original article by G.E. Mints (originator), which appeared in Encyclopedia of Mathematics - ISBN 1402006098. See original article