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

DSpace Repository

Show simple item record

dc.contributor.author Olkhovikov, Grigory K.
dc.contributor.author Schroeder-Heister, Peter
dc.date.accessioned 2022-08-16T11:41:28Z
dc.date.available 2022-08-16T11:41:28Z
dc.date.issued 2014
dc.identifier.isbn 978-884674033-5
dc.identifier.uri http://hdl.handle.net/10900/130949
dc.identifier.uri http://nbn-resolving.de/urn:nbn:de:bsz:21-dspace-1309499 de_DE
dc.identifier.uri http://dx.doi.org/10.15496/publikation-72309
dc.description.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. en
dc.language.iso en de_DE
dc.publisher Universität Tübingen de_DE
dc.rights ubt-podok de_DE
dc.rights.uri http://tobias-lib.uni-tuebingen.de/doku/lic_mit_pod.php?la=de de_DE
dc.rights.uri http://tobias-lib.uni-tuebingen.de/doku/lic_mit_pod.php?la=en en
dc.subject.classification Beweistheorie , Logische Partikel , Kalkül des natürlichen Schließens de_DE
dc.subject.ddc 004 de_DE
dc.subject.ddc 100 de_DE
dc.subject.other Beweistheoretische Semantik de_DE
dc.subject.other Proof Theory en
dc.subject.other Logical Constant en
dc.subject.other Natural Deduction en
dc.subject.other Proof-theoretic Semantics en
dc.title Proof-theoretic harmony and the levels of rules: Generalised non-flattening results en
dc.type Article de_DE
utue.publikation.fachbereich Informatik de_DE
utue.publikation.fakultaet 7 Mathematisch-Naturwissenschaftliche Fakultät de_DE
utue.publikation.source Second Pisa Colloquium in Logic, Language and Epistemology. Ed. by Enrico Moriconi and Laura Tesconi. Pisa: Edizioni ETS 2014, pp. 245-287 de_DE
utue.publikation.noppn yes de_DE

Dateien:

This item appears in the following Collection(s)

Show simple item record