Stepwise semantic system
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 
is that 
expresses the realizability of a construction 
, such that if 
is an arbitrary construction asserting 
, then 
and 
together make it possible to find a construction that asserts 
. This informal explanation does not lend itself to an exact definition, for a number of reasons. Markov's idea is that the implication 
can be considered as a formulation of a statement on the deducibility of 
from the premise 
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 
and 
, 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 
take either the form 
or 
, where 
are primitive recursive terms (terms of 
). The other formulas of 
are constructed in the usual way using the logical operations of conjunction 
, disjunction 
and the restricted quantifiers (cf. Restricted quantifier) 
, 
, where 
is a formula in 
and 
is a term in 
. The language 
is decidable in the sense that there is a general method of recognizing the true closed formulas of 
out of all the formulas of 
. The semantics of the formulas of 
is defined by induction with respect to the construction of the formula. Every formula of 
is equivalent to a formula without quantifiers.
The formulas of 
are constructed from the formulas of 
by means of any number of uses of the operations 
, 
and the existential quantifier. The language 
is undecidable, but a calculus 
can be constructed in which exactly the true closed formulas of 
are derivable. The formulas of 
are constructed inductively from the formulas of 
by means of a single application of the operation 
and any number of applications of the conjunction 
and the quantifier 
. Thus, the formulas of 
take one of the following forms: 1) the formulas of 
; 2) 
, where 
are formulas of 
; 3) 
, where 
are formulas of 
; 4) 
, where 
is a formula of 
. The implications 
are interpreted as follows: 
expresses the presence of a general method which, for any word 
in the alphabet of the language, makes it possible either to establish that 
is not a deduction of the formula 
in the calculus 
, or to give a deduction of 
in the calculus 
. A semi-formal theory 
is then constructed in which the closed formulas of 
can be deduced (for 
, the role of 
is played by 
). The true formulas of 
are the axioms of 
. Among the usual derivation rules is the effective 
-rule with an infinite number of premises: If a general method exists that enables one to derive the formula 
in 
for every natural number 
, then the formula 
can be considered to be derivable in 
. The soundness of 
is expressed by the following theorem: Every closed formula of 
that can be derived from a true formula of 
or from a premise, is true in 
.
The formulas of 
can be constructed inductively from 
by means of a single application of the operation 
and any number of applications of 
and 
. The implication 
expresses the fact that 
is derivable from the formula 
in the theory 
. It can be shown that the two forms of implication in the language 
are consistent with each other when they are both applicable. The semi-formal theory 
is then constructed, and its soundness is proved. The languages 
are constructed in the same way, as are the semi-formal theories 
. The formulas of 
are constructed from the formulas of 
by means of a single application of the operation 
to formulas of the previous language 
and of any number of applications of 
and 
to the formulas of 
. The implication 
expresses the fact that 
is derivable from 
in 
. All 
are sound: Every closed formula of 
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 
in a single language 
, whose formulas are obtained if the indices are removed from the implications in all the languages 
. A formula 
of 
is considered to be true if it is true in some 
, where the indices of the implications are chosen so as to make 
into a formula of 
.
If the negation 
is introduced in 
as a shorthand notation for 
, then the formula 
is true in 
for every formula 
of the language 
. Thus, the constructive selection principle proves to be true in 
. The languages 
form an essentially non-degenerate hierarchy from the point of view of the expressive possibilities of their formulas. Classical predicate calculus with the operations 
, 
, 
, 
is complete with respect to truth in 
.
Finally, 
contains all formulas of formal arithmetic. Using the algorithm exposing Shanin's constructive problem [4], every closed formula 
of 
can be reduced to the form 
, where 
is a formula of 
. A formula 
is considered to be true if a natural number 
can be given such that 
is true in 
. This concept of the judgements of arithmetic is consistent with all the fundamental principles of constructive mathematics. In particular, every formula of 
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) |
Stepwise semantic system. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Stepwise_semantic_system&oldid=48835