Re: Deep Thoughts # 17: Liar Paradox is a Formal Metamathematical Theorem

From: Charlie-Boo (chvol_at_aol.com)
Date: 12/16/04 

Date: 16 Dec 2004 07:52:02 -0800

David C. Ullrich wrote:
> On 13 Dec 2004 04:54:52 -0800, "Charlie-Boo" <chvol@aol.com> wrote:
> >David C. Ullrich wrote:
> >
> >> You _really_ need to work on the irony detector. Truth
> >> and provability are _different_ things - when you define
> >> one to be the other you exhibit amazing ignorance of the
> >> most basic issues.
> >
> >> ************************
> >>
> >> David C. Ullrich
> >
> >The definitions of Turing Machines and Lambda Calculus are very
> >different, too, aren't they?
>
> For heaven's sake, at some point you should just accept that
> you've made a fool of yourself and drop it. I mean you have
> plenty of experience with this phenomenon...

(Only at parties.) You are the one who claimed that what Smullyan and
I are doing is ignorant. I only agreed with Smullyan. (His 4 texts
were the source of many of the theorems that my formalism represents.)

Your statement above concerning the "ignorance" of defining truth
and provability to coincide makes sense only in the context of some
particular system - the system in which they are being defined. That
is exactly what Smullyan is doing. (It sounds to me like you are
trying to retract the statement by substituting an alternate
explanation of what it means - but haven't come up with a meaningful
alternative.)

> Ok. To answer your question: Yes, those two definitions
> are very different.
>
> I can't imagine what your point is.

Two points:

1. Having different definitions doesn't mean that two things are
different.

2. Truth and provability need not be defined with different systems.
They are defined with different systems only because those who describe
them as such just haven't developed a single system for both. The
notion of recursive functions is the one system developed to define the
functionality of both Turing Machines and Lambda Calculus. Likewise,
truth and provability (two sets of sentences) can be formalized within
a single system.

Both your premise (2) and reasoning (1) are wrong. (I could fault you
less for mistake 2 because that, of course, is current conventional
wisdom.)

> (i) If someone asked for the definition of a Turing Machine
> and someone else replied with the definition of the Lambda
> Calculus that person would indeed be exhibiting blithering
> confusion.

Yes! And if they say that any person who is wrong about question A
must have property B, in all fairness, does that mean that if they are
wrong about A then they themself possess property B?

> (ii) On the other hand, it's true that the set of functions
> computable by TM's is the same as the set of functions
> computable by the LC. _Guessing_ what your point might
> be here, I have to point out that truth and provability
> are _not_ equivalent.

What does it mean to say that truth and provability are or are not
equivalent? It depends on the system in which they are being defined.
It is meaningless to talk about truth and provability outside of some
particular system. They coincide in some systems and they don't
coincide in others. (This sounds like more of the ill-formed alternate
explanation of your original statement.)

> (Validity and provability are equivalent. And truth _in
> that one particular model_ is equivalent to provability
> _in that one particular formal system_. A very curious
> formal system, btw, since there's no procedure to recognize
> whether a proof is valid.)

How could something be a proof but not be a valid proof? You seem to
be trying to say either:

1. We cannot recognize if a given sequence of formulas is a proof.
2. We cannot recognize if a given proof proves a given sentence.
3. We cannot recognize if a given sequence of formulas is a proof of a
given sentence.

But none of these is definitely true anyway. Given that the set of
theorems is not r.e. (system N), any of these can be false if the other
two are true.

In any case, it is not curious to Smullyan (or me.) Every
non-axiomatizable theory has a non-recursive proof predicate, assuming
that the sets of (the Godel numbers of) formulas and of proofs are r.e.

Is PA "very curious" because there's no procedure to decide
whether a sentence is a theorem?

By your reasoning, the user of system N, which is non-axiomatizable and
complete, could equally well claim that PA is very curious because its
is axiomatizable but not complete.

The true lesson, of course, is that there is a trade-off. (The same
trade-off that I described in my 2 MetaMathematical Theorems,
actually.) It's not that the true and provable sentences can't be
the same. It is the fact that there are consequences - both good and
bad - if they are the same. After all, determining trade-offs in
formal systems is central to MetaMathematics. "If a system has
property A then it must have property B." Nothing curious about
that.

C-B

"We call a formula F(v1,. . .,vn) correct if for every n-tuple
(a1,...,an), the sentence F(a1,. . .,an) is true. We let N be the
first-order system whose axioms are all the correct formulas (this
includes all logically valid formulas.) Thus, the provable formulas of
N are nothing more than the axioms of N."

Recursion Theory for Metamathematics - Raymond M. Smullyan, 1993

"In applications to semantical systems, T will be the truth set, and
in syntactical systems, T will be the set of theorems." - Theory of
Formal Systems, Chapter III. Incompleteness and Undecidability
> ************************
>
> David C. Ullrich

Relevant Pages

  • Re: Godel, Rosser and Turing in 1 Easy Step - and Why would we want to?
    ... If "x proves y" is expressible, then provability does not coincide ... Note that we now have formal specifications for these theorems. ... Turing Machine a halts yes on input b. ... What has truth to do with arithmetic and logic? ...
    (sci.logic)
  • Re: FOL, ZFC, NGB and Prolog
    ... > tom wrote: ... > (I thought Goedel equated provability and truth). ... I am now going to implement all types of formal systems in Prolog. ...
    (sci.logic)
  • Re: Godels Theorem and Model Theory
    ... Yes, people are animals, and yes, theorems ... stuck imagining that the concept of truth is ... about truth of any kind (but only provability). ...
    (sci.logic)
  • theorem vs. truth
    ... TRUTH does NOT happen under THEORIES! ... Under THEORIES, PROVABILITY or DERIVABILITY or ... Theorems have to be true but truths DO NOT Have to be theorems! ...
    (sci.logic)
  • Re: The Law of the Excluded Middle again (long)
    ... "Inside the scope of quantification, ... to equate (or confuse) truth with provability." ...
    (sci.math)