Re: Godel proved maths inconsistent not incompleteness theorem

On Wed, 30 Apr 2008 01:54:34 -0700 (PDT), Charlie-Boo
<shymathguy@xxxxxxxxx> said:
No one is denying that it is not *in general* a good methodology for
developing software systems. The comment was in reference to
programming a proof checker. You are blowing smoke when you try to make
it sound like a major undertaking in software development. It just
isn't.

You can't even give the algorithms needed much less program them that
quickly.

It's been *done*, you putz. I gave you the link.

Proof checkers are *easy* to write, and any competent programmer
who understands basic first-order logic knows it. First you write
a WFF checker for your language. For first-order languages this is
a simple little exercise in recursive programming. Then you write
routines to check whether a given WFF in a purported proof (i.e.,
a sequence of WFFs) follows from WFFs occuring earlier in the
sequence by a rule of inference -- modus ponens, univeral
generalization, whatever you've got in your chosen system.

No, first you have to list out and exactly define how each Rule of
Inference works...

Er, that is exactly what I mean by "routines to check whether a given
WFF...follows from WFFS occurring earlier in the sequence by a rule of
inference...." RoutineS, plural -- one for each rule of inference.

That's an algorithm?

What?? I'm only pointing out that the routines in question "list out
and exactly define how each Rule of Inference works".

I have no idea what this means. Each contruct? You mean, like, each
parenthesis? Rules of inference are based upon the grammatic forms of
WFFs. What you need for implementing them are routines (part of the
above-mentioned WFF checker) that analyze a WFF recursively in terms of
its grammatically salient constituent parts. In particular, such
routines tell you, e.g., whether a given WFF is a negation, conditional,
etc. Thus, for example, to see whether Q follows by Modus Ponens from
earlier WFFs, you look for earlier wffs P and P->Q.

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

Obviously not. But I'm not giving you a spec. Are you so muddle-headed
that you can't distinguish an informal description of how a program
works from a formal spec?

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.

Try it and you'll see the truth.

Uh, I did.

Add in some method for tracking assumptions (e.g., Fitch-style
subproofs or Lemon-style dependency tracking) -- a mildly challenging
exercise for a bright 3rd-year undergraduate -- and you've got the
makings of a proof checker for natural deduction systems.Here's a
simple one here:http://logic.tamu.edu/daemon.html. If you want to
build axioms into the system, then, for each axiom, there simply
needs to be a routine that recognizes it.

That would be a single equality check against each axiom in the list

Well, yeah, of course.

Then why would that take a routine? Actually, you keep them all in a
table, and you have the same look-up regardless of how many of them
there are.

Newsflash: "For each X there needs to be a Y" does not imply that each X
needs to have its *own* Y. That said, it is by no means obvious that
you wouldn't want to have separate routines -- in proof checker for a
natural deduction system in which one annotates each line in a proof
with its justification, it would be faster to use the annotation to go
directly to a separate routine for checking a purported axiom than to
have to run through a list of axioms in a table.

But asking if something is an axiom is the trivial part. Applying
rules of inference is the hard part.

For you, I can well imagine, since there's little evidence you have a
clear conception of what a rule of inference even is.

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?

For axioms that are not given via a schema, this is just
a matter of storing them and having a routine that tells you when two
given WFFs are identical, or, more flexibly, alphabetic variants of one
another. For axioms given via schemas, it is a matter of storing a
template and writing a routine that tests whether a given WFF is an
instance of the template. All are elementary programming tasks.

Then why can't you give programmable specs?

Er, how does it follow that I can't give programmable specs? I could
give you specs for programming the factorial function, too, but the task
is so straightforward that it would be a pointless exercise in pedantry.

That means it actually describes the details of how algorithms work.

No kidding.

As I predicted, it is getting thicker and thicker. And we have barely
begun.

