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
The geometry of non-distributive logics
