Re: Godel proved maths inconsistent not incompleteness theorem

On Apr 30, 12:59 pm, Chris Menzel <cmen...@xxxxxxxxxxxxxxxxxxxx>
wrote:
On Wed, 30 Apr 2008 01:54:34 -0700 (PDT), Charlie-Boo

Can you code from specs that contain "e.g." and "etc."?

I'm not giving you a spec.

That's the problem. You don't even have a spec and you say it's
trivial.

That of couse depends on how wffs are represented.

No kidding. Presumably, they are "represented" they way WFFs are
typically "represented" in first-order languages, as strings in a
certain recursively defined set. Standard stuff.

Then why do the various expositions use different syntaxes?

Zohar Manna and Richard Waldinger gave up trying to implement
Inductive proofs years ago.  

*Inductive* proofs?  You think that is even *relevant* in a discussion
of *deductive* proof checkers?  Just how confused *are* you about the
issues here?

ZF without Induction??

Then why can't you give programmable specs?  

Er, how does it follow that I can't give programmable specs?

The above.

the task
is so straightforward that it would be a pointless exercise in pedantry.

Now you're using synonyms for "trivial".

As mentioned already, I gave you a link to a fully implemented proof
checker for a complete system of natural deduction, one that, in
particular, implements 20 of those rules of inference that you call "the
hard part".  All one would have to do to convert it into a dedicated
proof checker for ZF, PA or what have you would be to implement some
elementary pattern matching routines for the axioms/schemas of your
chosen theory.

Oh, I see. It's trivial if you already have a program that does 90%
of it.

But, even then, be careful. Have you ever heard of people spending
more time trying to get existing software to work than it would take
to write it themselves?

1. For each line in the purported proof
  a. Run one step of the theorem prover
2. For each theorem generated, compare it to the theorem at that line.
3. If equal, then go to the next line (1)
   a. If no more lines, the proof is valid.
4. If no more theorems to generate, the proof is not valid.

So you think hard things are easy and easy things are hard.

There is a pretty serious problem with your algorithm,
specifically the "If no more theorems to generate" condition in line 4
-- you *do* know there are infinitely many theorems of first-order
logic, right?

There are a finite number of theorems at that single step.

There are a number of popular axiomatizations
of ZFC.

I thought you said that the syntax is standard?

Really?  (I) wonder what it was I was doing when I laid out a computing
project and sketched out pseudo-code... :-)

That makes two of us.

or had anyone ask for your autograph or take your picture at a
computer conference.

Gosh, this is just sad.

No, it was pretty cool, actually. (You didn't answer the question.)

Anyone who has develped code of any complexity knows you can never
tell how big a task is until you spec it out.

Sure, to some extent, but if you've got a firm grasp of your subject
matter, some programming talent and some experience behind you can often
tell that a given task is going to be routine.  Writing a proof checker
for example.

Like I said, this sort of thing comes from a blend of book learning,
experience, and natural ability.

I thought it was trivial - why does it now take all that? Trivial if
Andrew Wiles did it?

Time to drop the discussion of what's trivial or not. (You can have
the last word if you want.)

C-B
.

Relevant Pages

  • Re: Godel proved maths inconsistent not incompleteness theorem
    ... equals that line. ... I never said that's how a proof checker works. ... tell how big a task is until you spec it out. ... a competent logician and programmer who understands the difference ...
    (sci.logic)
  • Re: Godel proved maths inconsistent not incompleteness theorem
    ... theorem prover for one step and see if any of the theorems proven ... to write a proof checker - the sketches you were given ... tell how big a task is until you spec it out. ... a competent logician and programmer who understands the difference ...
    (sci.logic)
  • Re: Open Sound Control
    ... 32bit int)) will not work with the OSC spec. ...   - indexing pass, scan this list one variable-length thing at a time, ... The 1 to 4 nulls is the correct spec for strings, ...
    (comp.lang.tcl)
  • Re: FunctionExpressions and memory consumptions
    ...   if { ... is an increased memory consumption in such cases. ... So, as far as I understand, function expression in "unreached" block ... Does spec actually define such behavior (object ...
    (comp.lang.javascript)
  • Re: Zoom H2 Handy Recorder - Brilliant!
    ... a device say its "USB 2" means nothing without it also saying what mode ...     USB2.0 Full-Speed compatible ... And the USB 2 spec says... ...
    (rec.audio.pro)