Equivalence between fragments of intuitionistic and classical logics

Question

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?

Answer 1

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.

Answer 2

Additionally to Henning's answer:

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).

Answer 3

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