Re: Godel proved maths inconsistent not incompleteness theorem

On Mar 25, 3:09 am, Chris Menzel <cmen...@xxxxxxxxxxxxxxxxxxxx> wrote:
On Mon, 24 Mar 2008 22:42:59 -0700 (PDT), Charlie-Boo
<shymath...@xxxxxxxxx> said:





On Mar 24, 1:38 pm, Chris Menzel <cmen...@xxxxxxxxxxxxxxxxxxxx> wrote:
On Mon, 24 Mar 2008 09:31:45 -0700 (PDT), Charlie-Boo
<shymath...@xxxxxxxxx> said:

On Mar 17, 11:38 am, Aatu Koskensilta <aatu.koskensi...@xxxxxxxxx>
wrote:
On 2008-03-17, in sci.logic, Charlie-Boo wrote:

(As far "standard terminology" goes, the words are something
poorly chosen and I like to avid that. E.g. a decidable wff has
nothing (directly) to do with a decidable system - numerous
authors have apologized for the confusion. In my personal
research, I use more consistent terminology. (A "decidable"
system is one in which all sentences are decidable.) Again, it
just works better.

What do you call, in your personal research, a decidable system in
the usual sense?

PR(I)*

What is its definition? What is its semantics? Why can it not express
"I makes a fine cup of hot chocolate"?

You gotta read the ARXIV paper, as well as my dozen detailed
explanations.  (I now realize that many people will never understand
it until I post it to my home page with a zillion pages of detailed
examples and explanations, including clarifications based on readers'
feedback.)

No, people will never understand it until it has genuine, rigorous
mathematical content.

What a slap in the face of Alan Turing!

Now, I can say that P is a variable that ranges over relations,
right?  That is a very common thing to do in Mathematics - a variable
with a range.  I don't have to define what a relation is or what a
variable is or give a formal system that explains it, do I?  

Well, it depends on what you are doing with it.  Typically, no, one
doesn't have to define what a relation is, unless one uses the term in a
way that cannot take them to be sets of ordered pairs.

That wouldn't be an omission, it's a misuse of the term.

 And, typically,
one doesn't have to say what a variable is.  It's not clear at all that
you are using them in a standard way in CBL.

Believe me, I am. Read the paper.

Your notation is quirky
and nonstandard, so one cannot be at all sure you have the usual notions
of relation and variable in mind.  

Example? I use Predicate Calculus syntax and add semantics to the use
of free variables I, J, K and X, Y, Z. Everything is standard (syntax
and semantics) or new semantics using existing syntax that has no
current semantics (free variables I,J,K,X,Y,Z) when there is no
standard syntax fo the semantics.

What is the standard formal syntax (wff of some sort) for the
assertion that the set of theorems (of a certain defined system) is
r.e.? That the Halting Problem is unsolvable? (But I actually need a
more general form that even that.)

After all, we all know what a relation is, what a variable is, and a
variable can range over relations.  When someone does this in a
published article, you don't write the editor of the journal and
complain that the author didn't include a whole bunch of background
material, right?  So let's try to be reasonable and consistent.

Say that the degree of P is 1, so it is just a set.  Then the
following expressions have the following meanings:

P(x)   P is recursively enumerable.
P(I)*  P is recursive.

And thus we have magickal thinking.  I will grant you that, other things
being equal, you don't owe us a definition of "relation" and "variable".
But "recursive" is a whole other kettle of fish -- at least in the sort
of foundational system CLB purports to be.  No, you need to define that
notion in terms of initial functions are the usual operations, or Turing
Machines, or a Turing-complete programming language, or what have you.

I define P(I)* (et. al.) in terms of Turing Machines, and references
to the concept of recursive use that. For example, "The Halting
Problem is solvable." means "The halting set is recursive." The
halting set is HALT and it being recursive is thus HALT(I,J)* so that
represents "The Halting Problem is solvable." It is all defined in
terms of Turing Machines. And I refer to Turing 1937 for the
definition of a Turing Machine.

When we are proving results concerning a Logic, we let PR = the set of
theorems

Theorems of *what system*?

Any system where PR being the set of theorems satisfies the axioms.

and TW = the set of true sentences.  

Sentences in *what language*?  True in *what model*?

Any system in which TW being the true sentences satisfies the axioms
expressed in CBL.

This may be a source of misunderstanding: CBL does not have a
particular set of axioms. I give axioms that satisfy PA or common
systems. But CBL basically provides a syntax and semantics to express
the axioms and rules needed to prove properties of formal systems. I
then use it to prove properties of PA or any system that satisfies the
axioms.

CBL is really more general than a particular system such as PA, even
when you allow for additional axioms as Godel does in his 2nd
Incompleteness Theorem. I think this is why you are looking for
particulars about specific systems, when CBL applies to any system -
actually to any sets PR and TW etc. - such that the axioms are
satisfied. And the axioms are also more general in that we state them
for the particular system or class of systems we want to study.

That is probably a reflection of your intimate knowledge and
understanding of particular systems. But Smullyan takes a more
general approach, and CBL is more general than that still (as well as
being completely formal.)

It seems that many people will never relate to that until I have my
home page working and can interactively make my description more
palatable to the general public. I have been using my little system
for more years than I care to admit (as well as knowing what I mean
when I write about it.) Likewise, the programmer is the worst person
to proofread software documentation - he can't tell what's missing
because he already knows what it's supposed to be explaining.

And we don't give "the" formal system because it applies to all formal
systems that meet the axioms given in CBL that refer to PR and TW.  We
simply give axioms.

Sorry, that's just not going to wash.  The sort of thing you are talking
about can indeed be done in a general way, but you need to put far
greater constraints constraints on what counts as a formal system, what
it for a sentence of such a system to be a theorem, what it is for a
sentence is to be true in an interpretation of the language of such as
system, and so on.  Otherwise nothing tethers "PR" and "TW" to the
theorems or truths of any given system besides your say so.

Right, nor should it. Theorems and truths of PA are two sets that
when used (substituted) for PR and TW the axioms that I often give
hold. If we can interchange PR and TW and use a different system than
PA, and the axioms hold for those PR and TW, then the CBL theorems
will apply to those sets PR and TW.

CBL proves properties of sets, really. And certain systems of Logic
involve sets that meet the axioms concerning PR and TW et. al. so that
the CBL theorems then concern those sets e.g. the theorems and truths.

(I can see at this point that it is used a little differently than the
typical axiomatic system: Typically we have a single Logic and axioms
about that Logic.  Here we are saying that we have any Logic that
satisfies the axioms.)

But you need to say what a Logic is for that claim to have any purchase.

No. That is an instantiation of CBL axioms. I can point out that
when PR is the theorems of PA and TW is the truths of PA (whatever
"interpretation" - not really needed here - we can think of wffs as
referring to particular relations rather than to variables and
associate the variables with relations elsewhere) then the CBL
theorems give properties of PA's theorems and truths. I don't
generally do that, but sometimes point out that PA satisifes some
particular set of CBL axioms, and note that in that case we have
certain well-known theorems about PA.

Now, we can give axioms for PA or we can just give axioms that hold
for a typical Logic.  (This is VERY common.)  We can say things like:

PR => TW   The Logic is sound.

What ensures that PR doesn't refer to the set of true sentences of a
system (in what interpretation?) and TW the set of theorems?  Answer:
NOTHING.

True. But that choice for PR and TW must satisfy the CBL axioms that
refer to PR and TW.

Not until you build your system from the ground up a produce
rigorous definitions of truth (in an interpretation) and theoremhood in
a system.

No. Like Smullyan, I refer to sets in general. Smullyan is more
general than PA and I am more general than that (as well as being
formal.)

PR(x)            The set of theorems is recursively enumerable.
PR(I)*           The set of theorems is recursive.

I have no idea what "x" and "I" are doing here, but what's to prevent:

  TW(I)*   The set of truths is recursive.

Answer: NOTHING.  Because you haven't defined "true" and "recursive".

If the set of truths of system XYZ is recursive, then the CBL theorems
will hold for system XYZ. I define everything in terms of Turing
Machines. P(I)* is defined in terms of TM's and the definition
amounts to P being recursive.

-TW(x)          The set of true sentences is not recursively enumerable.

What if the system in question is Presburger Arithmetic -- where the set
of true sentences *is* r.e.?

TW(x)

Again, we might be talking about PA and give correct axioms for PA, or
we can simply say that any Logic for which our axioms hold has the
properties we are about to prove from these axioms.

Again: Nothing tethers the strings above to your intended meanings.
There is no mathematics there.  It is just magickal thinking.

It's more general than that. PR and TW are any sets such that the
given CBL axioms hold. Think of how Godel's 2nd Theorem is
generalized by Boolos et. al. CBL is similar to that but a bit more
general.

Now define variable YES by YES(x,y) iff Turing Machine x halts yes on
input y.  Again, it is just a variable that is given a fixed value for
this discussion.  (And for heavens sake we don't need to copy Turing's
definition of a Turing Machine here.)

Oh, I beg to differ.  That is *exactly* what you need to do.

Can't I just refer to Turing 1937?

And in
particular you need to use that definition to provide rigorous
definitions of "recursive" and "r.e.".

You are talking about particular instantiations of CBL axioms. I
don't say recursive and r.e. because it's more general than that. But
I now realize that I am going to have to show specific uses of CBL in
more detail for people to relate to what they are used to, to the more
general and formal CBL formalization.

In other words, I give CBL axioms and certain systems, e.g. PA, have
sets of theorems and truths that when PR and TW are those sets the
given CBL axioms are satisfied. But I concentrate on the beginning
(showing the CBL axioms) and ending points (the particular theorem
concerning PA.) I now realize that I have to explicitly show that PR
and TW being the theorems and truths of PA makes the axioms hold.

Not to mention the fact that you
need to define what a Turing machine so you can enumerate them and
thereby make sense of the notion "Turing Machine x".

In general, if P is a 1-place relation and Q is a 2-place relation,
then P/Q means there is an M such that P(a) <=> Q(M,a) [for all a].

So, for example, let P be the set of primes and let Q be the set {<0,p>
| p in P}.  So we have P/Q.  Ok.

Yes, P/Q does hold in that case. 0 # P/Q. Q(0,x) is indeed P, the
set of prime numbers.

We can say that "M characterizes P in (base) Q."

So the number 0 characterizes the set of primes in base, uh,
set-of-pairs-<0,p>-for-any-prime-p?  Well, ok.

Yes!! : )

