Namespaces
Variants
Actions

Difference between revisions of "Stepwise semantic system"

From Encyclopedia of Mathematics
Jump to: navigation, search
(Importing text file)
 
m (tex encoded by computer)
 
Line 1: Line 1:
A variant of [[Constructive semantics|constructive semantics]] proposed by A.A. Markov [[#References|[2]]], . In the construction of this system, particular attention is paid to one of the problems of semantics — the constructive interpretation of [[Implication|implication]]. The traditional intuitionistic explanation of the meaning of the statement <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s0877301.png" /> is that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s0877302.png" /> expresses the realizability of a construction <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s0877303.png" />, such that if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s0877304.png" /> is an arbitrary construction asserting <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s0877305.png" />, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s0877306.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s0877307.png" /> together make it possible to find a construction that asserts <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s0877308.png" />. This informal explanation does not lend itself to an exact definition, for a number of reasons. Markov's idea is that the implication <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s0877309.png" /> can be considered as a formulation of a statement on the deducibility of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773010.png" /> from the premise <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773011.png" /> by means of a theory containing a principle of infinite induction (a semi-formal theory). The semi-formal theory in question, as well as the semantics of the formulas <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773012.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773013.png" />, can therefore be explained at an earlier stage of the construction. As a result a stepwise semantic system arises, in which the sense of the formulas of the next step is defined in terms of the objects of the previous step.
+
<!--
 +
s0877301.png
 +
$#A+1 = 139 n = 6
 +
$#C+1 = 139 : ~/encyclopedia/old_files/data/S087/S.0807730 Stepwise semantic system
 +
Automatically converted into TeX, above some diagnostics.
 +
Please remove this comment and the {{TEX|auto}} line below,
 +
if TeX found to be correct.
 +
-->
  
Markov constructed two equivalent variants of a stepwise semantic system — the  "long tower stepwise semantic system03B10long tower"  [[#References|[2]]] and the  "short tower stepwise semantic system03B20short tower"  . The short-tower variant is briefly explained below in the traditional notation of [[Predicate calculus|predicate calculus]] as well as in the language of formal arithmetic (cf. [[Arithmetic, formal|Arithmetic, formal]]) (Markov himself used a notation of formulas without brackets). The elementary formulas of the language <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773014.png" /> take either the form <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773015.png" /> or <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773016.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773017.png" /> are primitive recursive terms (terms of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773018.png" />). The other formulas of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773019.png" /> are constructed in the usual way using the logical operations of [[Conjunction|conjunction]] <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773020.png" />, [[Disjunction|disjunction]] <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773021.png" /> and the restricted quantifiers (cf. [[Restricted quantifier|Restricted quantifier]]) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773022.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773023.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773024.png" /> is a formula in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773025.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773026.png" /> is a term in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773027.png" />. The language <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773028.png" /> is decidable in the sense that there is a general method of recognizing the true closed formulas of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773029.png" /> out of all the formulas of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773030.png" />. The semantics of the formulas of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773031.png" /> is defined by induction with respect to the construction of the formula. Every formula of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773032.png" /> is equivalent to a formula without quantifiers.
+
{{TEX|auto}}
 +
{{TEX|done}}
  
The formulas of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773033.png" /> are constructed from the formulas of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773034.png" /> by means of any number of uses of the operations <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773035.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773036.png" /> and the existential quantifier. The language <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773037.png" /> is undecidable, but a calculus <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773038.png" /> can be constructed in which exactly the true closed formulas of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773039.png" /> are derivable. The formulas of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773040.png" /> are constructed inductively from the formulas of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773041.png" /> by means of a single application of the operation <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773042.png" /> and any number of applications of the conjunction <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773043.png" /> and the quantifier <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773044.png" />. Thus, the formulas of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773045.png" /> take one of the following forms: 1) the formulas of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773046.png" />; 2) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773047.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773048.png" /> are formulas of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773049.png" />; 3) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773050.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773051.png" /> are formulas of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773052.png" />; 4) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773053.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773054.png" /> is a formula of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773055.png" />. The implications <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773056.png" /> are interpreted as follows: <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773057.png" /> expresses the presence of a general method which, for any word <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773058.png" /> in the alphabet of the language, makes it possible either to establish that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773059.png" /> is not a deduction of the formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773060.png" /> in the calculus <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773061.png" />, or to give a deduction of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773062.png" /> in the calculus <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773063.png" />. A semi-formal theory <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773064.png" /> is then constructed in which the closed formulas of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773065.png" /> can be deduced (for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773066.png" />, the role of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773067.png" /> is played by <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773068.png" />). The true formulas of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773069.png" /> are the axioms of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773070.png" />. Among the usual derivation rules is the effective <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773072.png" />-rule with an infinite number of premises: If a general method exists that enables one to derive the formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773073.png" /> in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773074.png" /> for every natural number <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773075.png" />, then the formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773076.png" /> can be considered to be derivable in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773077.png" />. The soundness of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773078.png" /> is expressed by the following theorem: Every closed formula of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773079.png" /> that can be derived from a true formula of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773080.png" /> or from a premise, is true in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773081.png" />.
+
A variant of [[Constructive semantics|constructive semantics]] proposed by A.A. Markov [[#References|[2]]], . In the construction of this system, particular attention is paid to one of the problems of semantics — the constructive interpretation of [[Implication|implication]]. The traditional intuitionistic explanation of the meaning of the statement  $  ( A \supset B) $
 +
is that  $  ( A \supset B) $
 +
expresses the realizability of a construction  $  p $,  
 +
such that if  $  q $
 +
is an arbitrary construction asserting  $  A $,  
 +
then  $  p $
 +
and  $  q $
 +
together make it possible to find a construction that asserts  $  B $.  
 +
This informal explanation does not lend itself to an exact definition, for a number of reasons. Markov's idea is that the implication  $  ( A \supset B) $
 +
can be considered as a formulation of a statement on the deducibility of $  B $
 +
from the premise  $  A $
 +
by means of a theory containing a principle of infinite induction (a semi-formal theory). The semi-formal theory in question, as well as the semantics of the formulas $  A $
 +
and  $  B $,
 +
can therefore be explained at an earlier stage of the construction. As a result a stepwise semantic system arises, in which the sense of the formulas of the next step is defined in terms of the objects of the previous step.
  
The formulas of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773082.png" /> can be constructed inductively from <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773083.png" /> by means of a single application of the operation <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773084.png" /> and any number of applications of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773085.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773086.png" />. The implication <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773087.png" /> expresses the fact that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773088.png" /> is derivable from the formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773089.png" /> in the theory <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773090.png" />. It can be shown that the two forms of implication in the language <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773091.png" /> are consistent with each other when they are both applicable. The semi-formal theory <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773092.png" /> is then constructed, and its soundness is proved. The languages <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773093.png" /> are constructed in the same way, as are the semi-formal theories <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773094.png" />. The formulas of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773095.png" /> are constructed from the formulas of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773096.png" /> by means of a single application of the operation <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773097.png" /> to formulas of the previous language <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773098.png" /> and of any number of applications of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s08773099.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s087730100.png" /> to the formulas of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s087730101.png" />. The implication <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s087730102.png" /> expresses the fact that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s087730103.png" /> is derivable from <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s087730104.png" /> in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s087730105.png" />. All <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s087730106.png" /> are sound: Every closed formula of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s087730107.png" /> that can be derived from a true formula is true. Implications at different levels are consistent when they are both applicable.
+
Markov constructed two equivalent variants of a stepwise semantic system — the "long tower stepwise semantic system03B10long tower" [[#References|[2]]] and the  "short tower stepwise semantic system03B20short tower" . The short-tower variant is briefly explained below in the traditional notation of [[Predicate calculus|predicate calculus]] as well as in the language of formal arithmetic (cf. [[Arithmetic, formal|Arithmetic, formal]]) (Markov himself used a notation of formulas without brackets). The elementary formulas of the language $  L _ {0} $
 +
take either the form  $  ( t= r) $
 +
or  $  ( t \neq r) $,
 +
where  $  t, r $
 +
are primitive recursive terms (terms of  $  L _ {0} $).  
 +
The other formulas of  $  L _ {0} $
 +
are constructed in the usual way using the logical operations of [[Conjunction|conjunction]]  $  \wedge $,  
 +
[[Disjunction|disjunction]]  $  \lor $
 +
and the restricted quantifiers (cf. [[Restricted quantifier|Restricted quantifier]])  $  (\forall x \leq  t) \phi $,
 +
$  (\exists x \leq  t) \phi $,
 +
where  $  \phi $
 +
is a formula in  $  L _ {0} $
 +
and  $  t $
 +
is a term in  $  L _ {0} $.  
 +
The language  $  L _ {0} $
 +
is decidable in the sense that there is a general method of recognizing the true closed formulas of $  L _ {0} $
 +
out of all the formulas of $  L _ {0} $.  
 +
The semantics of the formulas of $  L _ {0} $
 +
is defined by induction with respect to the construction of the formula. Every formula of $  L _ {0} $
 +
is equivalent to a formula without quantifiers.
  
This consistency makes it possible to combine all the languages <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s087730108.png" /> in a single language <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s087730109.png" />, whose formulas are obtained if the indices are removed from the implications in all the languages <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s087730110.png" />. A formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s087730111.png" /> of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s087730112.png" /> is considered to be true if it is true in some <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s087730113.png" />, where the indices of the implications are chosen so as to make <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s087730114.png" /> into a formula of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s087730115.png" />.
+
The formulas of  $  L _ {1} $
 +
are constructed from the formulas of  $  L _ {0} $
 +
by means of any number of uses of the operations  $  \lor $,
 +
$  \wedge $
 +
and the existential quantifier. The language  $  L _ {1} $
 +
is undecidable, but a calculus  $  C $
 +
can be constructed in which exactly the true closed formulas of  $  L _ {1} $
 +
are derivable. The formulas of  $  L _ {2} $
 +
are constructed inductively from the formulas of  $  L _ {1} $
 +
by means of a single application of the operation  $  \supset $
 +
and any number of applications of the conjunction  $  \wedge $
 +
and the quantifier  $  \forall $.
 +
Thus, the formulas of  $  L _ {2} $
 +
take one of the following forms: 1) the formulas of  $  L _ {1} $;
 +
2)  $  ( \phi \wedge \psi ) $,
 +
where  $  \phi , \psi $
 +
are formulas of  $  L _ {2} $;
 +
3)  $  ( \alpha \supset \beta ) $,
 +
where  $  \alpha , \beta $
 +
are formulas of  $  L _ {1} $;
 +
4)  $  \forall x \phi $,
 +
where  $  \phi $
 +
is a formula of  $  L _ {2} $.
 +
The implications  $  ( \alpha \supset \beta ) $
 +
are interpreted as follows:  $  ( \alpha \supset \beta ) $
 +
expresses the presence of a general method which, for any word  $  Q $
 +
in the alphabet of the language, makes it possible either to establish that  $  Q $
 +
is not a deduction of the formula  $  \alpha $
 +
in the calculus  $  C $,
 +
or to give a deduction of  $  \beta $
 +
in the calculus  $  C $.  
 +
A semi-formal theory  $  S _ {2} $
 +
is then constructed in which the closed formulas of  $  L _ {2} $
 +
can be deduced (for  $  L _ {1} $,
 +
the role of  $  S _ {2} $
 +
is played by  $  C $).  
 +
The true formulas of  $  L _ {2} $
 +
are the axioms of  $  S _ {2} $.  
 +
Among the usual derivation rules is the effective  $  \omega $-
 +
rule with an infinite number of premises: If a general method exists that enables one to derive the formula  $  \phi ( n) $
 +
in  $  S _ {2} $
 +
for every natural number  $  n $,
 +
then the formula  $  \forall x \phi ( x) $
 +
can be considered to be derivable in $  S _ {2} $.  
 +
The soundness of $  S _ {2} $
 +
is expressed by the following theorem: Every closed formula of  $  L _ {2} $
 +
that can be derived from a true formula of $  L _ {2} $
 +
or from a premise, is true in  $  L _ {2} $.
  
If the negation <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s087730116.png" /> is introduced in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s087730117.png" /> as a shorthand notation for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s087730118.png" />, then the formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s087730119.png" /> is true in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s087730120.png" /> for every formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s087730121.png" /> of the language <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s087730122.png" />. Thus, the [[Constructive selection principle|constructive selection principle]] proves to be true in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s087730123.png" />. The languages <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s087730124.png" /> form an essentially non-degenerate hierarchy from the point of view of the expressive possibilities of their formulas. Classical predicate calculus with the operations <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s087730125.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s087730126.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s087730127.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s087730128.png" /> is complete with respect to truth in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s087730129.png" />.
+
The formulas of  $  L _ {3} $
 +
can be constructed inductively from  $  L _ {2} $
 +
by means of a single application of the operation  $  \supset _ {1} $
 +
and any number of applications of  $  \wedge $
 +
and  $  \forall $.  
 +
The implication  $  ( \alpha \supset _ {1} \beta ) $
 +
expresses the fact that  $  \beta $
 +
is derivable from the formula $  \alpha $
 +
in the theory  $  S _ {2} $.  
 +
It can be shown that the two forms of implication in the language $  L _ {3} $
 +
are consistent with each other when they are both applicable. The semi-formal theory  $  S _ {3} $
 +
is then constructed, and its soundness is proved. The languages  $  L _ {4} , L _ {5} \dots $
 +
are constructed in the same way, as are the semi-formal theories  $  S _ {4} , S _ {5} , . . . $.  
 +
The formulas of  $  L _ {n+} 1 $
 +
are constructed from the formulas of  $  L _ {n} $
 +
by means of a single application of the operation  $  \supset _ {(} n- 1) $
 +
to formulas of the previous language  $  L _ {n} $
 +
and of any number of applications of $  \wedge $
 +
and  $  \forall $
 +
to the formulas of  $  L _ {n+} 1 $.  
 +
The implication  $  ( \alpha \supset _ {(} n- 1) \beta ) $
 +
expresses the fact that  $  \beta $
 +
is derivable from  $  \alpha $
 +
in  $  S _ {n} $.  
 +
All  $  S _ {n} $
 +
are sound: Every closed formula of  $  L _ {n} $
 +
that can be derived from a true formula is true. Implications at different levels are consistent when they are both applicable.
  
Finally, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s087730130.png" /> contains all formulas of formal arithmetic. Using the algorithm exposing Shanin's constructive problem [[#References|[4]]], every closed formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s087730131.png" /> of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s087730132.png" /> can be reduced to the form <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s087730133.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s087730134.png" /> is a formula of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s087730135.png" />. A formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s087730136.png" /> is considered to be true if a natural number <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s087730137.png" /> can be given such that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s087730138.png" /> is true in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s087730139.png" />. This concept of the judgements of arithmetic is consistent with all the fundamental principles of [[Constructive mathematics|constructive mathematics]]. In particular, every formula of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s087730140.png" /> is equivalent to its proper recursive Kleene realization [[#References|[5]]].
+
This consistency makes it possible to combine all the languages  $  L _ {n} $
 +
in a single language  $  L _  \omega  $,
 +
whose formulas are obtained if the indices are removed from the implications in all the languages  $  L _ {n} $.
 +
A formula  $  \phi $
 +
of  $  L _  \omega  $
 +
is considered to be true if it is true in some  $  L _ {n} $,  
 +
where the indices of the implications are chosen so as to make  $  \phi $
 +
into a formula of  $  L _ {n} $.
 +
 
 +
If the negation  $  \neg \phi $
 +
is introduced in  $  L _  \omega  $
 +
as a shorthand notation for  $  ( \phi \supset 0 = 1) $,
 +
then the formula  $  \neg \neg \alpha \supset \alpha $
 +
is true in  $  L _  \omega  $
 +
for every formula  $  \alpha $
 +
of the language  $  L _ {1} $.  
 +
Thus, the [[Constructive selection principle|constructive selection principle]] proves to be true in  $  L _  \omega  $.
 +
The languages  $  L _ {n} $
 +
form an essentially non-degenerate hierarchy from the point of view of the expressive possibilities of their formulas. Classical predicate calculus with the operations  $  \wedge $,
 +
$  \neg $,
 +
$  \supset $,
 +
$  \forall $
 +
is complete with respect to truth in  $  L _  \omega  $.
 +
 
 +
Finally,  $  L _ {\omega + 1 }  $
 +
contains all formulas of formal arithmetic. Using the algorithm exposing Shanin's constructive problem [[#References|[4]]], every closed formula $  \phi $
 +
of $  L _ {\omega + 1 }  $
 +
can be reduced to the form $  \exists x \psi ( x) $,  
 +
where $  \psi ( x) $
 +
is a formula of $  L _  \omega  $.  
 +
A formula $  \phi $
 +
is considered to be true if a natural number $  n $
 +
can be given such that $  \phi ( n) $
 +
is true in $  L _  \omega  $.  
 +
This concept of the judgements of arithmetic is consistent with all the fundamental principles of [[Constructive mathematics|constructive mathematics]]. In particular, every formula of $  L _ {\omega + 1 }  $
 +
is equivalent to its proper recursive Kleene realization [[#References|[5]]].
  
 
====References====
 
====References====
 
<table><TR><TD valign="top">[1]</TD> <TD valign="top">  A. Heyting,  "Intuitionism: an introduction" , North-Holland  (1970)</TD></TR><TR><TD valign="top">[2]</TD> <TD valign="top">  A.A. Markov,  "Essai de construction d'une logique de la mathématique constructive. Logique et méthodologie des sciences en U.R.S.S."  ''Rev. Internat. Phil.'' , '''25''' :  4  (1971)  pp. 477–507</TD></TR><TR><TD valign="top">[3a]</TD> <TD valign="top">  A.A. Markov,  "On the language <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s087730141.png" />"  ''Soviet Math. Dokl.'' , '''15'''  (1974)  pp. 38–42  ''Dokl. Akad. Nauk SSSR'' , '''214''' :  1  (1974)  pp. 40–43</TD></TR><TR><TD valign="top">[3b]</TD> <TD valign="top">  A.A. Markov,  "On the language <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s087730142.png" />"  ''Soviet Math. Dokl.'' , '''15'''  (1974)  pp. 125–128  ''Dokl. Akad. Nauk SSSR'' , '''214''' :  2  (1974)  pp. 279–282</TD></TR><TR><TD valign="top">[3c]</TD> <TD valign="top">  A.A. Markov,  "On the language <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s087730143.png" />"  ''Soviet Math. Dokl.'' , '''15'''  (1974)  pp. 184–188  ''Dokl. Akad. Nauk SSSR'' , '''214''' :  3  (1974)  pp. 513–516</TD></TR><TR><TD valign="top">[3d]</TD> <TD valign="top">  A.A. Markov,  "On the language <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s087730144.png" />"  ''Soviet Math. Dokl.'' , '''15'''  (1974)  pp. 242–246  ''Dokl. Akad. Nauk SSSR'' , '''214''' :  4  (1974)  pp. 765–768</TD></TR><TR><TD valign="top">[3e]</TD> <TD valign="top">  A.A. Markov,  "On the languages <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s087730145.png" />"  ''Soviet Math. Dokl.'' , '''15'''  (1974)  pp. 313–318  ''Dokl. Akad. Nauk SSSR'' , '''214''' :  5  (1974)  pp. 1031–1034; 1262–1264</TD></TR><TR><TD valign="top">[3f]</TD> <TD valign="top">  A.A. Markov,  "On the language <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s087730146.png" />"  ''Soviet Math. Dokl.'' , '''15'''  (1974)  pp. 443–447  ''Dokl. Akad. Nauk SSSR'' , '''215''' :  1  (1974)  pp. 57–60</TD></TR><TR><TD valign="top">[3g]</TD> <TD valign="top">  A.A. Markov,  "On the completeness of the classical predicate calculus in constructive mathematics"  ''Soviet Math. Dokl.'' , '''15'''  (1974)  pp. 476–481  ''Dokl. Akad. Nauk SSSR'' , '''215''' :  2  (1974)  pp. 266–269</TD></TR><TR><TD valign="top">[4]</TD> <TD valign="top">  N.A. Shanin,  "On the constructive interpretation of mathematical judgements"  ''Transl. Amer. Math. Soc. (2)'' , '''23'''  (1960)  pp. 109–190  ''Trudy Mat. Inst. Steklov.'' , '''52'''  (1958)  pp. 226–311</TD></TR><TR><TD valign="top">[5]</TD> <TD valign="top">  A.G. Dragalin,  "Mathematical intuitionism. Introduction to proof theory" , Amer. Math. Soc.  (1988)  (Translated from Russian)</TD></TR></table>
 
<table><TR><TD valign="top">[1]</TD> <TD valign="top">  A. Heyting,  "Intuitionism: an introduction" , North-Holland  (1970)</TD></TR><TR><TD valign="top">[2]</TD> <TD valign="top">  A.A. Markov,  "Essai de construction d'une logique de la mathématique constructive. Logique et méthodologie des sciences en U.R.S.S."  ''Rev. Internat. Phil.'' , '''25''' :  4  (1971)  pp. 477–507</TD></TR><TR><TD valign="top">[3a]</TD> <TD valign="top">  A.A. Markov,  "On the language <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s087730141.png" />"  ''Soviet Math. Dokl.'' , '''15'''  (1974)  pp. 38–42  ''Dokl. Akad. Nauk SSSR'' , '''214''' :  1  (1974)  pp. 40–43</TD></TR><TR><TD valign="top">[3b]</TD> <TD valign="top">  A.A. Markov,  "On the language <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s087730142.png" />"  ''Soviet Math. Dokl.'' , '''15'''  (1974)  pp. 125–128  ''Dokl. Akad. Nauk SSSR'' , '''214''' :  2  (1974)  pp. 279–282</TD></TR><TR><TD valign="top">[3c]</TD> <TD valign="top">  A.A. Markov,  "On the language <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s087730143.png" />"  ''Soviet Math. Dokl.'' , '''15'''  (1974)  pp. 184–188  ''Dokl. Akad. Nauk SSSR'' , '''214''' :  3  (1974)  pp. 513–516</TD></TR><TR><TD valign="top">[3d]</TD> <TD valign="top">  A.A. Markov,  "On the language <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s087730144.png" />"  ''Soviet Math. Dokl.'' , '''15'''  (1974)  pp. 242–246  ''Dokl. Akad. Nauk SSSR'' , '''214''' :  4  (1974)  pp. 765–768</TD></TR><TR><TD valign="top">[3e]</TD> <TD valign="top">  A.A. Markov,  "On the languages <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s087730145.png" />"  ''Soviet Math. Dokl.'' , '''15'''  (1974)  pp. 313–318  ''Dokl. Akad. Nauk SSSR'' , '''214''' :  5  (1974)  pp. 1031–1034; 1262–1264</TD></TR><TR><TD valign="top">[3f]</TD> <TD valign="top">  A.A. Markov,  "On the language <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s087/s087730/s087730146.png" />"  ''Soviet Math. Dokl.'' , '''15'''  (1974)  pp. 443–447  ''Dokl. Akad. Nauk SSSR'' , '''215''' :  1  (1974)  pp. 57–60</TD></TR><TR><TD valign="top">[3g]</TD> <TD valign="top">  A.A. Markov,  "On the completeness of the classical predicate calculus in constructive mathematics"  ''Soviet Math. Dokl.'' , '''15'''  (1974)  pp. 476–481  ''Dokl. Akad. Nauk SSSR'' , '''215''' :  2  (1974)  pp. 266–269</TD></TR><TR><TD valign="top">[4]</TD> <TD valign="top">  N.A. Shanin,  "On the constructive interpretation of mathematical judgements"  ''Transl. Amer. Math. Soc. (2)'' , '''23'''  (1960)  pp. 109–190  ''Trudy Mat. Inst. Steklov.'' , '''52'''  (1958)  pp. 226–311</TD></TR><TR><TD valign="top">[5]</TD> <TD valign="top">  A.G. Dragalin,  "Mathematical intuitionism. Introduction to proof theory" , Amer. Math. Soc.  (1988)  (Translated from Russian)</TD></TR></table>
 
 
  
 
====Comments====
 
====Comments====
 
  
 
====References====
 
====References====
 
<table><TR><TD valign="top">[a1]</TD> <TD valign="top">  A.A. Markov,  N.M. [N.M. Nagornyi] Nagorny,  "The theory of algorithms" , Kluwer  (1988)  pp. §16  (Translated from Russian)</TD></TR></table>
 
<table><TR><TD valign="top">[a1]</TD> <TD valign="top">  A.A. Markov,  N.M. [N.M. Nagornyi] Nagorny,  "The theory of algorithms" , Kluwer  (1988)  pp. §16  (Translated from Russian)</TD></TR></table>

Latest revision as of 08:23, 6 June 2020


A variant of constructive semantics proposed by A.A. Markov [2], . In the construction of this system, particular attention is paid to one of the problems of semantics — the constructive interpretation of implication. The traditional intuitionistic explanation of the meaning of the statement $ ( A \supset B) $ is that $ ( A \supset B) $ expresses the realizability of a construction $ p $, such that if $ q $ is an arbitrary construction asserting $ A $, then $ p $ and $ q $ together make it possible to find a construction that asserts $ B $. This informal explanation does not lend itself to an exact definition, for a number of reasons. Markov's idea is that the implication $ ( A \supset B) $ can be considered as a formulation of a statement on the deducibility of $ B $ from the premise $ A $ by means of a theory containing a principle of infinite induction (a semi-formal theory). The semi-formal theory in question, as well as the semantics of the formulas $ A $ and $ B $, can therefore be explained at an earlier stage of the construction. As a result a stepwise semantic system arises, in which the sense of the formulas of the next step is defined in terms of the objects of the previous step.

Markov constructed two equivalent variants of a stepwise semantic system — the "long tower stepwise semantic system03B10long tower" [2] and the "short tower stepwise semantic system03B20short tower" . The short-tower variant is briefly explained below in the traditional notation of predicate calculus as well as in the language of formal arithmetic (cf. Arithmetic, formal) (Markov himself used a notation of formulas without brackets). The elementary formulas of the language $ L _ {0} $ take either the form $ ( t= r) $ or $ ( t \neq r) $, where $ t, r $ are primitive recursive terms (terms of $ L _ {0} $). The other formulas of $ L _ {0} $ are constructed in the usual way using the logical operations of conjunction $ \wedge $, disjunction $ \lor $ and the restricted quantifiers (cf. Restricted quantifier) $ (\forall x \leq t) \phi $, $ (\exists x \leq t) \phi $, where $ \phi $ is a formula in $ L _ {0} $ and $ t $ is a term in $ L _ {0} $. The language $ L _ {0} $ is decidable in the sense that there is a general method of recognizing the true closed formulas of $ L _ {0} $ out of all the formulas of $ L _ {0} $. The semantics of the formulas of $ L _ {0} $ is defined by induction with respect to the construction of the formula. Every formula of $ L _ {0} $ is equivalent to a formula without quantifiers.

The formulas of $ L _ {1} $ are constructed from the formulas of $ L _ {0} $ by means of any number of uses of the operations $ \lor $, $ \wedge $ and the existential quantifier. The language $ L _ {1} $ is undecidable, but a calculus $ C $ can be constructed in which exactly the true closed formulas of $ L _ {1} $ are derivable. The formulas of $ L _ {2} $ are constructed inductively from the formulas of $ L _ {1} $ by means of a single application of the operation $ \supset $ and any number of applications of the conjunction $ \wedge $ and the quantifier $ \forall $. Thus, the formulas of $ L _ {2} $ take one of the following forms: 1) the formulas of $ L _ {1} $; 2) $ ( \phi \wedge \psi ) $, where $ \phi , \psi $ are formulas of $ L _ {2} $; 3) $ ( \alpha \supset \beta ) $, where $ \alpha , \beta $ are formulas of $ L _ {1} $; 4) $ \forall x \phi $, where $ \phi $ is a formula of $ L _ {2} $. The implications $ ( \alpha \supset \beta ) $ are interpreted as follows: $ ( \alpha \supset \beta ) $ expresses the presence of a general method which, for any word $ Q $ in the alphabet of the language, makes it possible either to establish that $ Q $ is not a deduction of the formula $ \alpha $ in the calculus $ C $, or to give a deduction of $ \beta $ in the calculus $ C $. A semi-formal theory $ S _ {2} $ is then constructed in which the closed formulas of $ L _ {2} $ can be deduced (for $ L _ {1} $, the role of $ S _ {2} $ is played by $ C $). The true formulas of $ L _ {2} $ are the axioms of $ S _ {2} $. Among the usual derivation rules is the effective $ \omega $- rule with an infinite number of premises: If a general method exists that enables one to derive the formula $ \phi ( n) $ in $ S _ {2} $ for every natural number $ n $, then the formula $ \forall x \phi ( x) $ can be considered to be derivable in $ S _ {2} $. The soundness of $ S _ {2} $ is expressed by the following theorem: Every closed formula of $ L _ {2} $ that can be derived from a true formula of $ L _ {2} $ or from a premise, is true in $ L _ {2} $.

The formulas of $ L _ {3} $ can be constructed inductively from $ L _ {2} $ by means of a single application of the operation $ \supset _ {1} $ and any number of applications of $ \wedge $ and $ \forall $. The implication $ ( \alpha \supset _ {1} \beta ) $ expresses the fact that $ \beta $ is derivable from the formula $ \alpha $ in the theory $ S _ {2} $. It can be shown that the two forms of implication in the language $ L _ {3} $ are consistent with each other when they are both applicable. The semi-formal theory $ S _ {3} $ is then constructed, and its soundness is proved. The languages $ L _ {4} , L _ {5} \dots $ are constructed in the same way, as are the semi-formal theories $ S _ {4} , S _ {5} , . . . $. The formulas of $ L _ {n+} 1 $ are constructed from the formulas of $ L _ {n} $ by means of a single application of the operation $ \supset _ {(} n- 1) $ to formulas of the previous language $ L _ {n} $ and of any number of applications of $ \wedge $ and $ \forall $ to the formulas of $ L _ {n+} 1 $. The implication $ ( \alpha \supset _ {(} n- 1) \beta ) $ expresses the fact that $ \beta $ is derivable from $ \alpha $ in $ S _ {n} $. All $ S _ {n} $ are sound: Every closed formula of $ L _ {n} $ that can be derived from a true formula is true. Implications at different levels are consistent when they are both applicable.

This consistency makes it possible to combine all the languages $ L _ {n} $ in a single language $ L _ \omega $, whose formulas are obtained if the indices are removed from the implications in all the languages $ L _ {n} $. A formula $ \phi $ of $ L _ \omega $ is considered to be true if it is true in some $ L _ {n} $, where the indices of the implications are chosen so as to make $ \phi $ into a formula of $ L _ {n} $.

If the negation $ \neg \phi $ is introduced in $ L _ \omega $ as a shorthand notation for $ ( \phi \supset 0 = 1) $, then the formula $ \neg \neg \alpha \supset \alpha $ is true in $ L _ \omega $ for every formula $ \alpha $ of the language $ L _ {1} $. Thus, the constructive selection principle proves to be true in $ L _ \omega $. The languages $ L _ {n} $ form an essentially non-degenerate hierarchy from the point of view of the expressive possibilities of their formulas. Classical predicate calculus with the operations $ \wedge $, $ \neg $, $ \supset $, $ \forall $ is complete with respect to truth in $ L _ \omega $.

Finally, $ L _ {\omega + 1 } $ contains all formulas of formal arithmetic. Using the algorithm exposing Shanin's constructive problem [4], every closed formula $ \phi $ of $ L _ {\omega + 1 } $ can be reduced to the form $ \exists x \psi ( x) $, where $ \psi ( x) $ is a formula of $ L _ \omega $. A formula $ \phi $ is considered to be true if a natural number $ n $ can be given such that $ \phi ( n) $ is true in $ L _ \omega $. This concept of the judgements of arithmetic is consistent with all the fundamental principles of constructive mathematics. In particular, every formula of $ L _ {\omega + 1 } $ is equivalent to its proper recursive Kleene realization [5].

References

[1] A. Heyting, "Intuitionism: an introduction" , North-Holland (1970)
[2] A.A. Markov, "Essai de construction d'une logique de la mathématique constructive. Logique et méthodologie des sciences en U.R.S.S." Rev. Internat. Phil. , 25 : 4 (1971) pp. 477–507
[3a] A.A. Markov, "On the language " Soviet Math. Dokl. , 15 (1974) pp. 38–42 Dokl. Akad. Nauk SSSR , 214 : 1 (1974) pp. 40–43
[3b] A.A. Markov, "On the language " Soviet Math. Dokl. , 15 (1974) pp. 125–128 Dokl. Akad. Nauk SSSR , 214 : 2 (1974) pp. 279–282
[3c] A.A. Markov, "On the language " Soviet Math. Dokl. , 15 (1974) pp. 184–188 Dokl. Akad. Nauk SSSR , 214 : 3 (1974) pp. 513–516
[3d] A.A. Markov, "On the language " Soviet Math. Dokl. , 15 (1974) pp. 242–246 Dokl. Akad. Nauk SSSR , 214 : 4 (1974) pp. 765–768
[3e] A.A. Markov, "On the languages " Soviet Math. Dokl. , 15 (1974) pp. 313–318 Dokl. Akad. Nauk SSSR , 214 : 5 (1974) pp. 1031–1034; 1262–1264
[3f] A.A. Markov, "On the language " Soviet Math. Dokl. , 15 (1974) pp. 443–447 Dokl. Akad. Nauk SSSR , 215 : 1 (1974) pp. 57–60
[3g] A.A. Markov, "On the completeness of the classical predicate calculus in constructive mathematics" Soviet Math. Dokl. , 15 (1974) pp. 476–481 Dokl. Akad. Nauk SSSR , 215 : 2 (1974) pp. 266–269
[4] N.A. Shanin, "On the constructive interpretation of mathematical judgements" Transl. Amer. Math. Soc. (2) , 23 (1960) pp. 109–190 Trudy Mat. Inst. Steklov. , 52 (1958) pp. 226–311
[5] A.G. Dragalin, "Mathematical intuitionism. Introduction to proof theory" , Amer. Math. Soc. (1988) (Translated from Russian)

Comments

References

[a1] A.A. Markov, N.M. [N.M. Nagornyi] Nagorny, "The theory of algorithms" , Kluwer (1988) pp. §16 (Translated from Russian)
How to Cite This Entry:
Stepwise semantic system. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Stepwise_semantic_system&oldid=48835
This article was adapted from an original article by A.G. Dragalin (originator), which appeared in Encyclopedia of Mathematics - ISBN 1402006098. See original article