A Precise Definition of an Inference (by the Example of Natural Deduction Systems for Logics $I_{\langle \alpha,\beta \rangle}$


V. O. Shangin


In the paper, we reconsider a precise definition of a natural deduction inference given by V. Smirnov. In refining the definition, we argue that all the other indirect rules of inference in a system can be considered as special cases of the implication introduction rule in a sense that if one of those rules can be applied then the implication introduction rule can be applied, either, but not vice versa. As an example, we use logics $I_{\langle\alpha, \beta\rangle}, \alpha, \beta \in \{0, 1, 2, 3,\dots \omega\}$, such that $I_{\langle 0, 0\rangle}$is propositional classical logic, presented by V. Popov. He uses these logics, in particular, a Hilbert-style calculus $HI_{\langle\alpha, \beta\rangle}, \alpha, \beta \in \{0, 1, 2, 3,\dots \omega\}$, for each logic in question, in order to construct examples of effects of Glivenko theorem’s generalization. Here we, first, propose a subordinated natural deduction system $NI_{\langle\alpha, \beta\rangle}, \alpha, \beta \in \{0, 1, 2, 3,\dots \omega\}$, for each logic in question, with a precise definition of a $NI_{\langle\alpha, \beta\rangle}$-inference. Moreover, we, comparatively, analyze precise and traditional definitions. Second, we prove that, for each $\alpha, \beta \in \{0, 1, 2, 3,\dots \omega\}$, a Hilbert-style calculus $HI_{\langle\alpha, \beta\rangle}$and a natural deduction system $NI_{\langle\alpha, \beta\rangle}$are equipollent, that is, a formula $A$ is provable in $HI_{\langle\alpha, \beta\rangle}$iff $A$ is provable in $NI_{\langle\alpha, \beta\rangle}$. DOI: 10.21146/2074-1472-2017-23-1-83-104






Anisov, A.M. Modern logic. Moscow: IFRAN Publishers, 2002. 273 pp. (In Russian)
Bocharov, V.A., Markin, V.I. Introduction to logic. Moscow: Forum Publ. house INFRA-M Publ., 2011. 560 pp. (In Russian)
Bolotov, A., Shangin, V. “Natural Deduction System in Paraconsistent Setting: Proof Search for PCont”, Journal of Intelligent Systems, 2012, Vol. 21(1), pp. 1–24.
Bolotov, A., Basukoski, A., Grigoriev, O., Shangin, V. “Natural deduction calculus for linear-time temporal logic”, LNAI, 2006, Vol. 4160, pp. 56–68.
Gentzen, G. The collected papers, ed. M.E. Szabo. North-Holland Pub. Co., 1969. 338 pp.
Ivlev, Yu.V. Logic. Moscow: Prospect Publ., 2008. 304 pp. (In Russian)
Kozhemyachenko, D. “Simulation of natural and sequent calculi”, Logicphilosophical studies, 2016, Vol. 13(2), pp. 181–182. (in Russian)
Popov, V., Shangin, V. “Syntax and semantics of simple paracomplete logics”, Logical investigations, 2013, Vol. 19, pp. 325–334.
Popov, V., Shangin, V. “Syntax and semantics of simple paranormal logics”, Logical-philosophical studies, 2014, Vol. 6, pp. 290–297.
Popov, V. “On one generalization of Glivenko theorem”, Logical investigations, 2015, Vol. 21(1), pp. 100–121. (In Russian)
Quine, W.V. “On natural deduction”, The Journal of Symbolic Logic, 1950, Vol. 15, No. 2, pp. 93–102.
Smirnov, V.A. Formal inference and logical calculi. Moscow: Nauka Publishers, 1972. (In Russian)
Smirnov, V.A., Anisov, A.M., Arutyunov, G.P., Dmitriyev, D.V., Melentyev, A.S., and Mikhailov, F.T. Logic and clinical diagnostics. Theoretical foundations. Moscow: Nauka Publishers, 1994. 271 pp. (In Russian)
Smirnov, V.A., Markin, V.I., Novodvorsky, A.E., and Smirnov, A.V. “Proof and proof searching”, in: Logic and computer, Vol. 3. Moscow: Nauka Publ., 1996. 296 pp. (In Russian)
Tomova, N.E., Shalack, V.I. Introduction to logic for philosophy faculties’ students. Moscow: IFRAN Publishers, 2014. 191 pp. (In Russian)
Voishvillo, E.K. Concept as a form of thinking. Moscow: MSU Publishers, 1989. 239 pp. (In Russian)