how does type theory block Liar's paradox?

[YKY (Yan King Yin, 甄景贤)]

Hi Abram,

Do you know specifically how types block the Liar's paradox?

I heard that this solution is not particularly satisfying.

And if so, typed systems such as HOL Light may not be satisfactory KR
languages for AGI?

YKY

[Abram Demski]

YKY,

Let Y be the Y combinator, ie,

Y f ==> f (Y f)

This allows us to write recursive functions, and can be defined in
lambda calculus. Specifically, 'f' can be written as a function of
multiple arguments wherein we act as if the first argument stands for
the function itself. For example, if we'd normally define factorial as
follows:

Factorial(x) =
if x==1, 1; else x * Factorial(x-1)

We can define it as follows:

Factorial =
\ w x . if x==1, 1; else x * (w (x - 1))

Of course, I am mixing notations here, since if/then/else is not a
part of lambda calculus. Anyway, now construct a predicate F that
given a sentence, claims the sentence is false:

F:
\ x. x = false

Now put Y in front of it:

Y F

This is the liar sentence, since it claims itself to be false:

Y F ==> F (Y F)

One property of the sort of typing system that is used to block this
sort of paradox is that it guarantees that the evaluation of any
well-typed statement will terminate; the above expression never does,
so no such typing system will allow it!

Y F ==> F (Y F) ==> F (F (Y F)) ==> ...

