Re: Cantor diagonal argument and intuitionistic logic

"Torkel Franzen" <torkel@xxxxxxxxxx> wrote in
: "LordBeotian" <pokispy76@[CANCELLA QUESTO]yahoo.it> writes:
:
: > But how can it be proved without the excluded middle low?
: > Isn't it a proof "by contraddiction"?
: > And aren't proof by contraddiction rejected by intuitionism?
:
: This has been commented on many times in the group.
:
: "Proof by contradiction" in the sense of concluding A after deriving a
: contradiction from not-A (also known as "classical reductio" or
: "indirect proof") is not constructively valid.
:
: "Proof by contradiction" in the sense of concluding not-A after
: deriving a contradiction from A is constructively valid, and is the
: direct way of proving a negation.
:
: Diagonalization only involves "proof by contradiction" in the
: latter, constructively valid sense.

Torkel is a true believer that the problem, "what numbered box contains
the numbers of all the boxes that don't contain their own number", having
no answer, establishes a hyperplane of intractable super dense higher infinities.

Don't you Torkel?

Herc



.

Relevant Pages

  • Re: Cantor diagonal argument and intuitionistic logic
    ... "Proof by contradiction" in the sense of concluding A after deriving a ... "indirect proof") is not constructively valid. ... "Proof by contradiction" in the sense of concluding not-A after ... deriving a contradiction from A is constructively valid, ...
    (sci.logic)
  • Re: "Friendly Premises"
    ... >Your posts are teetering towards contradiction. ... >suppressed that link because it undermines their/our/whatever point. ... At least Torkel knew it was coming. ... Don't forget, there are readers. ...
    (sci.logic)
  • Re: Uncountable sets in CZF?
    ... You don't need excluded middle or negation elimination for this ... but I didn't realize you CAN prove -A by deriving a contradiction from ...
    (sci.math)
  • Re: Hans startling new set theory.
    ... >>> Assuming that there is a set satisfying a particular definition and ... >>> then deriving a contradiction does indeed prove that no such set ... You're babbling here. ...
    (sci.math)
Quantcast