Re: Newberry's Theses

On Apr 26, 7:43 am, Aatu Koskensilta <aatu.koskensi...@xxxxxxxxx>
wrote:
On 2008-04-26, in sci.logic, Newberry wrote:

In the same theory where 2 + 2 = 4.

What theory is that? And how do you think Godel's theorem establishes
that there is no proof that establishes with absolute certainty the
truth of Godel's sentence of that theory?

I do not quite understand what you are trying to say in the last
sentence, but mathematically compelling arguments are indeed the
issue. That is exactly what I am saying. But you and particularly
Daryl McCullough insist that the consistency of PA is *provable* in
ZFC. OK, I used imprecise terminology and definitions. Mea culpa. But
why the heck did we need to waste time going in circles when the issue
are mathematically compelling proofs, proofs with cogency?

It is only because you're confusing the two notions of proof,

Are you saying that we have two sets of proofs? One set of formal
proofs for shuffling around meaningless marks on paper and another set
of informal mathematically compelling arguments?

that of
a formal proof in this or that theory, and that of a mathematically
compelling argument. Godel's proof doesn't tell us anything of whether
the consistency of some given theory is provable in the latter sense,
and the provability of the consistency of this or that theory, in the
latter sense, does not contradict any result of Godel's.

Now having said that let's go back to reality. The formal proofs were
not designed to be an empty game with meaningless marks on papaer. We
do not have one set of formal proofs just for playing games with
symbols and another set of informal proofs to obtain the truth of
mathematics. On the contrary the formal proofs were designed to make
the informal proofs more rigourous, to dispel the last remnants of any
doubts that the theorems were true.

Mere formalisation does not dispel any doubts, except as to the
logical correctness of the argument. It's just as possible to doubt
the basic principles if they are presented formally as it is when they
are presented informally, in ordinary mathematical English.

And all the informal mathematically compelling proofs can be
performed by a Turing machine?

What does it mean for a Turing machine to "perform informally
mathematically compelling proofs"? Nothing I've said hinges on
Platonism, non-Platonism or the truth of the philosophical doctrine of
mechanism.

--
Aatu Koskensilta (aatu.koskensi...@xxxxxxxxx)

"Wovon man nicht sprechen kann, daruber muss man schweigen"
 - Ludwig Wittgenstein, Tractatus Logico-Philosophicus

.

Relevant Pages

  • Re: Newberrys Theses
    ... proof that establishes with absolute certainty the truth of Goedel's ... not formal proofs in this or that theory. ... and the we prove mathematics by informal mathematically compelling ...
    (sci.logic)
  • Re: Deep Thoughts # 17: Liar Paradox is a Formal Metamathematical Theorem
    ... Daryl McCullough wrote: ... Isn't truth independent of one's perceived ... Provability is defined in terms of logical ... such an axiomatic system for all of Mathematics.) ...
    (sci.logic)
  • Re: Newberrys Theses
    ... and the provability of the consistency of this or that theory, ... mathematics. ... On the contrary the formal proofs were designed to make ... the informal proofs more rigourous, to dispel the last remnants of any ...
    (sci.logic)
  • Re: Godel cant tell us what makes a mathematical statement true
    ... are identifying truth with provability. ... oppose such a truth definition I've given. ... define 'troo' as we had previously defined 'true'. ... mathematics just by redefining terms. ...
    (sci.logic)
  • Re: X = Z
    ... travel a path and return to its beginning, a goal of mathematics is ... that have otherwise generally canonical meaning. ... Fashion has nothing to do with truth. ... appear on the subject of 'primes' above and below mine, ...
    (sci.math)
Quantcast