scholarly journals The Rule of Existential Generalisation and Explicit Substitution

2021 ◽  
pp. 1-37
Author(s):  
Jiří Raclavský
Keyword(s):  
Natural Deduction ◽  
Existential Quantifier ◽  
Deduction System ◽  
Explicit Substitution ◽  
Natural Deduction System ◽  
Definition Of ◽  
Hyperintensional Logic

The present paper offers the rule of existential generalization (EG) that is uniformly applicable within extensional, intensional and hyperintensional contexts. In contradistinction to Quine and his followers, quantification into various modal contexts and some belief attitudes is possible without obstacles. The hyperintensional logic deployed in this paper incorporates explicit substitution and so the rule (EG) is fully specified inside the logic. The logic is equipped with a natural deduction system within which (EG) is derived from its rules for the existential quantifier, substitution and functional application. This shows that (EG) is not primitive, as often assumed even in advanced writings on natural deduction. Arguments involving existential generalisation are shown to be valid if the sequents containing their premises and conclusions are derivable using the rule (EG). The invalidity of arguments seemingly employing (EG) is explained with recourse to the definition of substitution.

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

2017 ◽  
Vol 23 (1) ◽  
pp. 83-104 ◽  
Author(s):  
В.О. Шангин
Keyword(s):  
Classical Logic ◽  
Natural Deduction ◽  
Precise Definition ◽  
The Other ◽  
Deduction System ◽  
Introduction Rule ◽  
Special Cases ◽  
Natural Deduction System ◽  
Alpha Beta ◽  
Definition Of

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

scholarly journals COMPLETENESS VIA CORRESPONDENCE FOR EXTENSIONS OF THE LOGIC OF PARADOX

2012 ◽  
Vol 5 (4) ◽  
pp. 720-730 ◽  
Author(s):  
BARTELD KOOI ◽  
ALLARD TAMMINGA
Keyword(s):  
Correspondence Analysis ◽  
Natural Deduction ◽  
Correspondence Theory ◽  
Truth Table ◽  
Deduction System ◽  
Natural Deduction System ◽  
Logic Of Paradox

AbstractTaking our inspiration from modal correspondence theory, we present the idea of correspondence analysis for many-valued logics. As a benchmark case, we study truth-functional extensions of the Logic of Paradox (LP). First, we characterize each of the possible truth table entries for unary and binary operators that could be added to LP by an inference scheme. Second, we define a class of natural deduction systems on the basis of these characterizing inference schemes and a natural deduction system for LP. Third, we show that each of the resulting natural deduction systems is sound and complete with respect to its particular semantics.

scholarly journals Normalization as a consequence of cut elimination

2009 ◽  
Vol 86 (100) ◽  
pp. 27-34
Author(s):  
Mirjana Borisavljevic
Keyword(s):  
Intuitionistic Logic ◽  
Natural Deduction ◽  
Cut Elimination ◽  
Deduction System ◽  
Normalization Theorem ◽  
Natural Deduction System

Pairs of systems, which consist of a system of sequents and a natural deduction system for some part of intuitionistic logic, are considered. For each of these pairs of systems the property that the normalization theorem is a consequence of the cut-elimination theorem is presented.

Sign in / Sign up

Export Citation Format

Share Document