src/FOL/ex/Intuitionistic.thy
 changeset 69591 cc6a21413f8a parent 69590 e65314985426 child 69593 3dda49e08b9d
equal inserted replaced
69590:e65314985426 69591:cc6a21413f8a
    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