Re: Play "Stump the Intuitionists!"
- From: Herbert Newman <nomail@invalid>
- Date: Sat, 10 Jan 2009 20:17:58 +0100
On 10 Jan 2009 05:40:31 -0800, Daryl McCullough wrote:
I guess, you meant it implies _|_, right? With other words,You can let P == Av~A. Then ~(Av~A) is a contradiction.
I'm not mistaken, (~P -> P) -> P is not int-valid.
~(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 impliesAh, nice.