Re: did Godel prove Incompleteness or did he disprove Excluded Middle?

From: David C. Ullrich (ullrich_at_math.okstate.edu)
Date: 06/29/04 

Date: Tue, 29 Jun 2004 06:57:26 -0500

On Tue, 29 Jun 2004 11:35:54 +0300, Aatu Koskensilta
<aatu.koskensilta@xortec.fi> wrote:

>David C. Ullrich wrote:
>> On Mon, 28 Jun 2004 18:27:15 +0300, Aatu Koskensilta
>> <aatu.koskensilta@xortec.fi> wrote:
> >
>>>The constructivistic interpretation of ~P is P->False, where False is
>>>e.g. 0=1. So if you assume P and derive a contradiction, you have
>>>provided a transformation f that transforms any proof p of P into a
>>>proof f(p) of absurdity, i.e. you have proved P->False, but this is just
>>>~P. This is what we use in the proof above to derive ~P from f(A)!=f(B).
>>
>>
>> Huh^2.
>
>Hopefully Frege's answers clarified the situation for you.

Maybe just saying "Huh" wasn't clear. I didn't mean to say I
was confused, just "Huh, that's interesting."

Which is not to say that I understood all the details that
you explained to him and explain below - I didn't really
feel any need to follow every detail, I was just curious,
and what you said was sufficient to convince me that the
answer to my question was yes. (Which suprised me, hence
the "Huh".)

>They should
>convince that the proof I presented is intuitionistically valid, in any
>case. What I tried to do above was to explain why proof by contradiction
>is constructively valid, while the rule
>
> ~p
> .
> .
> False
> -----
> p
>
>is not.
>
>The basic idea is as follows. Constructive interpretation of logic is
>based on the idea that that asserting P is (usually) an incomplete way
>of saying that P has a proof, i.e. the following schema holds
>
> P <-> P has a constructive proof
>
>Of course here "proof" can't mean proof in any specific formal system.
>Elaborating on this would lead us to the muddy waters, so I'll just go on.
>
>Every true atomic statement, such as 0=0 or (1+1)+(1+1) = 1+1+1+1, is a
>proof of itself.
>
>A proof of A&B is a pair (a,b) such that a is a proof of A and b is a
>proof of B.
>
>A proof of A\/B is a pair (n,p) such that if n=0 then p is a proof of A
>and if n=1 then p is a proof of B.

Since you insist on clarifying things<g>, I'm not sure what this
means. Is n something like a random variable? What is n, exactly?

Or is what you mean equivalent to saying just

"A proof of AvB is a proof of (n=0 -> A) & (n=1 -> B)"?

I know what _that_ means...

>A proof of A->B is a constructive function f which transforms every
>proof of A into a proof of B. This is a point of controversy - or was
>when I last checked, at least - since intuitively it seems that we
>should actually require that a proof of A->B be a pair (p,f) such that f
>is a function transforming every proof of A into B and p is a proof of
>this fact. For how could the constructive function alone convince us of
>A->B? It could be immensely complicated and depend on all sorts of
>mathematical facts which we don't know. On the other hand, it's not
>clear what notion of proof should be used when defining what proof of
>A->B means, at least if we wish to avoid circularity. Again, I won't
>elaborate on these subtleties here.

Was "On the other hand, it's not clear what notion of proof should
be used when defining what proof of A->B means" actually supposed
to be "On the other hand, it's not clear what notion of proof
should be used when defining what a proof that f transforms every
proof of A into a proof of B means"?

>A proof of ~A is a proof of A->False, where False is some absurd
>proposition. This should immediatedly render obvious why proof by
>contradiction is valid. For if you have proved some absurd proposition
>assuming A, i.e.
>
> A
> .
> . (k)
> .
> False
>
>then obviously you have provided a constructive function to transform
>every proof of A into a proof of absurdity, since given a proof t of A
>you can just expand it into a proof of absurdity:
>
> .
> . (t)
> .
> A
> .
> . (k)
> .
> False
>
>By the definition of proof of A->False, you have a proof of A->False.
>But by definition, ~A = A->False, so you have proved ~A.
>
>Let's then consider the case where you assume ~A and derive an
>absurdity. You have obviously provided a constructive function which
>transforms any proof of ~A into a proof of ~A->False, i.e. ~~A. But
>~A->False = (A->False)->False, i.e. a constructive function transforming
>any proof of (A->False) - i.e. a constructive function transforming any
>proof of A into a proof of absurdity - into a proof of absurdity. But
>this doesn't usually give you a proof of A, since you can't in general
>actually extract such a proof from a proof of (A->False)->False, which
>is why rule
>
> ~p
> .
> .
> False
> -----
> p
>
>is not constructively valid. As a rule of thumb one might say that it's
>perfectly OK to derive negative conclusions by a proof of contradiction
>in constructive logics, but positive conclusions do not always follow
>from proofs by contradiction even where they would in classical logic.

************************

David C. Ullrich

Relevant Pages

  • Re: did Godel prove Incompleteness or did he disprove Excluded Middle?
    ... What I tried to do above was to explain why proof by contradiction ... A proof of A->B is a constructive function f which transforms every ... you can just expand it into a proof of absurdity: ...
    (sci.logic)
  • Re: Yusef Islam Nominated for RNR HAll
    ... >> in your whacko assertion that Linda R's dated cover versions will ... Now, THAT is an absurdity. ... LOL! ... > saying what you wanted me to be saying. ...
    (rec.music.beatles)
  • Re: More lies from Wally
    ... What is your problem with my noting the absurdity of someone ... saying they agree with parts of something they claimed to not ... exist Snit, so in as much as "It" is merely one of your delusions I have no ... quote the comment that Tim Adams made it is always in an abbreviated form.. ...
    (comp.sys.mac.advocacy)
  • Re: The Nanometre Twin
    ... absurdity somehow somewhere is because you still ... that is a *mathematical* contradiction. ... That's the beauty of mathematics, ... clocks respond to motion. ...
    (sci.physics.relativity)
  • Re: More lies from Wally
    ... What is your problem with my noting the absurdity of someone ... saying they agree with parts of something they claimed to not ... There would be nothing wrong in anyone doing as you suggest Snit, ...
    (comp.sys.mac.advocacy)