Re: Contradiction or paradox

On May 20, 7:05 am, Charlie-Boo <shymath...@xxxxxxxxx> wrote:
On May 18, 12:42 pm, MoeBlee <jazzm...@xxxxxxxxxxx> wrote:

OnMay8, 5:29 am, David C. Ullrich <ullr...@xxxxxxxxxxxxxxxx> wrote:
On 7May200707:00:13 -0700, Charlie-Boo <shymath...@xxxxxxxxx>
wrote:
The assumption is that ~(x e x) is a wff
Wow, this again. The term "wff" has a perfectly standard
definition, and ~(x e x) _is_ a wff by that definition.
C-B appears to be a bit confused on this point, and on numerous
others.

The above line was not written by me, but rather it may have been part
of a quote that posted.

1. "Wff" has no standard definition - it is whatever syntax you want
to use in your system. (In programming terms: It's part of the spec -
the User Interface in particular.)

In various of these discussions, we've been talking about well formed
formulas of Z set theories and the like, in which case there are still
variations but not so great that we can't settle that some version of
~xex is well formed.

2. Even in the same system different authors use different syntaxes.

Yes, and in any ordinary exposition of the common set theories, there
is some syntax that has ~xex or some variant as well formed.

3. The question about ones definition of "wff" (which I asked and is
now being asked of me) is correct. But the people who give the
erroneous proof of the inconsistency of Naïve Set Theory have to give
it to explain their proof. There we can begin to see that their
argument is not well-formed.

You're confused about all of this at the most basic level. The
unrestricted comprehension schema is inconsistent by considerations of
just basic predicate logic.

In his much cited Arxiv paper (http://arxiv.org/html/cs/0003071),
he provides what is apparently supposed to be a BNF for
his "Program Calculus"
But nowhere in the "BNF are we told what a "set-definition", or even
an "expression", is; the BNF is lacking some crucial terminals here.

Again, not written by me, but rather quoted by me.

Thanks for making the effort. See the next paragraph: "The actual
arguments to commands will be defined for each axiom (given program)
on an ad hoc, informal basis, and serve to represent actual code in
real life programming languages that performs loops, variable
assignment, conditional execution and output." By this I mean that
the CBL program represents the program written in the executed
language (e.g. C++) and the arguments are just symbols (variables)
that represent the program code in that language.

Such a mess of ad hoc informal bases serving to represent some
computer code or another does not make a rigorous formulation of the
syntax of a system. You've not provided the reader with a way to
mechanically verify that the lines in your "proofs" are results of
purely syntactical operations on previous lines.

For example, one of the programs generated to tell if one number is a
factor of another is:

"Program 1: Search for an integer A such that A*I=J.
for A=1:1:J set B=A*I if B=J write (true)
write (false)"

What does this mean? Well, follow through the proof. Line 1 is:

1. ~LT(I,X)H Axiom 2 We can count to any given number.
for x=1:1:I write (x)

This axiom is saying that we have a program (written in C++) that
takes in any number I as input, lists all values of x such that
~LT(I,x) and then halts. So it lists the numbers from 1 to I for any
input I. "We can count to any number."

The CBL program for x=1:1:I write (x) represents the C++ program with
the FOR command to indicate repeated execution with an argument of
x=1:1:I. This argument (as explained above) is an arbitrary sequence
of characters ("x=1:1:I") to represents the C++ code that assigns
variable x the values 1, 2, . . . , I and for each executes the rest
of the line. The rest of the line is CBL command write with argument
(x). This means we have the C++ code that outputs the current value
of x at that point.

What a mess of confusion between syntax and purported meanings that
is. Again, you've not provided the reader with a way to mechanically
verify that the lines in your "proofs" are results of purely
syntactical operations on previous lines.

From that point onward the expression x=1:1:I represents the C++ code

I did not write that.

for iterating through the values from 1 to I. It is used to construct
the final program, above. So in Program 1, the expression A=1:1:J
("informally") represents the C++ code to iterate variable A from 1 to
J.

I now realize that it takes a lot for people to learn the detailed use
of CBL to perform Program Synthesis. To me it is obvious and so
simple - in hindsight.

Because it is a sketchbook for various notions you have in your own
mind, but you haven't given a rigorous system that admits of objective
syntactical verification, thus it is not a formal system but indeed
remains a kind of free-form sketchbook of your own notions and thus
requires having your various personal notions to make sense of it.

The lesson is that Program Synthesis is
performed by combining primitive programs using a small set of
universal rules for combining programs together. That's how Program
Synthesis actually works, and it is a lesson that has eluded published
papers to date.

About 6-8 people have volunteered to help me implement (program) CBL.
I tried a couple of years ago to organize the effort, but it was
difficult using only an email address and a word processor. I decided
that I needed a web-site to organize the many questions and offers of
support (I have done nothing to promote it beyond the ARXIV paper and
Google Groups posts.) Hopefully my new home pagewww.charlie-boo.com
will soon be the hub of all CBL development.

Sure, a real hub.

Notably, we are never provided with a rigorous definition of what a
program is, nor does the semantics provide a rigorous definition of
what it means for a program to halt; that is, there is no actual
mathematical definition of the notation Q(I,x)_H.

Again, not written by me, but rather quoted by me.

The key statement is "(We decide upon a single programming language
for all of our discussions.)", which is a pretty standard approach.
All we really need is for the program to follow the general form of a
CBL program, i.e., to be expressible in terms of the control
structures FOR, SET, IF and WRITE. This suffices for all of the
examples that I give and is true of conventional programming languages
such as C++.

