Proof-Theoretic Harmony: The Issue of Propositional Quantification

DSpace Repository


Dateien:

URI: http://hdl.handle.net/10900/130967
http://nbn-resolving.de/urn:nbn:de:bsz:21-dspace-1309676
http://dx.doi.org/10.15496/publikation-72327
http://nbn-resolving.org/urn:nbn:de:bsz:21-dspace-1309678
Dokumentart: Article
Date: 2014
Source: Trends in Logic XIII. Gentzen's and Jaśkowski's Heritage. 80 Years of Natural Deduction and Sequent Calculi. Ed. by Andrzej Indrzejczak, Janusz Kaczmarek and Michał Zawidzki. Łódż University Press 2014, pp. 5-15
Language: English
Faculty: 7 Mathematisch-Naturwissenschaftliche Fakultät
Department: Informatik
DDC Classifikation: 004 - Data processing and computer science
100 - Philosophy
Keywords: Logik , Beweistheorie
Other Keywords: Beweistheoretische Semantik
Propositionale Quantifikation
Proof-theoretic Semantics
Propositional Quantification
Proof Theory
Logic
ISBN: 978-83-7969-161-6
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:

We present our calculus of higher-level rules, extended with propositional quantification within rules. This makes it possible to present general schemas for introduction and elimination rules for arbitrary propositional operators and to define what it means that introductions and eliminations are in harmony with each other. This definition does not presuppose any logical system, but is formulated in terms of rules themselves. We therefore speak of a foundational (rather than reductive) account of proof-theoretic harmony. With every set of introduction rules a canonical elimination rule, and with every set of elimination rules a canonical introduction rule is associated in such a way that the canonical rule is in harmony with the set of rules it is associated with. An example given by Hazen and Pelletier is used to demonstrate that there are significant connectives, which are characterized by their elimination rules, and whose introduction rule is the canonical introduction rule associated with these elimination rules. Due to the availability of higher-level rules and propositional quantification, the means of expression of the framework developed are sufficient to ensure that the construction of canonical elimination or introduction rules is always possible and does not lead out of this framework.

This item appears in the following Collection(s)