Failure of Completeness in Proof-Theoretic Semantics
| LEADER | caa a22 4500 | ||
|---|---|---|---|
| 001 | 605539030 | ||
| 003 | CHVBK | ||
| 005 | 20210128100905.0 | ||
| 007 | cr unu---uuuuu | ||
| 008 | 210128e20150601xx s 000 0 eng | ||
| 024 | 7 | 0 | |a 10.1007/s10992-014-9322-x |2 doi |
| 035 | |a (NATIONALLICENCE)springer-10.1007/s10992-014-9322-x | ||
| 245 | 0 | 0 | |a Failure of Completeness in Proof-Theoretic Semantics |h [Elektronische Daten] |c [Thomas Piecha, Wagner de Campos Sanz, Peter Schroeder-Heister] |
| 520 | 3 | |a Several proof-theoretic notions of validity have been proposed in the literature, for which completeness of intuitionistic logic has been conjectured. We define validity for intuitionistic propositional logic in a way which is common to many of these notions, emphasizing that an appropriate notion of validity must be closed under substitution. In this definition we consider atomic systems whose rules are not only production rules, but may include rules that allow one to discharge assumptions. Our central result shows that Harrop's rule is valid under substitution, which refutes the completeness conjecture for intuitionistic logic. | |
| 540 | |a Springer Science+Business Media Dordrecht, 2014 | ||
| 690 | 7 | |a Proof-theoretic semantics |2 nationallicence | |
| 690 | 7 | |a Intuitionistic logic |2 nationallicence | |
| 690 | 7 | |a Mints's rule |2 nationallicence | |
| 690 | 7 | |a Harrop's rule |2 nationallicence | |
| 690 | 7 | |a Completeness |2 nationallicence | |
| 700 | 1 | |a Piecha |D Thomas |u Department of Computer Science, University of Tübingen, Sand 13, 72076, Tübingen, Germany |4 aut | |
| 700 | 1 | |a de Campos Sanz |D Wagner |u Faculdade de Filosofia, Campus II, Universidade Federal de Goiás, 74001-970, Goiânia, GO, Brasil |4 aut | |
| 700 | 1 | |a Schroeder-Heister |D Peter |u Department of Computer Science, University of Tübingen, Sand 13, 72076, Tübingen, Germany |4 aut | |
| 773 | 0 | |t Journal of Philosophical Logic |d Springer Netherlands |g 44/3(2015-06-01), 321-335 |x 0022-3611 |q 44:3<321 |1 2015 |2 44 |o 10992 | |
| 856 | 4 | 0 | |u https://doi.org/10.1007/s10992-014-9322-x |q text/html |z Onlinezugriff via DOI |
| 898 | |a BK010053 |b XK010053 |c XK010000 | ||
| 900 | 7 | |a Metadata rights reserved |b Springer special CC-BY-NC licence |2 nationallicence | |
| 908 | |D 1 |a research-article |2 jats | ||
| 949 | |B NATIONALLICENCE |F NATIONALLICENCE |b NL-springer | ||
| 950 | |B NATIONALLICENCE |P 856 |E 40 |u https://doi.org/10.1007/s10992-014-9322-x |q text/html |z Onlinezugriff via DOI | ||
| 950 | |B NATIONALLICENCE |P 700 |E 1- |a Piecha |D Thomas |u Department of Computer Science, University of Tübingen, Sand 13, 72076, Tübingen, Germany |4 aut | ||
| 950 | |B NATIONALLICENCE |P 700 |E 1- |a de Campos Sanz |D Wagner |u Faculdade de Filosofia, Campus II, Universidade Federal de Goiás, 74001-970, Goiânia, GO, Brasil |4 aut | ||
| 950 | |B NATIONALLICENCE |P 700 |E 1- |a Schroeder-Heister |D Peter |u Department of Computer Science, University of Tübingen, Sand 13, 72076, Tübingen, Germany |4 aut | ||
| 950 | |B NATIONALLICENCE |P 773 |E 0- |t Journal of Philosophical Logic |d Springer Netherlands |g 44/3(2015-06-01), 321-335 |x 0022-3611 |q 44:3<321 |1 2015 |2 44 |o 10992 | ||