To bad that with all your false boasting you can't provide a self-
contained system but rather must send everybody scurrying to see how
whatever it is your are trying to say is actually found in existing
programming languages anyway as then interpreted through some ad hoc
informal reguritation mixed with various of your own confused
notions.

Of course, without an actual syntax for his theory and only an
informal, quasi-mathematical semantics, it is pretty much impossible
to verify all of the alleged theorems that follow, let alone C-B's
oft repeated claims about how CBL proves the undecidability of the
halting problem, Gödel's theorem, Rosser's theorem, etc.

See VII. Unsolvable Wffs.

We saw it. A mess doesn't get less of a mess the deeper it gets.

The key statement is, "the standard syntax of the Predicate Calculus
is used (~ not, ^ and, v or, (e) there exists, (a) for all, A B C ...
variables, '...' literals)." All of the CBL expressions here are
Predicate Calculus wffs. I do add the H subscript to mean that the
program that calculates it halts (an important distinction in
practice.) The use of I and X variables is still Predicate Calculus
syntax. I extend the semantics to interpret P(I) to mean that we have
a program that decides set P, P(x) means we have a program that
enumerates set P, and P(x)-H means we have a program that enumerates
set P and then halts (so P must be finite.)

And your very first application of a rule in a "proof" in that paper
is an application of a "rule" that requires considerations (such as
dovetailing) that go well beyond any purely syntactical rules you have
yourself stipulated.

How ironic that you claim your mess to be an axiomatization of
computer science when your "axiomatization" ITSELF depends on having
ALREADY presumed a huge amount of computer science.

a definition of "Turing Machine" is not to be found.

Turing Machines (aka programs) are axiomatized in section VI:

"Universal Set: { 1, 2, ... }

