The subformula property of natural deduction derivations and analytic cuts

Logic Journal of the IGPL (forthcoming)
  Copy   BIBTEX

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.

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 93,642

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Analytics

Added to PP
2020-06-18

Downloads
12 (#1,115,280)

6 months
27 (#114,075)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Mirjana Borisavljević
University of Belgrade