Re: Godel proved maths inconsistent not incompleteness theorem

On Sun, 27 Apr 2008 09:47:17 -0700 (PDT), Charlie-Boo
<shymathguy@xxxxxxxxx> said:
On Apr 26, 8:24 am, Aatu Koskensilta <aatu.koskensi...@xxxxxxxxx>
wrote:
On 2008-04-25, in sci.logic, Charlie-Boo wrote:

My point was that if Atta is going to say that something is trivial,
then I ask for a little substantiation, starting with his choice of
formal axioms.

You will find a description of the formal axioms of ZFC in any number
of textbooks on the subject. There are minor differences in the choice
of axioms but these are all inessential.

The choice of how axioms are represented has a big affect on the task
of writing a proof checker.

He didn't say "choice of how axioms are represented" (what does it even
mean to "represent an axiom"?) he said "choice of axioms". That is,
there are different, logically equivalent, axiomatizations of ZFC. Be
that as it may, the task of writing a proof checker for any common
axiomatization would be a simple task for any competent programmer, as
you'd discover if you actually desired to learn something instead of
just blowing smoke.

It also allows us to be explicit in describing how "trivial" it is to
write a proof checker for those axioms.

Which representation would you use to write your trivial proof
checker? Then we can talk about how rules of inference can be applied
to them, from a computer programming point of view.

Sheesh, just pick one. Use the ones on Wikipedia.

.

Relevant Pages