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) -> _|_
or
~~(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.


Herb
.

Relevant Pages

  • Re: Critique
    ... I invoke the program with an int ... > representing a site code and a long representing a date and my ... > with the int and the long I pass in. ... Since you already have a template file, ...
    (comp.lang.c)
  • Re: [MSDOS] Trouble with mouse programming
    ... >> which not only consume a lot of stack but probably also invoke ... All that int 29h does is to invoke the int 10h ... and forgetting a declaration when calling it. ...
    (comp.programming)
  • Re: REFERENCES REVEALED
    ... > int main ... that the same is not true of pointers. ... address of that object with that label. ... It's good that you have something in mind that gives you a better ...
    (comp.lang.cpp)
  • Re: Endless Dorkness
    ... Mind blast 1/day, Int vs Will, stunned on hit, save ends ... use differing judgements. ...
    (rec.games.frp.dnd)
  • Re: Endless Dorkness
    ... Mind blast 1/day, Int vs Will, stunned on hit, save ends ... Very dangerous candy and not safe to get close to, ...
    (rec.games.frp.dnd)