Paradoxes of higher-order logic
Russell Wallace
one to write inconsistent statements. But are there any that allow one
to start off with only true statements and derive a falsehood?
For example, Curry's paradox; the version I've seen defines Y =
(^y.yy => X)(^y.yy => X) and then writes Y |- Y, which translates as
"if we were given Y, then we could derive Y", and goes on from there
to derive a contradiction.
But Y has no truth value (its computation is nonterminating), so that
amounts to "if we start off by asserting that undefined equals true,
then we can derive a contradiction". This should not be surprising!
Are there any variants that derive a contradiction without having to
use any untrue statements as axioms?
Luke Palmer
I'm not sure what you mean. Y |- Y doesn't use Y as an axiom. The
axiom is, for all propositions x, x |- x: if you assume x, then you
can derive x. It's an obvious judgement.
I suspect that not allowing any "untrue" statements on the left of the
turnstile would result in a fantastically unpowerful logic. Phrasing
a sentence such as "if there are infinitely many twin primes, then
..." would be illegal, since you would first have to know that the
antecedent is true.
Along this line, you might be interested in Bunder's System IΞ. He
blocks Curry's paradox, as well as many others, by introducing a new
symbol "H", such that "HX" means "X is a well-formed proposition".
So, it can be true or false or unprovable, but it's got to mean
something. Y above is meaningless, and in IΞ, HY is not derivable,
and the system's rules thus prevent it from being generalized over.
I gave an introduction to the system on my blog:
http://lukepalmer.wordpress.com/2009/04/12/some-constructions-in-ixi/.
Martin Bunder has a bunch of work on this and related systems.
"Systems of Illative Combinatory Logic complete for First Order
Predicate Calculus" is a good place to start:
http://repository.ubn.ru.nl/bitstream/2066/17259/1/13276.pdf
Luke
Russell Wallace
> I'm not sure what you mean. Y |- Y doesn't use Y as an axiom. The
> axiom is, for all propositions x, x |- x: if you assume x, then you
> can derive x. It's an obvious judgement.
>
> I suspect that not allowing any "untrue" statements on the left of the
> turnstile would result in a fantastically unpowerful logic. Phrasing
> a sentence such as "if there are infinitely many twin primes, then
> ..." would be illegal, since you would first have to know that the
> antecedent is true.
Well, I'll explain where I'm coming from; I'm trying to write an
automated theorem prover for higher-order logic. Now the most
important property of an automated theorem prover is that it be sound,
which is to say, if the statements you feed into the program are all
true it should never derive a contradiction. But the turnstile symbol
is not part of an automated theorem prover's input language, so proofs
that contain the turnstile symbol cannot directly demonstrate
unsoundness. That's why I'm asking whether there's an unsoundness
generating paradox that does not use the turnstile symbol.
And thanks for the references! Abram Demski gave me a link to your
blog while he was inviting me to this list, so the page you mentioned
and a link to the PDF were what I had in front of me when I was
discussing Curry's paradox :-) ixi strikes me as being on the right
lines, but I can't be sure until I have a use case in a form that a
computer could process.
YKY (Yan King Yin, 甄景贤)
1986] "Intro to Combinators and lambda-Calculus" has chapter 17
devoted to "Logic based on combinators". You may have a look, but
it's from the 1980s.
YKY
Russell Wallace
conversation last night; I think this is also consistent with what
Luke Palmer is doing with ixi. Relevant section of log:
YKY: you let Y be "Santa Claus exists"
then let X = X -> Y
then run the Curry paradox
me: unsoundness is when you feed a theorem prover a set of
statements all of which are true, and it derives a contradiction. I
haven't yet seen a demonstration of how that would happen
YKY: you can feed it with "X = X -> Y"
and then ask for the truth of Y
me: so the statements you would input are X = X -> Y, and ~Y
YKY: it will probably return True
yeah i guess....
can you try it now :)
me: thanks! I'll have another go at analyzing it from that, then
YKY: ok...
Sent at 4:51 AM on Monday
me: given that, the logic does seem unassailable, at least by the usual rules
consider this statement: x -> x
YKY: really?
me: that translates into ~x | x
YKY: maybe that doesn't work in LC..
me: which in ordinary Boolean logic is correct
however, once we have computational completeness, then it stops being true
YKY: what do you mean?
me: because there is also the undefined value: a nonterminating
computation does not have a value either true or false
and x is a nonterminating computation
so the statement x -> x is not actually true
YKY: but we start with X = X -> Y
x -> x is actually true!
you can negate it to get... ~x ^ x
me: x = x -> y is true, because they are both undefined
YKY: and then you get the null clause
me: but I don't understand what you're saying here about x -> x
YKY: x -> x is a tautology
ie, it can be proven to be true
me: how do you go about proving it, given that x is neither true nor false?
YKY: you just negate it first
so that's ~ (x | ~x)
me: Yeah but
the same issue arises
YKY: whether x is given or not is irrelevant
me: we are no longer working in an environment where refuting
p=false allows us to conclude p=true
because there is also the possibility p= nonterminating
YKY: are you using intuitionistic
me: so the fact that you can derive a contradiction by negating x ->
x, does not imply x -> x is true in all circumstances
YKY: where does the concept of nonterminating come from?
me: I don't know what intuitionistic means in this context. the
concept of nonterminating comes from Turing completeness
YKY: i see..
me: and x is in fact nonterminating
YKY: but why don't you use proof-by-refutation?
me: well I have been up till now. But now I see there is a problem with it
YKY: what's the problem?
me: proof by refutation assumes that if you can refute p=false then
you can conclude p=true
YKY: yeah
that's OK
me: but once we are dealing with Turing complete formalism, it is not okay
YKY: how so?
me: because there is a third possibility, p= nonterminating
YKY: can you give an example of a nonterminating thing?
me: yes, x is such an example
or, any translation of infinite recursion into lambda calculus
YKY: like x = x?
me: that is an example of non-termination, yes
YKY: hmmm... i dont understand why x alone is nonterminating
me: look at the full definition and try to evaluate it
you'll find it gets into infinite regression
YKY: so x ^ ~x is terminating then?
me: if x alone terminates, then x & ~x also terminates, yes
YKY: what's the full translation of x
?
me: Let Y = (\x. x x ⇒ X) (\x. x x ⇒ X)
from http://lukepalmer.wordpress.com/2009/04/12/some-constructions-in-ixi/
where he uses X and Y the other way around than the other example
but it's the same concept
brb
YKY: hmmmm looks very complicated...
Sent at 5:17 AM on Monday
YKY: oh, so terminating mean H x?
Sent at 5:20 AM on Monday
YKY: that seems to be the correct answer to block curry paradox...
Sent at 5:24 AM on Monday
me: yes I think so, that is what he seems to mean by H - I'm
guessing he chose the letter to stand for "halting", which is a
synonym of terminating
Sent at 5:32 AM on Monday
me: and it seems to me from what I understand so far of what he is
doing with ixi, that this is the correct answer
Sent at 5:34 AM on Monday
me: I might copy the relevant sections of this conversation log to
the one logic mailing list, if that's okay with you, since it seems
relevant to ixi
Sent at 5:35 AM on Monday
YKY: Yeah you can quote my chat to the lists :)
Sent at 3:30 PM on Monday