Rubbish. We're done. It's completely trivial stuff. I could write
(indeed, I've written) routines to add this functionality to the system
above in a few dozen lines of perl code. The more axioms, of course,
the more code, but each routine in itself is an entirely elementary
task. If you think otherwise, then you have no idea what it is involved
in programming a proof checker.

Pure bluster. All talk and no beef.

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. But given how difficult you think it is to implement
rules of inference, I'm not surprised you find the idea of pattern
matching completely daunting.

Being forced to program something is a wonderful way to sharpen
your understanding of it.

Great advice. I'd suggest you start with a proof-checker for
propositional logic and go from there.

I've written programs to generate theorems in Lambda Calculus,
Combinatory Logic, and some of CBL.

I'd love to see them. Where can we download them?  But you *do*
realize, don't you, that all we're talking about here is proof checking?
And you do understand there is a huge difference between proof checking
and theorem proving, right?

Yeah. For each line of the purported proof you have to run the
theorem prover for one step and see if any of the theorems proven
equals that line.

*choke* My gawd. I guess I shouldn't be surprised, but you really
*don't* have any idea what a proof checker is.

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.

You mean "the purported theorem at that line", I guess.

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.

Well, I'll grant you that you've certainly *made it* hard! No wonder
you can't write a proof checker for CBL. (Well, the fact that it is
completely ill-defined aside...) But this really is no surprise. Your
"spec" of CBL does not contain a well-defined deductive system, so it is
no surprise that you don't know what a proof is.

That said, 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? So suppose someone enters an invalid sentence S in a
purported proof. Then the condition of line 4 in your algorithm will
never be satisfied and the algorithm will run forever. There is of
course a partial fix here if S is a logical falsehood -- you could have
your theorem generator looking for ~S. But, of course, first-order
validity is only semi-decidable. Hence, if S is invalid but not a
logical falsehood, then when you run your algorithm and you reach
sentence S, your theorem prover will never generate it and again your
algorithm will run forever.

C-B, this is *such* basic stuff. It's rather appalling that you blather
on as you do when you obviously have no idea what you are talking about,
even regarding the most elementary concepts of mathematical logic.

I will be charitable and chalk up this misrepresentation of the facts to
your own inadequate grasp of the basics of mathematical logic rather
than deliberate dishonesty. ZFC is a *theory* -- by definition, a
deductively closed set of sentences. An *axiomatization* of ZFC is a
recursive set of sentences whose deductive consequences are exactly the
sentences of the theory. There are a number of popular axiomatizations
of ZFC. From a logical point of view, they are all equivalent; it
doesn't matter which axiomatization you choose.

It does when you're the one who has to write the programs.

Yet further confirmation that you have absolutely no idea what you are
talking about...not that any more evidence is needed than your algorithm
above.

So a choice will always be determined either by simple aesthetics --
perhaps you prefer to use the axiom schemas of collection and
separation instead of just replacement -- or by practical
considerations.  For the purposes of a proof checker, it would be
easiest to choose an axiomatization with the fewest number of
axioms/schemas, simply because there would be fewer subroutines to
code.

You forget the 80/20 rule.

And you forgot to learn elementary logic.

But I have sympathy for him. Authors have that same problem - there
are at least a dozen versions of the ZF axioms per se,

At least. Big deal. There are also dozens of different semantically
complete systems of first-order logic. Everyone who understands
elementary logic knows that these are simply alternative paths to the
same end. One chooses one approach over another based upon one's
practical purposes and aesthetic sensibilities. This is part of the
general freedom there is in mathematics that one has in studying an
abstract domain.

You've obviously never designed software (maintenance, maybe),

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

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

Gosh, this is just sad.

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.

Perhaps so. But we *do* know how big a task it is to program proof
checker, so all of this gassing on your part is a red herring.

How can you tell without seeing the design or deciding which axioms
have to be processed?

Like I said, this sort of thing comes from a blend of book learning
(which you seriously lack), experience (which perhaps you have), and
natural ability (jury's out on this one). Given that you lack at least
one of these critical ingredients, it's no surprise you don't understand
this.

.

Relevant Pages