Re: Godel proved maths inconsistent not incompleteness theorem

On Apr 27, 2:46 pm, Chris Menzel <cmen...@xxxxxxxxxxxxxxxxxxxx> wrote:
On Thu, 24 Apr 2008 17:05:03 -0700 (PDT), Charlie-Boo
<shymath...@xxxxxxxxx> said:





...
Well, let's see. First of all, where is the list of the formal ZFC
axioms that you would use?

I found the following site:

 http://pine.cs.yale.edu/pinewiki/SetTheory

Since I am not a mathematical logician, I am not sure that they are
correct.

The question is how Mr. Koskensilta would like to represent them.  As
far as being correct or not, I have read of a number of expositions
that people other than the author claim are not correct, and at least
one for which it is said that nobody is quite sure if it is right or
not.

The problem becomes nontrivial very quickly.  I don't know why some
people are so foolish as to not know "The devil's in the details."  As
a computer programmer, I know that, as in any system with multiple
levels of abstraction, you verify specs (for completeness,
consistency, ambiguities, etc.) by going down a level: written specs
=> formal ("programmable") specs => program algorithms => executable
code.  And at each level you find problems with the level above, you
go back up a level and try to fix it, and work your way down to the
lowest level, executable code.

This is just so much crap, all this talk about multiple levels of
abstraction, verifying specs, executable code, etc in reference to proof
checkers.

That is how I have been implementing software systems for many years.
After 10 years, 4% of my notes were on how to improve the execution
speed of software. From that I wrote a 184 page book. I could easily
write 500 pages on designing and implementing systems.

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, and in particular how it handles each construct in a
wff. That of couse depends on how wffs are represented.

 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
(or a programming construct for checking whether a given value is in a
given list.)

 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.

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

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. The first task is to make sure
the system does everything you want. That is the spec. Then you can
design code to manipulate it.

Since ZF has already been specified (supposedly), then we are at the
point of designing the proof checker. But Atta seems to have a
problem even deciding how to represent the axioms.

But I have sympathy for him. Authors have that same problem - there
are at least a dozen versions of the ZF axioms per se, and probably an
equal number of ways of represeting the complete set of axioms.

Anyone who has develped code of any complexity knows you can never
tell how big a task is until you spec it out. That's why companies
don't give quotes for software development without the spec. And just
developing the spec is a big job. First the customer pays to have a
spec developed, which includes a price for implementing it. Then they
pay to implement it (if they can afford it.)

Programmers laugh at companies who quote projects without complete
formal specs. And what I am hearing now is equivalent to a price
quote. It's like a BS salesman, "Oh, we can do it easy." and the
programmer rolls his eyes. "Yeah, and who has to try to meet his
deadline which was made without even specing it out, much less
performing a technical design to get an idea of how long it will
take." and "Yeah, anything is easy if you don't have to do it. Talk
is cheap. . . ."

"It's trivial." Atta must be an ex-salesman.

C-B
.

Relevant Pages

  • Re: Godel proved maths inconsistent not incompleteness theorem
    ... ZFC axioms that you would use? ... about programming the factorial function. ... WFFs) follows from WFFs occuring earlier in the sequence by a rule of ... That is the spec. ...
    (sci.logic)
  • Re: Godel proved maths inconsistent not incompleteness theorem
    ... ZFC axioms that you would use? ... about programming the factorial function. ... First you write a WFF ... needs to be a routine that recognizes it. ...
    (sci.logic)
  • Re: (Not quite) Cantors diagonal proof
    ... So MetaMath doesn't create theorems, ... their links, only states an assertion concerning classes or wffs, as ... drilled down deeper and deeper until axioms will ultimately be found ... df-2 seems to be taking an arbitrary wff ...
    (sci.logic)
  • Re: (Not quite) Cantors diagonal proof
    ... So MetaMath doesn't create theorems, ... their links, only states an assertion concerning classes or wffs, as ... drilled down deeper and deeper until axioms will ultimately be found ... df-2 seems to be taking an arbitrary wff ...
    (sci.math)
  • Re: truth/falsity of sentences in first-order logic
    ... substitute different functions and relations, ... This is at a higher level of abstraction than theorem-proving. ... axioms must be TRUE of these specific functions and relations. ... those used in the wff. ...
    (sci.logic)