Re: How do We Know that ZF is the Axiomatization that Proves everything Provable?

On Feb 12, 3:10 pm, Chris Menzel <cmen...@xxxxxxxxxxxxxxxxxxxx> wrote:
On Sat, 9 Feb 2008 09:52:29 -0800 (PST), Charlie-Boo
<shymath...@xxxxxxxxx> said:

On Feb 8, 4:57 pm, William Hale <h...@xxxxxxxxxx> wrote:
In article
<5d73eb21-7613-49fd-a53a-17383ac6e...@xxxxxxxxxxxxxxxxxxxxxxxxxxxx>, Charlie-Boo
<shymath...@xxxxxxxxx> wrote:

[cut]

Possibility A. If only ZFC is used: Then the axioms in ZFC, which
refer to sets, are translated into statements about some other
mathematical objects (natural number, line, real number, etc.)

The axioms in ZFC are *not* translated into statements about some
other mathematical objects (natural number, line, real number, etc.).

I don't know where you got that idea.

Feel free to explain your interpretation of doing math in ZFC.

Using CBL.  It's extremely powerful.  For example, Godel's 1st
Incompleteness Theorem is PR'=TW (proof does not equal provability)
and Rosser 1936 is PR'=~DIS (provable does not coincide with non-
refutable.)  These we prove very quickly: TW is negation complete
because of the "~" (not) symbol, and PR is not because the set of
theorems is representable.  PR is r.e. but ~DIS is not.  So we have
both Godel and Rosser in a couple of steps!!

CBL is terribly ill-defined.  (I take it you meanhttp://arxiv.org/html/cs.lo/0003071.)

No, that's 8 years old. I mean the various proofs that I have posted
in the past couple of years. I don't believe anyone has even claimed
that they are not valid proofs. The only response is that it's easy
or uninteresting, or the occasional praise from someone who actually
read it. (I myself would jump on any reference that claims to
formalize or shrink these results.)

The language of predicate logic
you claim to be using is nowhere defined

Standard.

and seems to involve undefined,
nonstandard concepts ("output variable"?).

It's all defined - P(I) means P is recursive, P(x) is r.e., That was
in 2000. Now there are 2 others and I say P(I)* = recursive P(I) =
partially solvable = r.e. P(x) = can output set P which is equivalent
to P(I) when characterizing sets using theorems or programs (r.e.
sets) formally because equality and the universal set are r.e. First
is the fact that the difference between recursive and r.e. is that the
process halts in the first case, so there are 4 cases: Input or Output
a value, and the process halts or not. I expanded it to 4, where 2
are equivalent in this case, to introduce P(I,x)* "finitely
enumerable" which means that we can list the x in P(I,x) and then
halt. This is not the same as that set being finite, because of the
variable input I. For example, for any I the set of iteration numbers
on which program I halts is finite, having 0 or 1 element. We can
list them, but we cannot then halt, as that would solve (reduces to)
the halting problem. This is needed to formalize Rosser 1936 at a
detailed level and also can be used to simplify the representation of
"bounded quantifiers" - an awful kludge in how it is represented in
print.

 The syntax for the
programming language in Section II is incomplete.

That's not the programming language itself. That's the representation
of the program created. When you axiomatize the programming language,
you give segments of code that are combined with this syntax. The
program synthesized is represented by that syntax, but to create the
actual program you have to substitute the pieces of code that
axiomatizes the programming language.

I have since greatly improved this. The problem is that I formalize
the set being listed or decided, but was only implicit in the
existance and manipulation of the programs to create the synthesized
program. Now I include the program explicitly in a simple general
scheme that uses only 2 types of expressions.

The problem is program synthesis: input a spec, output programs. P =
spec (e.g. compute a function f(I), list a set P(x), decide a set P(I)
now P(I)*) M = program (term - expression equal to a number). M # P
means program M meets spec P. Now consider:

A. The system is legitimate program synthesis.
B. We prove that each program output meets the spec. |- M # P

A == B. So the problem of program synthesis is the problem of proving
M # P. Any effort to prove anything else is a waste of time or not
correct.

So how do we show |- M # P? Axioms and rules, of course. What
rules? My ARXIV paper. What axioms? More detailed than my ARXIV
paper. Assume the programming language is PHP.

"function LT($a,$b){ return $a<$b ; }" # LT(I,J)*

The above PHP program "solves" LT(I,J) i.e. it decides the less than
relation.

Now suppose we want to program to solve the not less than relation?

1. "function LT($a,$b){ return $a<$b ; }" # LT(I,J)* Axiom
2. not("function LT($a,$b){ return $a<$b ; }") # ~LT(I,J)* NOT Rule







 Standard terminology
is given nonstandard meanings (an axiom is a program that "solves a
particular wff"?).  There is no formal semantics and (hence) no soundess
proofs for your "axioms" and rules of inference.  Use/mention confusions
abound.  Most seriously, crucial terms and predicates are introduced to
"prove" this or that, but are invested with meaning only via your
intentions rather than through formal definitions, axioms or a formal
model theory.  For example, "for set-definition ..." is supposed to mean
"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"
but you nowhere define what a set-definition is or specify what set
theory you are assuming, nor do you define what it is for a "line" to be
"executed", i.e., you provide no formal model of computation or program
execution.  Lack of a model of computation is particularly serious.  For
example, in Section VI, "NIT(a,b,c)" is introduced with the intended
meaning "Turing Machine a halts no on input b at iteration number c",
yet one seeks in vain for the definition of a Turing Machine or a
definition or axiomatization of NIT (or of halting, for that matter)
that would mathematically ground the intended meaning.  You simply start
using the predicate with your intended meaning, and when you "prove"
something involving "NIT" (e.g., your Theorem III) you inject your
intended meaning into the result.  But the actual syntax of the proof is
untethered to any real mathematics.  So it's no surprise that you can
deliver "results" like Gödel's theorem "in a couple of steps".  All the
real mathematics is left out.  The connection between the syntax CBL
generates and Gödel's actual theorem is, quite literally, only in your
head.

.

Relevant Pages
Loading