Re: incompleteness and inconsistency



lugit...@xxxxxxxxx wrote:
No one has actually given a direct, certain consistency proof,

How do you define 'direct, certain proof'?

To my mind, a proof requires axioms and/or rules of inference,
preferably formal. But even in an informal context, there are still
some general principles upon which the proofs depend, right? (And is
there anything that is informal that can't be formalized, even informal
meta-theory? I am strongly inclined to Hilbert's thesis, which (I hope
I am stating correctly) is that if a proof can be given then the proof
can be formalized at least in principle.)

As I understand, it is proven finitistically that there is no
finitistic proof of the consistency of first order PA. And 'finitistic'
can be defined as 'within PRA'. (Do I have these points correct?)

So, if 'direct, certain proof' means 'finitistic', then it would seem
that there is no direct, certain proof' of the consistency of PA.

But, ordinary mathematical proofs occur in set theory or at least
freely use principles of set theory even if the proofs are informal.
So, why would such a set theoretic proof of the consistency of PA be
considered any more dubious than other ordinary mathematical proofs?
(This is a rhetorical question that Torkel Franzen asks and it makes
great sense to me.)

But my own question is:

If we consider PRA to be the "embodiment" of finitistic proof, don't we
still rely upon infinitistic set theory to be the meta-theory for PRA?
Isn't some infinitistic set theory needed even to FORMULATE the
language of PRA? How could we formulate our paragon of finitistic
mathematics without doing it without using infinite sets (such as sets
of symbols)? If we cannot, then my feeling would be that set theoretic
principles are the "buck stops here" of mathematics anyway. (And I
admit that I' haven't defined "the buck stops here".)

Thanks in advance for any helpful comments or criticisms of my attempt
to grasp some part of this subject.

MoeBlee

.



Relevant Pages

  • Re: Internet, Goldbach conjecture, cranks and anticranks.
    ... Of course, anyone is free to doubt the basic principles of set theory, but then there is no particular reason for him to care about ZFC or to be interested in proofs of ordinary mathematical statements that use these principles. ... ZFC is not special in this regard, as Rudolph notes - we could with equal justification claim that no one can know that the axioms of PA are true, or even that no one can know anything at all in mathematics. ...
    (sci.math)
  • Re: The meaning of set?
    ... sound argument and what you don't. ... So we have a precise characterization of what ... We have a precise characterization of what counts as correct reasoning, though we have no precise characterization of what counts as an acceptable principle of set theory. ... In practice, the axioms of ZFC are sufficient, but an indefinite number of principles not provable in ZFC follow form the basic informal principles of set theory, although this observation isn't at all interesting in context of ordinary mathematics; also, in practice we almost never produce machine checkable proofs, only proofs we're sure could be formalized in ZFC in some idealized sense. ...
    (sci.math)
  • Re: Should we worry about contradictions?
    ... we all know that Global compherension leads to ... someone could conclude that Cantor believed such a thing. ... to find what principles it relied on, and ZFC was developed from that. ... formalized set theory in order to fix the contradiction" seems to have ...
    (sci.math)
  • Re: Godels comments about the "true reason" for incompleteness
    ... On 2008-03-18, in sci.logic, MoeBlee wrote: ... formalizable in PRA or Robinsion arithmetic or PA or even Z set theory ... - all first order theories. ...
    (sci.logic)
  • Re: Godels comments about the "true reason" for incompleteness
    ... formalizable in PRA or Robinsion arithmetic or PA or even Z set theory ... - all first order theories. ... Not bad for rookie off the bench. ...
    (sci.logic)

Loading