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

DSpace Repository


Dokumentart: Aufsatz
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: Publishing license including print on demand
Order a printed copy: Print-on-Demand
Show full item record


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)