paradoxes and intuitionist logic

[btanksley@hifn.com]

>From: iepos@tunes.org [mailto:iepos@tunes.org]
>Subject: paradoxes and intuitionist logic

>i've been doing a bit of thinking about the paradoxes and haven't
>come to any really good answers and am wondering if any of you have.

>one of the most paradoxes occurs when reasoning on a statement
>that says "this statement is not true". One first supposes that it
>is true; then it follows that it is not true. This is a contradiction,
>so the assumption must have been not true. So, the statement is not
>true; but this is precisely what the statement says, so we have
>admitted the statement. So there is an inconsistency in this logic.
>Unfortunately, the inconsistency is not caused merely by the funny
>nature of the English language; the argument can be formalized in
>a fairly simple sound-appearing logic using the Y combinator (or
>lambda term) to achieve the self-reference.

Only if you fail to typecheck your variables.

>I: x -> x 
>B: (x -> y) -> (z -> x) -> z -> y
>C: (x -> y -> z) -> y -> x -> z
>W: (x -> x -> y) -> x -> y
>K: x -> y -> x

The trouble is, what are you allowed to substitute for the variables?
Obviously, you can only substitute things which have possible boolean
answers (as an example, you can't set x to any natural number and expect
anything to make sense).  Paradoxes cannot have boolean answers, so
substituting them into these laws is simply ignoring type safety.

Things which can be substituted into these laws are called 'propositions'.

>- iepos

-Billy