|
Section
|
Mathematics
|
|
Title
|
Interactive realizations of logical formulas
|
|
Author(-s)
|
Beltyukov A.P.a
|
|
Affiliations
|
Udmurt State Universitya
|
|
Abstract
|
A new constructive understanding of logical formulas is considered. This understanding corresponds to intuition and traditional means of constructive logical inference. The new understanding is logically simpler than traditional realizability (in the sense of quantifier depth), but it also natural with respect to algorithmic solution of tasks. This understanding uses not only witness (realization) of the formula to understand but it also uses notion of test (counteraction) of this realization at the given formula. The main form of a sentence to understand a formula $A$ is $a:A:b$, that means that “the witness $a$ wins the obstacle $b$ while trying to approve the formula $A$”. This procedure can be regarded as a procedure of arbitration for making the necessary solution. The basis of the arbitration procedure for atomic formulas is defined by the interpretation of the language. The procedure for complex sentences is given by special rules determining the meaning of logical connectives. In the most natural definition of the arbitration procedure it has polynomial time complexity. A formula $A$ is considered to be true in the new sense if there is a witness of the formula that wins all possible obstacles at the formula. A language without negation is considered. A theorem of correctness of traditional intuitionistic axioms and inference rules is proved. The system of logical inference is formulated in sequent form. It is oriented to the inverse method of logical inference search.
|
|
Keywords
|
logical formulas, understanding, realization, counteraction
|
|
UDC
|
510.252
|
|
MSC
|
03B20, 03B30
|
|
DOI
|
10.20537/vm160204
|
|
Received
|
5 May 2016
|
|
Language
|
Russian
|
|
Citation
|
Beltyukov A.P. Interactive realizations of logical formulas, Vestnik Udmurtskogo Universiteta. Matematika. Mekhanika. Komp'yuternye Nauki, 2016, vol. 26, issue 2, pp. 177-193.
|
|
References
|
- Markov A.A. An attempt to construct the logic of constructive mathematics, Issledovaniya po teorii algorifmov I matematicheskoi logike: Sbornik statei, Tom 2 (Investigations on the theory of algorithms and mathematical logic: Proceedings, vol. 2), Moscow, 1976, pp. 3-31 (in Russian).
- Shanin N.A. A hierarchy of ways of understanding judgements in constructive mathematics, Tr. Mat. Inst. Steklova, 1973, vol. 129, pp. 203-266 (in Russian).
- Kleene S.C. Introduction to metamathematics, North-Holland, 1951, 500 p. Translated under the title Vvedenie v metamatematiku, Moscow: Inostr. Lit., 1957, 526 p.
- Vereshchagin N.K., Shen' A. Lektsii po matematicheskoi logike i teorii algoritmov. Chast' 3. Vychislimye funktsii (Lectures on mathematical logic and algorithm theory. Part 3. Computable functions), Moscow: Moscow Center for Continuous Mathematical Education, 2012, 160 p.
- Maslov S.Yu. The inverse method for establishing deducibility for logical calculi, Tr. Mat. Inst. Steklova, 1968, vol. 98, pp. 26-87 (in Russian).
- Beltiukov A.P. Intuitionistic formal theories with realizability in subrecursive classes, Annals of Pure and Applied Logic, 1997, vol. 89, pp. 3-15.
- Beltiukov A.P. A strong induction scheme that leads to polynomially computable realizations, Theoretical Computer Science, 2004, vol. 322, pp. 17-39.
- Beltiukov A.P. A polinomial programming language, Mathematical Problems of Computer Science: Transactions of the Institute for Informatics and Automation Problems of the National Academy of Sciences of Armenia, 2006, vol. 27, pp. 11-19.
|
|
Full text
|
|
+7 (3412) 91 60 92
Russian