Embedding classical in minimal implicational logic

Ishihara, Hajime and Schwichtenberg, Helmut (2016): Embedding classical in minimal implicational logic. In: Mathematical Logic Quarterly, Vol. 62, No. 1-2: pp. 94-101

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-Blackwell Verlag GmbH & Co. KGaA, Weinheim

• Item Type: Journal article
• Faculties: Mathematics, Computer Science and Statistics > Mathematics
• Subjects: 500 Science > 510 Mathematics
• ISSN: 0942-5616
• Language: English