Then the expression P/YES means that P is recursively enumerable.  

Yeah, I can see that that is what that would mean if you worked out the
details.

Don't know if you're being facetious or not, but that is true.

And if Q is other relations besides YES, P/Q means that P is
representable or expressible, as you can perhaps see.

Perhaps I could, if you actually defined what it means to be
representable -- in what language?  Relative to what interpretation?

Now now - interpretation has no role in this one. :)

Take you pick. No, that's not irresponsible - it's more general.

Say you have a given Logic and define Q as Q(x,y) iff wff number x
with y substituted for its one free variable is a theorem. The P/Q
means P is representable.

The natural numbers?  Where do you say?

P(x) is actually an abbreviation for P/YES.

(I'd be glad to discuss in detail the two approaches. But formally
expressing a property instead of giving a "kludge" definition of that
one case is not only easier to work with, the special particular
definitions actually interfere with proofs that use the general,
formal approach.)

Except CBL doesn't "formally express" any properties at all.

But when you use particular sets for P and Q it tells you properties
of that P and Q. And if P and Q are defined by referring to a
paricular Logic(s) then guess what you get? Metamathematics!

CBL is a formalization of Metamathematical Logic.  

Oh, but it isn't.  It really isn't.  It's nowhere close to a
formalization of metamathematics.

