A Precise Definition of an Inference (by the Example of Natural Deduction Systems for Logics I‹α, β›

Аннотация

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α, β›, α, β ∈ $$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

Скачивания

Данные скачивания пока не доступны.

Article Details

Как цитировать
[1]
V. O. Shangin. A Precise Definition of an Inference (by the Example of Natural Deduction Systems for Logics I‹α, β› // Логические исследования / Logical Investigations. 2017. Т. 23. № 1.
.
Раздел
Неклассические логики