equal
deleted
inserted
replaced
24 text\<open>Metatheorem (for \emph{propositional} formulae): |
24 text\<open>Metatheorem (for \emph{propositional} formulae): |
25 $P$ is classically provable iff $\neg\neg P$ is intuitionistically provable. |
25 $P$ is classically provable iff $\neg\neg P$ is intuitionistically provable. |
26 Therefore $\neg P$ is classically provable iff it is intuitionistically |
26 Therefore $\neg P$ is classically provable iff it is intuitionistically |
27 provable. |
27 provable. |
28 |
28 |
29 Proof: Let $Q$ be the conjuction of the propositions $A\vee\neg A$, one for |
29 Proof: Let $Q$ be the conjunction of the propositions $A\vee\neg A$, one for |
30 each atom $A$ in $P$. Now $\neg\neg Q$ is intuitionistically provable because |
30 each atom $A$ in $P$. Now $\neg\neg Q$ is intuitionistically provable because |
31 $\neg\neg(A\vee\neg A)$ is and because double-negation distributes over |
31 $\neg\neg(A\vee\neg A)$ is and because double-negation distributes over |
32 conjunction. If $P$ is provable classically, then clearly $Q\rightarrow P$ is |
32 conjunction. If $P$ is provable classically, then clearly $Q\rightarrow P$ is |
33 provable intuitionistically, so $\neg\neg(Q\rightarrow P)$ is also provable |
33 provable intuitionistically, so $\neg\neg(Q\rightarrow P)$ is also provable |
34 intuitionistically. The latter is intuitionistically equivalent to $\neg\neg |
34 intuitionistically. The latter is intuitionistically equivalent to $\neg\neg |