# Equivalence between fragments of intuitionistic and classical logics

Is the fragment $\{\vee,\land,\Rightarrow\}$ (no $\neg$) of intuitionistic propositional logic equivalent to the corresponding fragment of classical propositional logic, i.e. a formula is intuitionistic provable iff it is classically valid? If yes, where can I find such a proof?

Classical and intuitionistic propositional logic do not prove the same formulas, even in the purely implicational fragment.

Most famously, Peirce's Law $((P\to Q)\to P)\to P$ is a classical tautology, but is not intuitionistically valid. (That is, classical logic proves it, but intuitionistic logic doesn't).

The two logics are equivalent for the $\{\land,\lor\}$ fragment, though. In terms of which formulas are theorem of the pure calculus, this is not very interesting (because no formula in the $\{\land,\lor\}$ fragment are theorems), but it also holds if you consider non-empty theories: Classical and intuitionistic entailment coincide for this fragment.

See this question which shows that the only change to the classical sequent calculus LK that is necessary to get intuitionistic logic instead is to the ${\to}R$ rule. However a cut-free proof in the sequent calculus never uses rules for connectives that don't appear in the conclusion, so the valid (cut-free) proofs in the classical LK for conclusions in the $\{\land,\lor\}$ fragment are the same as the valid proofs in the intuitionistic variant.

• "The two logics are equivalent for the {∧,∨}{∧,∨} fragment, though." There don't exist any theorems in that fragment. Note that the question makes reference to a formula as "proofable" [sic]. So, yes, they are equivalent. Nov 17, 2015 at 15:55
• @DougSpoonwood: They are also equivalent in the non-vacuous sense that their entailment relations are the same for this fragment. Nov 17, 2015 at 15:56

Usually you have at least some expression in your logic expressing "contradiction", for example $0=1$ in Heyting Arithmetic. Then you immediately get all of intuitionistic logic by setting $\neg a :\equiv a \Rightarrow (0 = 1)$, so removing $\neg$ usually does not change anything.

If you don't have contradiction already, you can just "adjoin" it in the same fashion you add an $-\infty$ to the lattice of reals (and more generally: a least element to a poset or initial object to a category).

• Also if I have no constants? Like just propositional variables and connectives, not bottom, etc. can I still express contradiction then? Thanks for your answer anyway! Nov 17, 2015 at 15:57
• @fweth: If all you have is $\{\land,\lor,\to\}$ and no constants, then you cannot express negation even classically -- because every expression you can build with those connectives will evaluate to true when all the variables in it are true. Nov 17, 2015 at 16:00
• I also think I can't express negation classically, but still not every formula is valid. $A$ is not classically valid but e.g. $A\Rightarrow A$ is. Nov 17, 2015 at 16:05

I use Polish notation.

The formation rules go:

1. All lower case letters of the Latin alphabet qualify as significant expressions.
2. If $\alpha$ and $\beta$ qualify as significant expressions, then so do N$\alpha$, C$\alpha$$\beta, A\alpha$$\beta$, and K$\alpha$$\beta$.

The significant expression CApqCCpqq can get proved in intuitionistic logic from the axiom set {

1. CpCqp
2. CCpCqrCCpqCpr
3. CpApq
4. CpAqp
5. CCpqCCrqCAprq
6. CKpqp
7. CKpqq
8. CpCqKpq
9. CpCNpq
10. CCpNqCqNp

} under uniform substitution and detachment.

However, CCCpqqApq, which does hold in classical logic, cannot get proved since the following model satisfies the above 10 axioms but does not satisfy CCCpqqApq according to Mace4. Thus, the fragment {A, K, C} of intuitionistic logic is not equivalent to the fragment {A, K, C} of classical logic:

A   0   1   2
0   0   0   2
1   0   1   2
2*  2   2   2

C   0   1   2
0   2   1   2
1   2   2   2
2   0   1   2

K   0   1   2
0   0   1   0
1   1   1   1
2   0   1   2

N
0  1
1  2
2  1