Relations
1. TRUE(a) "a is any value in the universal set."
2. YES(a,b) "Turing Machine a halts yes on input b."
3. NO(a,b) "Turing Machine a halts no on input b."
4. HALT(a,b) "Turing Machine a halts on input b."
5. NIT(a,b,c) "Turing Machine a halts no on input b at iteration
number c."
DEF
1. P , ~~P Law of Double Negation
2. P ^ Q , Q ^ P Commutative Law of Conjunction
3. P v Q , Q v P Commutative Law of Disjunction
4. ~(P ^ Q) , ~P v ~Q DeMorgan's Law for Conjunction
5. ~(P v Q) , ~P ^ ~Q DeMorgan's Law for Disjunction
6. P v (Q ^ R) , (P v Q) ^ (P v R) Distribution of Disjunction over
Conjunction
7. P(a) , TRUE(a) ^ P(a) Property of Universal Set
8. P(a) v ~P(a) , TRUE(a) Tautology
9. HALT(a,b) , YES(a,b) v NO(a,b) Definition of halt
10. NO(a,b) , ($A) NIT(a,b,A) Definition of halting no
11. YES(a,b) , YES(a,b) ^ ~NO(a,b) Consistency of Programs

Axioms
1. TRUE(x) We can list the Universal Set (Peano).
for x=1:1 write (x)

2. NIT(I,J,K) We can tell if a Turing Machine halts no
if NIT(I,J,K) write (true) at any given iteration (universality).
write (false)"


That is NOT a DEFINITION of 'Turning machine'.

Why don't you just look at a book such as Martin Davis's
'Computability And Unsolvability' for a mathematically rigorous
definition 'Turing machine' (which definition and discussion, by the
way, is easily done in Z set theory, I mention since you are disputing
that set theory can't develop computability theory).

an "Incompleteness Axiom" just appears on the scene: -~YES(x,x). But
what the values of x are supposed to be here is unstated. YES itself
simply appears in the preceding sentence

Again, not written by me, but rather quoted by me.

As explained by definitions, this means that there is no program that
enumerates the values x such that x is not the number of a program
(Turing Machine) that halts yes when run on x as input. All
incompleteness theorems are proven by reducing to expression
~YES(x,x). (BTW It is more general to reduce to ~YES(x,x) than to
reduce to the Halting Problem HALT(I,J), which is the common informal
approach.)

And that thread is yet another example of your ineptitude

No, it's an example of miscommunication.

You can't communicate coherently on such subjects as were discussed
since you have not taken sufficient time out from your infatuation
with your own personal notions to understand the basics of the subject
that was under discussion.

Our VERY FIRST CONVERSATION was as to the
technical matter of the definition of 'wff of the language of ZFC' in
which I answered your question but you never (even after I asked you a
few times) responded to my question as to what your point is in asking
such a question and having people provide you with such information.

Time to move all of this towww.charlie-boo.com?

You're a clown. You still don't say what your purpose is in having
people provide you technical definitions that you ignore anyway but
suggest instead that the conversation re-locate to a web site that is
not even running. Poor misunderstood Charlie-Boo.

MoeBlee


.

Relevant Pages

  • Re: Godel proved maths inconsistent not incompleteness theorem
    ... a Turing Machine that halts yes on just its elements. ... You are assuming that CBL is at a different level of abstraction than ...
    (sci.logic)
  • Re: A resolution to the Russel paradox
    ... diagnoalization to wit a Turing Machine that tells if a Turing Machine ... halts, a wff that expresses and/or represents whether a given wff is ...
    (sci.logic)
  • Re: Rados Sigma and the Halting Problem for Programs
    ... AD> computer language that does not contrive a logic paradox ... Halting Theorem may be proven without recourse to reductio ... computation halts, and is bottom, i.e. _|_ if the computation diverges ... Assume that from a Turing Machine M we can construct a Turing Machine ...
    (comp.theory)
  • Re: Rados Sigma and the Halting Problem for Programs
    ... AD> computer language that does not contrive a logic paradox ... Halting Theorem may be proven without recourse to reductio ... computation halts, and is bottom, i.e. _|_ if the computation diverges ... Assume that from a Turing Machine M we can construct a Turing Machine ...
    (sci.math)
  • Re: Rados Sigma and the Halting Problem for Programs
    ... AD> computer language that does not contrive a logic paradox ... Halting Theorem may be proven without recourse to reductio ... computation halts, and is bottom, i.e. _|_ if the computation diverges ... Assume that from a Turing Machine M we can construct a Turing Machine ...
    (sci.logic)