Re: Catalog of undecidable problems?



tchow@xxxxxxxxxxxxx wrote:
> In article <1117695210.491930.53720@xxxxxxxxxxxxxxxxxxxxxxxxxxxx>,
> george <greeneg@xxxxxxxxxx> wrote:
> >Well, one could PERHAPS (I'm ignorant) begin by
> >formalizing first-order-proof-IN-GENERAL in PA; that
> >might (if achieved)largely moot my objection.
>
> Not sure what this means.

OK, here's one thing it might mean. Godel basically
exhibited that first-order-provability-from-PA
could be formalized in PA. If that is the case
then it must follow that provability in anything
strictly weaker than PA can also be formalized in PA.
In particular, it implies that provability from the
absolutely weakest initial axiom-set possible, namely
the empty one, can be formalized in PA, i.e., that first-
order validity can be formalized in PA. Arguably,
having done this, one could formalize provablity in any
more complicated axiom-set (as long as it was recursive,
like ZFC) simply by noting that, by the compactness
theorem, everything that is provable from ZFC is provable
from some particular finite set of (instances of) axioms
of ZFC, and if this set is P (and the provable theorem is
T), then P->T is valid. The only thing you'd stand
obligated to formalize AFTER that would be
"P is a finite set of axioms of ZFC". The conjunction
of these two would be equivalent to "T is provable from ZFC".

> A basic sticking point, perhaps the
> biggest sticking point, is that mathematicians
> freely use infinities and set-theoretical
> constructions in their work. If your goal is to
> create a proof in PA, then these invocations
> have to be circumvented and eliminated.

Arguably not. They just have to be moved to the
hypothesis of a conditional, so that what you are
trying to prove becomes a pure validity as opposed
to a theorem of ZFC -- That is, IF you are trying
to PROVE something: for you might, instead, be trying
to show something UNprovable.
One place you might need an infinitary construction is
in the construction of an infinitary model: once you've
proved the existence of this model, you've shown (perhaps)
that something is NOT provable. Independence results have
had major historical importance and they really are a
different breed of cat from "proven" or derived results.
We are in fact usually in a realm where proofs have to be
finite AND models have to be infinite. Discovering a proof
implies that something is provable from some axioms;
constructing a model often implies that something was NOT
provable. Constructing (finitary) proofs and constructing
(infinitary) models are arguably two fundamentally opposite
kinds of work.

.

Relevant Pages

  • Re: THIS STATEMENT HAS NO PROOF IN ANY SYSTEM = true or false?
    ... The first point is that ZFC is a set of axioms whereas V is the class of all ... To formalize "S is provable in ZFC" we need to ... The provability predicate is a monstrously complicated thing if written ... What is probably generating confusion is the familiar sociological fact ...
    (comp.theory)
  • Re: THIS STATEMENT HAS NO PROOF IN ANY SYSTEM = true or false?
    ... The first point is that ZFC is a set of axioms whereas V is the class of all ... To formalize "S is provable in ZFC" we need to ... The provability predicate is a monstrously complicated thing if written ... What is probably generating confusion is the familiar sociological fact ...
    (sci.math)
  • Re: THIS STATEMENT HAS NO PROOF IN ANY SYSTEM = true or false?
    ... The first point is that ZFC is a set of axioms whereas V is the class of all ... To formalize "S is provable in ZFC" we need to ... The provability predicate is a monstrously complicated thing if written ... What is probably generating confusion is the familiar sociological fact ...
    (sci.logic)
  • Re: Why is ZF not finitely axiomatizable?
    ... first-order logic is provable in ZFC. ... conclude from the provability of the cut-elimination theorem that it ... quantifier complexity less than equal to P. Alas, induction is not ...
    (sci.logic)
  • Re: Is this proof valid?
    ... in polynomial time; thus, PROVABLE_X is an element of P. ... Still working in ZFC, assume P!= NP. ... non-membership in P to the provability of P!= NP? ... cannot be solved in polynomial time, then ZFC is provably consistent. ...
    (comp.theory)