The reason this is not satisfying is the standard reason that applies
to any "solution" of the liar paradox: the system will have holes in
its referential capability. It won't be able to construct its own
semantics. This sort of system will contain a truth predicate, "\ x .
x = true", but not a "well-typed-ness" or "meaningfulness" predicate
(so we can't say "this statement is either false or meaningless").

Of course, in the case if ixi, we *do* have a "meaningfulness"
predicate... but we have other restrictions to avoid paradox...

--Abram

2009/9/23 YKY (Yan King Yin, 甄景贤) <generic.in...@gmail.com>:

--
Abram Demski
http://dragonlogic-ai.blogspot.com/
http://groups.google.com/group/one-logic

[Abram Demski]

YKY,

Also, the more specific reason that type theory is unsatisfactory
(which Russel and I have been talking about a little) is that a typing
system destroys the turing-completeness of the underlying formalism
(lambda calculus).

The seriousness of the concern arises from the fact that such typing
systems require a function to be well-typed *before* it is applied to
an argument. Proving that functions always terminate is an endeavor
doomed to incompleteness, so the expressions we can use is necessarily
a subset of the meaningful expressions.

If we accept proofs of termination, we're still doomed to
incompleteness in proving functions always-meaningful (and thus, for
example, limited in ascribing meaningfulness to universal
quantifications); however, as I understand it, we lose the limitations
on ascribing meaningfulness to pure lambda functions of the provably
meaningful statements. If an expression evaluates to something
meaningful, it's meaningful, period.

Question: when is an equality statement meaningful? Is it always
meaningless to compare partial functions (by which I mean functions
whose computations don't terminate for all their values)? Do we take
the convention that (meaningless = meaningless) = true?

--Abram

2009/9/23 YKY (Yan King Yin, 甄景贤) <generic.in...@gmail.com>:
>

[Russell Wallace]

On Thu, Sep 24, 2009 at 1:54 AM, Abram Demski <abram...@gmail.com> wrote:
> Question: when is an equality statement meaningful? Is it always
> meaningless to compare partial functions (by which I mean functions
> whose computations don't terminate for all their values)?

Mmm? Surely, for example, the reciprocal function is perfectly
meaningful, as long as you don't call it on zero?

> Do we take
> the convention that (meaningless = meaningless) = true?

I would be inclined to think so. Specifically, I would be inclined to
define equality in terms of equivalence; a=b iff you can always
substitute one for the other in any term without changing the meaning
of that term. And two nonterminating expressions meet that criterion.

[Abram Demski]

> Mmm? Surely, for example, the reciprocal function is perfectly
> meaningful, as long as you don't call it on zero?

Good one.

I should mention that I know little about typing systems more
complicated than the simply typed lambda calculus. Is there a system
wherein we can construct a type of everything-but-zero, so that the
reciprocal function can be typed?

In such a system, comparing the reciprocal function to a function with
a different domain (say, a doubling function) would simply be
not-well-typed, right? ...

>> Do we take
>> the convention that (meaningless = meaningless) = true?
>
> I would be inclined to think so. Specifically, I would be inclined to
> define equality in terms of equivalence; a=b iff you can always
> substitute one for the other in any term without changing the meaning
> of that term. And two nonterminating expressions meet that criterion.

Sounds suspiciously simple... I think asking for such a nice
definition of equality might be paradoxical.

B = \x. ( (x = meaningless) or (x = false) )

Consider (Y B).

Y B ==> B (Y B) ==> B (B (Y B)) ==> ...

Thus Y B is a nonterminating evaluation, like Y F as defined in my
response to YKY. Therefore, Y B is meaningless, right? But if so, and
if we take (meaningless = meaningless) = true, then...

(Y B) = meaningless

(Y B) = B (Y B)

B (Y B) = B meaningless

B meaningless = true

thus, meaningless = true.

What's the way around this? (This is the standard "strengthened liar" paradox.)

--Abram

[Luke Palmer]

On Wed, Sep 23, 2009 at 10:21 PM, Abram Demski <abram...@gmail.com> wrote:
>
>> Mmm? Surely, for example, the reciprocal function is perfectly
>> meaningful, as long as you don't call it on zero?
>
> Good one.
>
> I should mention that I know little about typing systems more
> complicated than the simply typed lambda calculus. Is there a system
> wherein we can construct a type of everything-but-zero, so that the
> reciprocal function can be typed?

Yes, absolutely. One of the more popular ones is the Calculus of
Inductive Constructions, the calculus that the Coq proof assistant
uses.

>>> Do we take
>>> the convention that (meaningless = meaningless) = true?
>>
>> I would be inclined to think so. Specifically, I would be inclined to
>> define equality in terms of equivalence; a=b iff you can always
>> substitute one for the other in any term without changing the meaning
>> of that term. And two nonterminating expressions meet that criterion.
>
> Sounds suspiciously simple...

Yes, quite suspicious. Extensional equality won't do here, at least I
have some indication why not.

Let's bring in some computable topology jargon. A set is "open" when
there is a program that halts whenever its input is in the set. It
follows that a set is "closed" when there is a program that halts
whenever the input is not in the set.

"Meaningless" statements don't have normal forms in the lambda
calculus; i.e. they are the "non-halting" terms. So, the set of
meaningless terms is closed, where as the set of provable statements
is open. So you can't prove in general that two meaningless
statements are the same (otherwise we could make an open set of them
by picking one canonical example and enumerating proofs).

So (meaningless=meaningless)=true is a nice definition, but it is an
uncomputable one.

[Russell Wallace]

On Thu, Sep 24, 2009 at 5:21 AM, Abram Demski <abram...@gmail.com> wrote:
> What's the way around this? (This is the standard "strengthened liar" paradox.)

Good catch!

So maybe ixi is the solution? I gather it has no known
inconsistencies, and unlike conventional type systems, doesn't
preclude reasoning about arbitrary functions.

Does the standard paramodulation inference rule work in ixi?

[Abram Demski]

Luke,

Well, uncomputability isn't what's concerning me here... that just
means we've got to have an incomplete theory concerning it. What's
worrying me is possible inconsistency.

Right now, I don't understand how ixi escapes paradox while making the
assertion that it's always meaningful to claim that a statement is
meaningful... Shouldn't that open it up to the strengthened liar
paradox? I need to try and work it through to see where it fails.

--Abram

[Luke Palmer]

On Thu, Sep 24, 2009 at 10:37 PM, Abram Demski <abram...@gmail.com> wrote:
>
> Luke,
>
> Well, uncomputability isn't what's concerning me here... that just
> means we've got to have an incomplete theory concerning it. What's
> worrying me is possible inconsistency.
>
> Right now, I don't understand how ixi escapes paradox while making the
> assertion that it's always meaningful to claim that a statement is
> meaningful... Shouldn't that open it up to the strengthened liar
> paradox? I need to try and work it through to see where it fails.

It doesn't. I'm amazed, having checked the extension against this
very paradox. I guess I made an error (hope blinds us sometimes). My
error was probably not using the dependent conjunction, which I use
below: i.e. the one where you can assume a while proving Hb to prove
H(a /\ b).

Seems you have enough experience in logic to have seen it coming.
Thanks for poking at it.

We still have the ixi from Bunder's completeness paper, and we know
it's consistent. Too bad many of my constructions don't work as
smoothly in that one (or at all without axioms).

Here's my proof:

Define a /\ b = Xi H (\c. (a -> b -> c) -> c)

|- H(a /\ b)
|- H(Xi H (\c -> (a -> b -> c) -> c)
|- H(Hc)
Hc |- H((a -> b -> c) -> c)
Hc |- H(a -> b -> c)
Hc |- Ha *
Hc, a |- H(b -> c)
Hc, a |- Hb *
Hc, a, b |- Hc

So to prove H(a /\ b), it suffices to prove Ha and a |- Hb.

Define X = Y(\x. Hx /\ (x -> False)).
So X = HX /\ (X -> False)

|- HX
|- H(HX /\ (X -> False))
|- H(HX)
HX |- H(X -> False)
HX |- HX
HX, X |- H False

Luke

[Russell Wallace]

Thinking a bit more about the way the strengthened liar paradox breaks
extensional equality, trying to get an intuitive feel for the reasons
why so as to be able to see a way around it:

We start off wanting to believe that x=x in all cases, this seems both
necessary and unobjectionable.
By extensional equality, we want to believe this is true even where x
has no normal form.
But nonterminating computations can give different results depending
on which evaluation shortcut you take.
(Can we disallow evaluation shortcuts and insist there is just one
canonical way of evaluating a term? I don't think so, in a sense the
whole point of logic is to allow shortcuts; we already have lots of
systems that just compute things in a canonical order.)
Therefore we actually cannot assume x=x unless x terminates (a
terminating computation always gives the same answer no matter what
evaluation order you use).

Can we then use the inference rule: H(x) |- x=x?
By itself that doesn't help, because it leaves us with the problem of
proving H(x)... but we can't prove anything whatsoever, or do any
inference whatsoever, without being able to substitute equals for
equals! Chicken and egg.

The biological answer to the bird/egg paradox is dinosaurs, which were
the ancestors of birds and which laid eggs without being birds.
Similarly, the most commonly proposed answer to this problem and logic
is a dinosaur: the usual type system, which essentially allows us to
prove H(x) in some cases using a separate, much weaker inference
engine, which does not rely on x=x.
But a dinosaur is no good if you want flight, and the usual typed
lambda calculus is no good if you want general computation.

Suppose we say we are going to use the type system as a bootstrap
rather than a straitjacket. That is, instead of the requirement for
working with x being typed(x), we say that the requirement is a proof
of H(x) by the type system or any other means. The hope would be that
we can bootstrap via typed statements to other statements that are not
typed but can be proven to terminate. Would this help?
If we know we are going to be doing this, is it possible to come up
with a simpler or more integrated system than the usual type system
plus other stuff?
Am I reinventing stuff that has already been done with ixi here?

Also, eventually to reason about programs, it is presumably going to
be necessary to have Quote and Eval.
Quote(x) is perfectly valid regardless of whether x terminates or not.
Presumably we are going to say that Eval(Quote(x)) is only okay if x terminates.
How does that fit into all this?