Re: Godel proved maths inconsistent not incompleteness theorem

On Apr 17, 6:52 am, David C. Ullrich <dullr...@xxxxxxxxxxx> wrote:
On Wed, 16 Apr 2008 08:42:02 -0700 (PDT), Charlie-Boo





<shymath...@xxxxxxxxx> wrote:
On Apr 16, 6:28 am, David C. Ullrich <dullr...@xxxxxxxxxxx> wrote:
On Tue, 15 Apr 2008 19:34:54 -0700 (PDT), Charlie-Boo

<shymath...@xxxxxxxxx> wrote:
On Apr 1, 10:37 am, David C. Ullrich <dullr...@xxxxxxxxxxx> wrote:
On Fri, 28 Mar 2008 11:33:19 -0700 (PDT), Charlie-Boo

<shymath...@xxxxxxxxx> wrote:
On Mar 28, 10:00 am, David C. Ullrich <dullr...@xxxxxxxxxxx> wrote:
On Thu, 27 Mar 2008 18:15:24 -0700 (PDT), Charlie-Boo

<shymath...@xxxxxxxxx> wrote:
On Mar 27, 2:54 pm, MoeBlee <jazzm...@xxxxxxxxxxx> wrote:
On Mar 26, 5:28 pm, Charlie-Boo <shymath...@xxxxxxxxx> wrote:

On Mar 25, 2:25 pm, MoeBlee <jazzm...@xxxxxxxxxxx> wrote:

On Mar 24, 10:46 pm, Charlie-Boo <shymath...@xxxxxxxxx> wrote:

Neither you nor anyone else has ever claimed that any of the dozen or
so proofs that I have posted is not a proof.  Yet you state the
opposite.

In at least one other thread, I told you that your purported "proofs"
in your paper are not proofs. I discussed that in some detail at that
time.

Proof : "An English exposition that shows us that some assertion must
be true."

In mathematical logic, we also have more technical definitions.. So in
a given context, we need to understand which sense of proof is in
play.

I would define a proof more formally along the lines of: "The
execution history of an effective procedure that has one input and one
output, the latter being the single value TRUE."

Oh my gosh. If that's what you think a proof is that explains a lot.

Of course I need to revise the theorem generator I just posted
elsewhere in this thread. Noting that in (old) Python 1 is TRUE
and 0 is FALSE:

from random import choice

from string import lowercase

def s(n):
  res = ''
  for j in range(n):
    res = res + choice(lowercase)
  return res

def proof():
  N = choice(range(5,10))
  for j in range(N):
    print s(choice(range(5,10)))
  return 1

proof()
proof()

I just used it to generate a few more proofs:

[9]
ldpwuwv
njqzd
bstrohsp
ujixcvkh
cuicqou
mppsxbel
efwcd
owwkm
kcvehiofk

[10]
knnlzo
gxwcqeq
vetzf
oxycuofmi
jmfceti
ssvosgqz
tvdxib
cwksgjrt
wgjndr
daahul
ncwqcxqm
ngfospt
khyid
qqotcvuv

Those are the proofs of Theorem 9 and Theorem 10 of UATPS.

[...]

If it always outputs TRUE then in your system everything is a theorem.

Well, duh, that's correct - everything in that system is a theorem.

The inconsistency is curious. Above you say that you'd define a
formal proof as "The execution history of an effective procedure
that has one input and one output, the latter being the single
value TRUE." By _your_ definition I've presented some formal
proofs here, but in another post you seem to doubt that they're
valid.

You're confusing your implications.  Any formal proof is an execution
history, not vice versa.

No, it's not _me_ doing the confusing. It was you who said

I would define a proof more formally along the lines of: "The
execution history of an effective procedure that has one input and one
output, the latter being the single value TRUE."

The point to this little subthread has just been to point out how
silly that is as a definition of "formal proof".

Do you know of correspondances between the following two relations?

YIT(x,y,z) : Turing Machine x with tape input y halts yes at iteration
number z.

PRIT(x,y,z) : Wff x with y substituted for its free variable is proven
by proof number z.

Do you know of ways in which these two relations play the same role?
That there is some sort of equivalence between them?

You like to call things "equivalent" without explanation or defintion
(e.g. my proof of Rosser 1936 is "equivalent to" Turing's), so you
should be able to see the equivalence here, no?


Did you notice that your "reply" has nothing to do with the
post it's nominally a reply to?

I don't know what that means - sounds like some sort of paradox or
something.

My "silly" definition of proof is part of the foundation of Recursion
Theory. I was asking to see if you were aware of any part of that
correspondance between programs and proofs. I asked about those two
relations because they are both used to define any r.e. set (with a
Turing Machine that accepts it or a wff in a Logic that represents
it.)

This is the beginning of the parallel that Recursion Theory exploits.
Recursion Theory is an abstraction from that commonality between
Turing Machines and axiomatic systems of Logic. Kleene's T predicate
is the formalization of that common relation. It is a general base of
computing.

You have not shown any understanding or knowledge of this and this
principle is what shows that a proof is alalogous to the execution
history of a program that leads to a HALT YES command.

A program halts yes if there is an execution history that includes a
HALT YES, just as a theorem is proven if there is a proof that ends
with that theorem. The execution history of the Turing Machine is
analogous to the proof. The existance of either means the value being
tested by the Turing Machine or wff of Logic is in the given set.

Any formal proof you can give must in a Rube Goldberg Mousetrap sort
of way end up producing a value of TRUE for the theorem.  That can be
done with a program and the final result of TRUE is output calculated.

The correspondance between proof and execution history has been known
since the 1930's and is the basis for Recursion Theory:

wff = program
prove wff = program halts yes
refute wff = program halts no
provable = exists a proof
halts yes = exists an execution history leading to Halt YES
halts no = exists an execution history leading to Halt NO

- Hide quoted text -

- Show quoted text -- Hide quoted text -

- Show quoted text -

David C. Ullrich- Hide quoted text -

- Show quoted text -

David C. Ullrich- Hide quoted text -

- Show quoted text -- Hide quoted text -

- Show quoted text -

David C. Ullrich- Hide quoted text -

- Show quoted text -- Hide quoted text -

- Show quoted text -

.

Relevant Pages