Re: Godel proved maths inconsistent not incompleteness theorem

On Mar 27, 11:44 am, Charlie-Boo <shymath...@xxxxxxxxx> wrote:
On Mar 25, 4:35 pm, MoeBlee <jazzm...@xxxxxxxxxxx> wrote:
He doesn't know what a formal proof is.

Do you think that a proof created by running a computer program, with
no input from the user, would necessarily be formal?  

IF it were a proof in the sense of a finite sequence of formulas, each
either an axiom from a recursive set of axioms or derived by a
recursive rule from previous entries in the sequence. (Or another
format such as, tree, sequents, etc.)

Did you read my
paper that gives such a program and its output?

http://selfref.googlegroups.com/web/A%20Simple%20Generator%20of%20Inc...

Is that the same piece of garbage you asked me to read a few months
ago? If so, we already discussed it, so you would know I read it.

Do you know of any other paper that does this - show a computer
program that lists theorems with no input from the user (and thus was
actually generated by the program itself)?

I'm aware of research in automatic theorem proving. I've not
personally checked on whether such programs do perform as claimed.

I answer just about all your questions (that are substantive). But you
leave so many of mine still unanswered. For example, have you even
TRIED to see how that theorem in Boolos I mentioned as a typical
example is provable in set theory? And adding another: Did you even
bother to look at the expression I posted that renders the theorem
that any Boolean algebra is isomorphic to a field of sets? (By the
way, do you even know what that MEANS?)

MoeBlee
.

Relevant Pages

  • Re: Godel proved maths inconsistent not incompleteness theorem
    ... IF it were a proof in the sense of a finite sequence of formulas, ... either an axiom from a recursive set of axioms or derived by a ... How could output from a computer program be considered informal? ... axioms against any other system does not produce anything. ...
    (sci.logic)
  • Re: Undecidability in Physics
    ... we can calculate the behavior of any Turing machine under certain ... Here is a rule for this sequence. ... N.B. This rule can be written as a formal algorithm (or computer program). ... of the universe as mathematical functions, ...
    (sci.logic)
  • Re: Well Ordering the Reals
    ... I have always allowed that sequences can be countably infinite, ... like the sequence of standard naturals is. ... TO nor anyone else has produced any axiom system in which it can be ... at several removes from pure mathematics, ...
    (sci.math)
  • Re: an true information theory
    ... > Kolmogorov, Chaitin, Wolfram and so on, consider a non random>sequence, ... > a small program that generate pi, for example, which has no pattern, no ... is already interested in meaning within a statistically emergent mentality. ... Can the rule finding itself be done by some computer program? ...
    (sci.math)
  • Re: Why? [was Re: Cantor`s powerset theorem is false?]
    ... (and even question what it means to say that an axiom is true or to say ... whether a sequence of formulas is or is not a proof is computable. ... and visualization as devices for discovering proofs is also allowed as ... What would be the point of this hypothetical activity of producing formal proofs? ...
    (sci.logic)
Quantcast