Re: Play "Stump the Intuitionists!"

On 10 Jan 2009 05:40:31 -0800, Daryl McCullough wrote:

I'm not mistaken, (~P -> P) -> P is not int-valid.

You can let P == Av~A. Then ~(Av~A) is a contradiction.

I guess, you meant it implies _|_, right? With other words,

~(A v ~A) -> _|_
~~(A v ~A)

is a theorem in int. logic. But how can we _prove_ that? (Well, Glivenko's
theorem comes to mind. Did you invoke it here?)

Anyway, then ~(Av~A) -> _|_ and _|_ -> Av~A would give ~(Av~A) -> Av~A.

So ~(Av~A) -> Av~A. So the [formula] (~P -> P) -> P implies
excluded middle.

Ah, nice.