The subformula property of natural deduction derivations and analytic cuts

2020 ◽  
Author(s):  
Mirjana Borisavljević
Keyword(s):  
Natural Deduction ◽  
Deduction System ◽  
Natural Deduction System ◽  
Sequent System ◽  
Subformula Property

Abstract In derivations of a sequent system, $\mathcal{L}\mathcal{J}$, and a natural deduction system, $\mathcal{N}\mathcal{J}$, the trails of formulae and the subformula property based on these trails will be defined. The derivations of $\mathcal{N}\mathcal{J}$ and $\mathcal{L}\mathcal{J}$ will be connected by the map $g$, and it will be proved the following: an $\mathcal{N}\mathcal{J}$-derivation is normal $\Longleftrightarrow $ it has the subformula property based on trails $\Longleftrightarrow $ its $g$-image in $\mathcal{L}\mathcal{J}$ is without maximum cuts $\Longrightarrow $ that $g$-image has the subformula property based on trails. In $\mathcal{L}\mathcal{J}$-derivations, another type of cuts, sub-cuts, will be introduced, and it will be proved the following: all cuts of an $\mathcal{L}\mathcal{J}$-derivation are sub-cuts $\Longleftrightarrow $ it has the subformula property based on trails.

scholarly journals Labelled Natural Deduction for Public Announcement Logic with Common Knowledge

Mathematics ◽  
2020 ◽  
Vol 8 (4) ◽  
pp. 626
Author(s):  
Muhammad Farhan Mohd Nasir ◽  
Wan Ainun Mior Othman ◽  
Kok Bin Wong
Keyword(s):  
Natural Deduction ◽  
Common Knowledge ◽  
Deduction System ◽  
Public Announcement ◽  
Public Announcement Logic ◽  
Natural Deduction System ◽  
The Common ◽  
Subformula Property

Public announcement logic is a logic that studies epistemic updates. In this paper, we propose a sound and complete labelled natural deduction system for public announcement logic with the common knowledge operator (PAC). The completeness of the proposed system is proved indirectly through a Hilbert calculus for PAC known to be complete and sound. We conclude with several discussions regarding the system including some problems of the system in attaining normalisation and subformula property.

scholarly journals Sequent Systems without Improper Derivations

2021 ◽  
Author(s):  
Katsumi Sasaki
Keyword(s):  
Propositional Logic ◽  
Natural Deduction ◽  
Inference Rules ◽  
Classical Propositional Logic ◽  
Deduction System ◽  
Structural Rules ◽  
Sequent Systems ◽  
Natural Deduction System ◽  
Sequent System

In the natural deduction system for classical propositional logic given by G. Gentzen, there are some inference rules with assumptions discharged by the rule. D. Prawitz calls such inference rules improper, and others proper. Improper inference rules are more complicated and are often harder to understand than the proper ones. In the present paper, we distinguish between proper and improper derivations by using sequent systems. Specifically, we introduce a sequent system \(\vdash_{\bf Sc}\) for classical propositional logic with only structural rules, and prove that \(\vdash_{\bf Sc}\) does not allow improper derivations in general. For instance, the sequent \(\Rightarrow p \to q\) cannot be derived from the sequent \(p \Rightarrow q\) in \(\vdash_{\bf Sc}\). In order to prove the failure of improper derivations, we modify the usual notion of truth valuation, and using the modified valuation, we prove the completeness of \(\vdash_{\bf Sc}\). We also consider whether an improper derivation can be described generally by using \(\vdash_{\bf Sc}\).

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.

Sign in / Sign up

Export Citation Format

Share Document