Re: Godel proved maths inconsistent not incompleteness theorem

On Apr 23, 10:38 pm, Chris Menzel <cmen...@xxxxxxxxxxxxxxxxxxxx>
wrote:
On Wed, 23 Apr 2008 13:03:09 -0700 (PDT), Charlie-Boo
<shymath...@xxxxxxxxx> said:





On Apr 22, 12:05 pm, Chris Menzel <cmen...@xxxxxxxxxxxxxxxxxxxx>
wrote:
The recursive functions can be recursively listed because they are
represented by the elements of the universal set and one of the
axioms is TRUE(x) which means that the universal set is r.e.  (This
axiom replaces Peano's 5 axioms.)

This is not a proof sketch, as you are omitting fundamental definitions
and axioms.

The axiom is TRUE(x).  See ARXIV paper for many uses of this axiom.

(Compare Daryl's proof sketch of how to reconstruct computability
theory in ZF.)

You like Daryl’s account because it’s more complicated? You’re doing
it again. That’s backwards. You say there’s something wrong when I
prove Rosser’s 1936 result using only Computability and Propositional
Calculus because of all the Propositional Calculus, and you like the
complicated formalization of Daryl based on that awful mess called ZF.

No, I don't leave stuff out. I just do it right and don't need all
those messy definitions. Just a simple general framework works.

Your problem is that you keep saying how CBL should work, rather than
just saying that it should work. First question is whether it
produces theorems, are they new, are they better. You just talk about
not liking how it’s put together. Sorry, but it isn’t like the messy
systems you’re used to. That might be because it’s for real - it’s
designed well and it captures the essence of the theories it is
formalizing. That makes it nice and simple.

Since you say "the universal set is r.e." I guess by
"universal set" you just mean the set N of natural numbers -- why the
perverse terminology? Be that as it may:

"Universal set" is perverse?

Well, the term has a pretty widely understood meaning in logic already,

Yeah, Einstein, we all know that.

but, of course, being as clueless as you are of everything outside of
your own quirky and ill-defined system, it's no surprise you don't know
that.

So why can’t I use it like other authors do?

I prove theorems of Godel, Rosser, Turing, Smullyan and you say I
don’t know anything outside of my own system? Are you nuts?

I use that term because it denotes the set of all values variables in
the system can be.

Really?  CBL appears to have variables ranging over Turing machines,
sets, programs, all sorts of stuff.

All sets are subsets of the natural numbers. I guess looks can be
deceiving.

* In virtue of what axioms of CBL does the existence of N exist? What
is CBL's set theory?

Recursion Theory doesn't use a set theory, idiot.

Sure it does.  (You should avoid the name-calling when you don't really
now what you're talking about.)

No, one should always avoid name-calling, except perhaps in jest as
above. No offense.

One is after all quantifying over sets
and functions.

Who is? Where

In a typical exposition, enough set theory to do the job
is simply tacitly assumed.

Oh, so why can’t CBL do likewise?

But this is a red herring.

Especially when you realize you’re wrong. Set Theories were developed
to fix the Russell Paradox. That doesn't occur when the universal set
is all numbers.

The question
really had to do with CBL per se, as the framework for metamathemtics
that you trumpet it to be, not simply its application to recursion
theory.  One of the many completely bungled elements of CBL is its set
"theory".  For example, the quasi-BNF you provide for your "program
calculus" contains the following clause:

 for set-definition : For each element of a set defined by
 set-definition, the variables in set-definition assume that value and
 the rest of the line is executed.

Yet nowhere is "set-definition" unpacked.  Great stuff.  How about {x :
x is not in x} as a set definition?  No?  Why not?  CBL doesn't say.
(You no doubt will mumble something to the effect that you don't have to
specify any particular set theory in CBL, that it "transcends" such
mundane details, etc etc.)

Yes, you are right. In the ARXIV paper I tried to show how to
synthesize programs written in a generic programming language and
translate that into whatever programming language you want. You are
referring to variables, the values of which depend on the programming
language you want the synthesized programs to be written in. I know
that confuses a lot of people who think that this language is what the
programs will be written in. It represents the flow and the values of
these unknowns you refer to depend on the actual language used.

Since then I have realized that it is a lot easier to just use some
particular programming language and note that it works with any
programming language. Now I use the PHP programming language as an
example and there is no need to have the variables that you mention
are not very clear to many people.

* In virtue of what does "TRUE(x)" MEAN that the universal set is r.e.?
  This appears to be nothing but magickal thinking. Why can't "TRUE(x)"
  mean "x is prime"?

You never heard of variables and definitions?

Uh, sure.  So where is the definition of "TRUE(x)" that constrains it to
mean that the universal set is r.e.?

What I’m actually saying is that the set expressed by the
propositional constant TRUE, as a one-place relation instead of a zero-
place relation, is (in common terminology) r.e., although that is a
special case of characterizing a set in CBL and I don’t give special
names to special cases. But P/YES, a special case of P/Q, expresses
the assertion that P is r.e.

M # P/Q means P(a) is Q(M,a) for all values of (a).
P/Q means there is an M such that M # P/Q
YES(a,b) means Turing Machine a halts yes on input b.

So that P/YES means P is r.e. There is an M such that P(a) is
YES(M,a). M is a Turing Machine that accepts set P.

Other values of Q allow us to assert that P is expressible,
representable, a well-defined set, and other characterizations of a
set P.

* What is the definition of "r.e." in CBL?

"r.e." is not a term in CBL.  You mean, how do I express the assertion
that a given set is r.e.?  P is r.e. is expressed by P(x) in the
Theory of Computation, and in more general contexts (e.g.
Incompleteness in Logic) as P/YES.

And *presto*!  Prefixing the name of a set to "(x)" expresses that it is
r.e.

Yes, you got it. P(x) is an abbreviation for P/YES. I originally
needed only P(x) for the Theory of Computation. When I added
Incompleteness in Logic, I had to generalize that to include
expressible and representable. So I defined M#P/Q and P/Q as above,
and P(x) remains as an abbreviation for P/YES. We can use P(x)
because the Theory of Computation needs only P/YES for r.e., while
Incompleteness in Logic uses P/TW for P is expressible, P/PR for P is
representable, and occasionally e.g. P/DIS for P is
contrarepresentable.

Not a recursive function to be found that lists the elements of P,
or of which P is the domain.  Just write "P(x)".  Truly magickal.

Actually P is YES(M,a) for some number (Turing Machine) M, although I
don’t think there’s anything wrong with just saying that P(x) means
the set expressed by wff P is r.e.

* How do you know "TRUE(x)" replaces the Peano axioms?  What is the
 proof of this claim?

Quiz time: Think of a program that lists the natural numbers.  Now see
if you can extract Peano's Axioms from that.

Uh, ok:

#! /usr/bin/perl
my $n=0;
while ('CBL_ROCKS!') {
  print "$n\n";
  $n++}

Why, yes, it's all so clear to me now!  ??  Ok, I admit it, I'm stumped;
"extract" an instance of the induction schema for me.  Or even the axiom
that 0 is no number's successor.  Extract away.  Can't wait for that
extraction.

You sound like you're going to the dentist. ("It's just a drill.")

This is not formal, of course, as the fact that TRUE(x) replaces
Peano’s Axioms is not a theorem of CBL, but rather a study in
comparing CBL to other axiomatic systems. Let’s express this
enumeration as:

1. N=0
2. Print N
3. N=N+1
4. Goto 2

TRUE(x) means this program exists which enumerates the set of
numbers. Then Peano’s Axioms are extracted as follows:

1. 0 is a number: After line 1, N=0 so from there we get to line 2
with N=0 and we print 0, so 0 is a number.

2. Every number has a successor number: For every N printed in line 2,
we reset N to the successor of N in line 3, then go to line 4 and then
line 2 where the successor of N is printed, so the successor is also a
number.

3. 0 is not the successor to any number: If the successor of a number
were 0, then after that number is printed on line 2, N would be reset
to 0 by line 3, and we would go to line 4 then line 2 where we output
0 again. Thus only a finite number of values of N would be printed.
The fact that N is infinite makes this impossible.

4. Different numbers have different successors: Let A and B be
different numbers that have the same successor C, where A is printed
before B. Then after A is printed we will reach line 2 with N equal
to C, and later after B is printed we will again reach line 2 with N
equal to C. Thus we will repeat the sequence of steps between those
two points and the set of number printed will be finite. But the
number of numbers is infinite.

5. A set S containing only 0 and the successor of every element of S
contains all numbers: The above program prints 0 and the successor of
all numbers, so it prints all elements of S. The set of all numbers
is defined to be what is printed by this program, so S contains all
numbers.

Note that axioms (3) and (4) are both implied (in the above arguments)
by the fact that this program cannot transition from two different
states to the same state, where state is (current value of N,current
line executing), as then the number of numbers would be finite. So
(3) and (4) are both implied by the same general principle of not
repeating a state since the set of numbers printed is infinite..

If (3) were false then we would transition from (0,1) and (M,4) to
(0,2) where M is the number that the negation of (3) says exists. If
(4) were false, then we would transition from (A,2) and (B,2) to (C,
2).

(This is just a small part of Axioms from Programs, one of the best
ideas I've ever had regarding Mathematical Logic. You define the
universal set, Addition and Multiplication with simple programs, and
the axioms are extracted from them - hopefully automatically, if I
ever get to it.)

(As mentioned before, in first-order PA,
there are *infinitely many* axioms, so how can TRUE(x) possibly
"replace" them?  Is CBL supposed to be second-order?  Do you even
understand the question?)

See above.

s-m-n would be formalized by proving f(I,J) => N # f(I,M) which
means that if f is a two-place recursive function, then for any M
there is an N that computes f(I,M).

More of what you usually refer to as BS. There is no proof here.

Right, you clipped the rest of the proof.

Well, cuz it wasn't a proof of the s-m-n theorem.  Folks were free to
consult your original post to see for themselves.

Not if they think your quote is accurate.

There is a recursive function g(I,J) such that for every recursive
function f(I,J) computed by program M and for every number N, g(M,N)
computes f(N,I).

For any i < or = j, function Sij(I,J) is defined to be the number of
the wff formed by substituting J for the i-th free variable out of j
free variables in wff number I.

For each i,j there are two axioms. One states a property of the value
of Sij by definition and one states that Sij is recursive. We will
use s12 with axioms:

M # f(I,J) => s12(M,N) # f(N,I) : Property of the value of s12 (by
definition)
If program M computes two-place function f, then program s12(M,N)
computes one-place function f(N,I).

s12(I,J) : s12 is recursive (an axiom of the recursive functions)

[NB1. Most treatments drop the j and say that there is a function s
for each i and not for each i,j.]
[NB2. The family of functions sij could be expressed as a single
function sub where Sij(I,J) is an abbreviation for sub(i,j,I,J).]

Thm. There is a g(I,J) such that for all N if M#f(I,J) then g(M,N)
# f(N,I).
1. M # f(I,J) Premise
2. M # f(I,J) => s12(M,N) # f(M,I) Axiom: Definition of s12.
3. s12(M,N) # f(M,I) MP 1,2
4. s12(I,J) Axiom: s12 is
recursive.
qed

I proved the theorem.  It is very easy to prove in CBL.  You can make
up all sorts of red herrings, but if it produces theorems then you
have no case.

But I've always agreed it produces theorems.  Just not the theorems you
claim them to be.

What theorems does CBL produce IYHO?

There is only the claim that something can be proved. And, as usual,
there are no definitions or axioms for the most crucial notions,
notably, "recursive function".

"Axioms for the crucial notions"??  

You don't understand the concept of an axiom?

I don’t know what it means for an axiom to be “for a notion”. If you
mean an axiom that refers to that notion, then we only need what is
needed to prove the theorems. This is a minor case of trying to
dictate how CBL should work, as opposed to simply saying that it
should work, meaning it should produce theorems.

Remember that CBL expresses concepts more general than r.e. or
expressible or representable.

I know you believe that to be true, but it has to be able *at least* to
express the concepts that it is claiming to prove theorems about.

Again, contrast with Daryl's account.  A recursive function is either
one of the initial functions (zero, successor, the projection
functions) or a function resulting from the application of the
operations of composition, primitive recursion, or minimization to
given recursive functions. What's your account?

You set up the axioms and if they hold for a given system then the
theorems do.  

OK, so do it.  Set up the axioms of recursion theory in CBL.  Why is it
you don't seem able to do that?

Why do you think I can’t? I’ve posted the axioms at least 3 or 4
times, including recently.

Note the definition above of family of functions sij.

Function wr(I) returns a program that writes the value of I.
Function yes(I) returns the set of inputs which program I accepts.

Ax1. wr(I) # I : Program wr(I) calculates I.
Ax2. wr(I) : Function wr is recursive.
Ax3. I # yes(I) : Program I calculates yes(I).
Ax4. yes(I) : Function I is computable.
Ax5. M # f(I) => s11(M,N) # f(N): If M computes f(I) then s11(M,N)
calculates f(N).
Ax6. s11(I,J) : s11 is recursive.
Ax7. f(I) , M # f(I) : Function f is recursive iff there is a program
M that calculates f.

I also use operators ~ and = which are:

M ~ N : Programs M and N calculate the same function.
M = N : Functions M and N are the same.

Ax8. M ~ N , M # O + N # O
M and N calculate the same function iff there is a function O that M
calculates and N calculates.

Nice Useful Theorem: M ~ N , yes(M) = yes(N)

Ax9. M = N , O # M + O # N
M and N are equal iff there is an O that calculates M and calculates
N.

Ax10. P(M) , M=N => P(N) Substitution for equals.

This suffices to prove:

1. There is a self-outputting program.
2. The recursion theorem.
3. The fixed point theorem.
4. Solve various sets of equations involving recursive functions.
5. Various weak/strong single/double recursion theorems.

1: M # M
2: f(I) => M # f(M)
2a: f(I,J) => M # f(M,I)
3: f(I) => M ~ f(M)
4: Ex. f(I) + g(I) => M # f(N) + N # g(M)
If f and g are recursive, there are programs M and N such that M
calculates f(N) and N calculates g(M).

Creating a Quine Atom is a special case of solving a set of
simultaneous recursion equations, where instead of I # yes(I) which
says we can run a Turing Machine, we have e.g. I # se(I) where se(I) =
the set defined by expression I. This is how I created the Quine Atom
and variations posted on FOM http://cs.nyu.edu/pipermail/fom/2002-September/005844.html
.

5: Many of the more advance theorems are simply uses of other Sij e.g.
s12, s22, s13, s23, s33 etc.

Rule SUB applies to any substitution, as there is no reference to the
program.
SUB: P(I) => P(“…”) and f(I) => f(M)

When the program is included, we need to show the function that maps
the given programs into the program that is guaranteed to exist. For
example:

M#f(I) + N#g(I) => do(M,N) # f(g(I))
do(I,J) : Function do is recursive.

M # f(I) + N # g(I,J) => sec(M,N) # g(I,f(J))
sec(I,J) : Function sec is recursive.

The task here is to develop a minimal set of functions needed to
create any term.

C-B
.

Relevant Pages

  • Re: Godel proved maths inconsistent not incompleteness theorem
    ... to me as to the purpose of your question about set theory that I ... matter, the CBL axioms). ... Turing only uses one base, Turing Machines, while Logic uses at least ... theorem, recursion theorem, double recursion theorem and others. ...
    (sci.logic)
  • Re: Godel proved maths inconsistent not incompleteness theorem
    ... represented by the elements of the universal set and one of the axioms ... before I included Recursion Theory.) ... substituted for free variable number i out of j free variables. ... theorems that I am personally interested in - those of Godel, Rosser, ...
    (sci.logic)
  • Re: Godel proved maths inconsistent not incompleteness theorem
    ... Perhaps if you answered the following for CBL: ...   it is recursive. ... represented by the elements of the universal set and one of the axioms ... Recursion Theory doesn't use a set theory, ...
    (sci.logic)
  • Re: A recursion axiom for N?
    ... needs a stronger version of induction to do so." ... it, "It's valid using some basic axioms of set theory, or some basic ... recursion is defined in this system, ...
    (sci.math)
  • Re: Categorical model of N?
    ... etc., as new axioms, will be recursively ENUMERATING them, ... Looking at the sequence T_n defined above, we see that given that we ... and unlike in the case of successor ordinals ... (this is proved using the recursion theorem). ...
    (sci.logic)
Loading