Re: Godel proved maths inconsistent not incompleteness theorem

In article
<f0626702-e936-4889-9bb4-8683c3fcf0be@xxxxxxxxxxxxxxxxxxxxxxxxxxxx>,
Charlie-Boo <shymathguy@xxxxxxxxx> wrote:
[cut]
Do you think a "formal proof" must include an "actual
proof" (like those we learned in Math class)?

No.

None of the 78 proofs
of the Pythagorean Theorem from the web page that I posted is more
than a few lines long - I assume the actual proof you are formalizing
can't be that big. Why not give it here?

There is no actual proof that is being formalized. Its size is zero.

We are not formalizing a natural language proof. We are proving a
theorem.

Honestly, when someone says they have something, and every time I ask
to see it they say, "You can make it yourself.", I get the impression
that they're not being honest with me.

We say we have a formal proof: you say can I see it. We show it to you.
You say that is not a formal proof: a formal proof needs to be
accompanied with a natural language proof and the formal proof should
only be a few lines.

Yes, you did not find what you were looking for. But, until recently, it
wasn't clear to me what you were asking. I thought you wanted a formal
proof (according to the standard meaning in mathematics). Now I know
that you want not only a formalized proof, but also the natural language
proof that is being formalaized. Yes, you won't find that in most of the
books that were recommended to you. You can stop looking. I agree that
what you mean by formal proof probably appears no where except in CBL.

The proofs of the Pythagorean
Theorem are pretty simple - why not explain which proof you are
formalizing?

But it's not a personal thing. It is just a Mathematical principle -
Mathematical statements must be substantiated, assertions must be
proven - otherwise it is not Mathematics.

This is your opinion. I don't agree with it.

 >> You asked for a ZF proof, not a proof that it "corresponds to
 >> nature."
 >
 > "Corresponds to nature" means represents (maps to) an actual proof.

Perhaps by "actual proof" you mean a proof outline.  An outline
of the proof is as follows.

Where's the part about a triangle, the square of the hypotenuse, etc?
It's a simple theorem and it has many simple proofs. Can you just
prove the original theorem and not get into other subjects which only
obfuscate the explanation?

I'm sure you want people to read and understand it, so why introduce
all of this extraneous stuff? The Pythahorean Theorem can be proven
in just a few simple lines using only principles from elementary
Geometry.

But, we are not using the axioms of Euclid. We are using the axioms of
ZFC. It does not follow that the Pythahorean Theorem can be proven in
just a few simple lines. In ZFC, we are not allowed to use the
principles from elementary Geometry that are based on the axioms of
Euclid. We are not using the axioms of Euclid! Thus, we cannot use those
principles from elementary Geometry that you are referring to.
.

Relevant Pages

  • Re: What is a proof, exactly?
    ... Because that's what proving things is all about. ... proof - I'm trying to get to know what that standard looks like. ... there is a formal proof, being a sequence of statements following from ... be possible to actually have a foundation for mathematics based purely on ...
    (sci.math)
  • Re: Definition of Mathematics and Above
    ... I allow that one may have a notion of informal axioms for informal ... can't be meaningful non-axiomatic mathematics. ... The high level summary of the purported ZFC proof that nobody is able ... each line of some formal proof of the theorem ...
    (sci.logic)
  • Re: Definition of Mathematics and Above
    ... I allow that one may have a notion of informal axioms for informal ... can't be meaningful non-axiomatic mathematics. ... The high level summary of the purported ZFC proof that nobody is able ... each line of some formal proof of the theorem is translated ...
    (sci.logic)
  • Re: Godel proved maths inconsistent not incompleteness theorem
    ... One CBL formal proof of the unsolvability of the Halting Problem ... I am trying to "speak" your language: I said something in CBL and I ... BTW If a system produces theorems ... Briefly, I am trying to understand things: in mathematics, logic, ...
    (sci.logic)
  • Re: alternate characterization of the class NP?
    ... replaced a simple certificate with a formal proof. ... specify which axioms for mathematics you're using. ... If you Google "Goedel completely convinced Turing's paper" then you will ...
    (comp.theory)