But if when PR is the theorems and TW is the truths of a system the
given CBL axioms hold, then the resulting CBL theorems tell us about
those theorems and truths. E.g. -PR,TW means sets PR and TW are not
the same, and when PR is the theorems of PA and TW is the truths
(interpretations not needed - assume wffs refer to particular
relations) and the CBL axioms hold, then we have the theorem that the
theorems and the truths in PA are not the same.

 It is *at best* a wan gesture in the
direction of such a formalization, though I think even that is an
generous overstatement.  If you want a formalization of metamathematics,
you need to formalize, say, Mendelson; or Enderton; or Kleene;

That is one instantiation of CBL. Boolos rarely refers to PA, but we
know his theorems apply to PA.

more
generally, books contain the actual mathematics of metamathematics.
Though it would be frankly crazy to do so, unless you have, say, a
kickass automated theorem prover and you want to see how well it does
with metatheory.

PA formalizes part of Mathematics and CBL formalizes Metamathematics.

Sorry, it does no such thing.

Some day you'll see. When my home page explains it all in
excruciating detail.

You have shown me a lot more where I need to expand my exposition of
CBL. Your intimate knowledge and understanding of PA and its
variations has wed you to them, and I need to show more how to
generalize that understanding - or at least to bring it down to your
specific level with a detailed explanation of how to create that
particular instantiation of CBL.

You are obviously very sincere and have spent a great deal of valuable
time and effort examining CBL, to which I can only thank you, a small
part of the compensation you deserve for doing me such a service.

C-B
.

Relevant Pages

  • Re: Godel proved maths inconsistent not incompleteness theorem
    ... learn CBL. ... But the theorems of "Set Theory" are not well- ... theorems or a set of axioms that defines those theorems. ... How does this relate to ZFC? ...
    (sci.logic)
  • Re: Godel proved maths inconsistent not incompleteness theorem
    ... learn CBL. ... But the theorems of "Set Theory" are not well- ... theorems or a set of axioms that defines those theorems. ... How does this relate to ZFC? ...
    (sci.logic)
  • Re: Godel proved maths inconsistent not incompleteness theorem
    ...  How does this tethering happen in real mathematics? ... any evidence that CBL is tethered in the same way to computation at ... with axioms written in CBL, as I have done and described for PA. ... From that point onward, PR refers to the set of theorems, ...
    (sci.logic)
  • Re: Godel proved maths inconsistent not incompleteness theorem
    ... I find it hard to understand CBL because you usually give all the things ... I think it would help to present CBL with regards to "Set Theory" only. ... We can state most of the standard axioms of Set Theory pretty easily. ... You mean how do I generate theorems of set theory? ...
    (sci.logic)
  • Re: primitive recursive: obsolete?
    ... we have to add more axioms. ... all true sentences of arithmetic in the language of PA. ... logic we define the set of sentences true in the standard model of PA ... theorems" or not has no bearing on the fact that what I said is ...
    (sci.logic)