Name
Abstract | ||
|---|---|---|
Consider the problem which set V of propositional variables suffices for Stab(V) proves(i) A whenever proves(c) A, where Stab(V) := {(sic)(sic)P --> P vertical bar P is an element of V}, and proves(c) and proves(i) denote derivability in classical and intuitionistic implicational logic, respectively. We give a direct proof that stability for the final propositional variable of the (implicational) formula A is sufficient; as a corollary one obtains Glivenko's theorem. Conversely, using Glivenko's theorem one can give an alternative proof of our result. As an alternative to stability we then consider the Peirce formula Peirce(Q, P) := ((Q --> P) --> Q) --> Q. It is an easy consequence of the result above that adding a single instance of the Peirce formula suffices to move from classical to intuitionistic derivability. Finally we consider the question whether one could do the same for minimal logic. Given a classical derivation of a propositional formula not involving., which instances of the Peirce formula suffice as additional premises to ensure derivability in minimal logic? We define a set of such Peirce formulas, and show that in general an unbounded number of them is necessary. (C) 2016 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim |
Year | DOI | Venue |
|---|---|---|
2016 | 10.1002/malq.201400099 | MATHEMATICAL LOGIC QUARTERLY |
Field | DocType | Volume |
Intuitionistic logic,Discrete mathematics,Combinatorics,Satisfiability,Minimal logic,Corollary,Well-formed formula,Mathematics,Propositional variable,Propositional formula,Direct proof | Journal | 62 |
Issue | ISSN | Citations |
1-2 | 0942-5616 | 0 |
PageRank | References | Authors |
0.34 | 0 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Hajime Ishihara | 1 | 220 | 41.93 |
| Helmut Schwichtenberg | 2 | 373 | 44.83 |