Proof-theoretic harmony and the levels of rules: Generalised non-flattening results

DSpace Repository


Dateien:

URI: http://hdl.handle.net/10900/130949
http://nbn-resolving.de/urn:nbn:de:bsz:21-dspace-1309499
http://dx.doi.org/10.15496/publikation-72309
http://nbn-resolving.org/urn:nbn:de:bsz:21-dspace-1309494
http://nbn-resolving.org/urn:nbn:de:bsz:21-dspace-1309496
Dokumentart: Article
Date: 2014
Source: Second Pisa Colloquium in Logic, Language and Epistemology. Ed. by Enrico Moriconi and Laura Tesconi. Pisa: Edizioni ETS 2014, pp. 245-287
Language: English
Faculty: 7 Mathematisch-Naturwissenschaftliche Fakultät
Department: Informatik
DDC Classifikation: 004 - Data processing and computer science
100 - Philosophy
Keywords: Beweistheorie , Logische Partikel , Kalkül des natürlichen Schließens
Other Keywords: Beweistheoretische Semantik
Proof Theory
Logical Constant
Natural Deduction
Proof-theoretic Semantics
ISBN: 978-884674033-5
License: http://tobias-lib.uni-tuebingen.de/doku/lic_mit_pod.php?la=de http://tobias-lib.uni-tuebingen.de/doku/lic_mit_pod.php?la=en
Order a printed copy: Print-on-Demand
Show full item record

Abstract:

If we generate elimination from introduction rules, or, conversely, introduction rules from elimination rules according to a general pattern, we often observe a rise in level: To introduction rules that are just production rules, there correspond elimination rules that discharge assumptions, and vice versa. In a previous publication we showed that this situation cannot always be avoided, i.e., that elimination and introduction rules cannot always be ‘flattened’. More precisely, we showed that there are connectives with given introduction rules which do not have corresponding elimination rules in standard natural deduction, and vice versa. In this paper we generalise this result: Even if we allow for rules of higher levels, i.e. rules that may discharge rules used as assumptions, the level rise is often necessary. For every level n we can find a connective with introduction rules of level n, whose corresponding elimination rules must at least have level n+1, and a connective with elimination rules of level n, whose corresponding introduction rules must at least have level n+1.

This item appears in the following Collection(s)