[FOM] "feasible" proofs
Arnon Avron
aa at tau.ac.il
Sat Sep 14 03:19:23 EDT 2013
As you say, the main property of the concept of a proof
should be that there be an algorithm for deciding whether a
given formal structure is a proof, and if so of what sentence. The
reason is that while each of us accepts that there might be
persons clever than him/her (at least at a certain point...)
who can produce proofs of theorems that s/he can't, we do no want
to treat any person as an oracle. So failing to find a proof is one thing.
Being unable to check a claimed proof is another. And frankly,
the possibility that a very clever person will be able to
produce a proof of length feasible to him/her but not to me
is not taken be as something I should worry about... Well, maybe
a computer will be able to do so, but then my computer will
be able to check its proof. The principle remains the same: checking
a proof should in principle be a lot easier than finding one,
and this principle makes sense only if proofs are finite objects.
(I say "in principle", because frequently it is boring and exhausting
to read long proofs of others, and we prefer to reproduce
great parts of them ourselves rather than to follow the given proof.)
Arnon Avron
On Fri, Sep 13, 2013 at 10:12:48PM +0100, Alan Weir wrote:
> One assumption which seems to be accepted by all so far, in the debate on 'What is second-order ZFC', is that a derivation, a 'certificate', must be finite. Indeed one usually requires that there be an algorithm for deciding whether a given formal structure is a proof, and if so of what sentence.
>
> But of course in the formal languages and systems which are our idealisations of informal mathematical practice, all but a tiny fragment of the constructions contain more parts than the estimated number of neutrinos in the observable universe. Perhaps more telling: we know from speed-up considerations (in reverse, as it were) that no matter what formal system we work with, there will be provable formulae which are of 'feasible' length- their tokens can be grasped by us or at least by machines we can in some decent sense comprehend- but whose shortest proof will be unfeasibly long. This will be true even for polynomially decidable logic, a logic which is surely far too restricted to act as a formalisation of actual mathematical practice.
>
> Given all this, and assuming (as I think we should) that we nonetheless must idealise beyond the patchy fragment of our formal systems which we can feasibly digest, what is the rationale for idealising to systems, such as first-order logic, in which the theorems are recursively enumerable but the anti-theorems are not, and in which the derivations are of lengths vastly beyond anything we can grasp? Why is omega-logic not a candidate for an idealisation of our informal practice; or more powerful infinitary logics? And if they are, does the fact that (full, non-Henkin) 2nd order logic is not complete tell against it any more than the fact that first-order logic is not decidable or propositional logic is not polynomial-time decidable (if P is not NP)?
>
> I suggest there is no non-ad hoc limit on the power of the abstract idealisations which are formal systems, if they are to count as legitimate idealisations of informal proof.
>
> Alan Weir
> Roinn na Feallsanachd/Philosophy
> Sgoil nan Daonnachdan/School of Humanities
> Oilthigh Ghlaschu/University of Glasgow
> GLASGOW G12 8QQ
> ________________________________________
> From: fom-bounces at cs.nyu.edu [fom-bounces at cs.nyu.edu] On Behalf Of fom-request at cs.nyu.edu [fom-request at cs.nyu.edu]
> Sent: 11 September 2013 20:39
> To: fom at cs.nyu.edu
> Subject: FOM Digest, Vol 129, Issue 15
>
>
> Today's Topics:
>
> 1. Re: What is second order ZFC? (Richard Heck)
> 2. Re: What is second order ZFC? (Harvey Friedman)
> 3. Re: What is second order ZFC? (Colin McLarty)
>
>
> ----------------------------------------------------------------------
>
> Message: 1
> Date: Wed, 11 Sep 2013 11:46:50 -0400
> From: Richard Heck <richard_heck at brown.edu>
> To: Colin McLarty <colin.mclarty at case.edu>
> Cc: Foundations of Mathematics <fom at cs.nyu.edu>
> Subject: Re: [FOM] What is second order ZFC?
> Message-ID: <5230906A.9060906 at brown.edu>
> Content-Type: text/plain; charset="iso-8859-1"; Format="flowed"
>
> On 09/11/2013 11:17 AM, Colin McLarty wrote:
> >
> > And towards the end of his post Richard offers the following as if it
> > disagreed with Harvey:
> >
> > Nonetheless, there are lots of ways in which logic can be used in
> > the study of mathematics, mind, and world, and one should not
> > confuse unsuitability for one's own purposes with unsuitability
> > tout court. Solipsism, after all, is false.
> >
> >
> > But Harvey had already said what I quote from him above: "I'm not
> > talking about arbitrary interesting foundational purposes." And he is
> > obviously not talking about other non-foundational purposes. This is
> > not a point of disagreement. Taking it to be a disagreement may be
> > one source of confusion in this discussion.
>
> Well, we can ask Harvey what he had in mind, but it seems pretty obvious
> to me that he has made some pretty strong claims in other places, that
> seem to border on claiming that there is something fundamentally unclear
> about "truly" second-order theories---a viewpoint that is not exactly
> unknown in the history of logic. Indeed, just preceding the quoted
> remark, Harvey said that he was talking about "any of the usual
> classical foundational purposes". I'm not sure what that includes
> exactly, but it's a pretty broad claim. I was simply trying to point out
> that plenty of people interested in what one surely would have thought
> counted as such have been interested in (truly) second-order theories,
> and without simply ignoring the kinds of questions Harvey is asking.
>
> I'm all for finite representations of proofs. And I think axiomatization
> is a wonderful thing. I think it's a very nice question, for example,
> what kinds of axioms we should accept for the ancestral. The fact that
> we know no complete axiomatization is possible doesn't mean we shouldn't
> produce partial axiomatizations, and we can study them in the usual way.
> (To say that I am then treating the theory as "first-order" would be
> misleading at best and terminological quibbling at worst.) What it means
> is that we can never regard any such axiomatization as final and so that
> it will remain difficult to say, in some cases, whether some formula A
> does or does not follow, in ancestral logic, from some other formula B.
>
> Apparently, it is supposed to follow that ancestral logic is useless
> "for any of the usual classical foundational purposes". Why? Yes, it's
> useless for one particular salient purpose, and I'm sure there are
> others, too. But any stronger claim wants argument.
>
> Richard Heck
>
> -------------- next part --------------
> An HTML attachment was scrubbed...
> URL: </pipermail/fom/attachments/20130911/477d4727/attachment-0001.html>
>
> ------------------------------
>
> Message: 2
> Date: Wed, 11 Sep 2013 12:19:03 -0400
> From: Harvey Friedman <hmflogic at gmail.com>
> To: rgheck at brown.edu, Foundations of Mathematics <fom at cs.nyu.edu>
> Subject: Re: [FOM] What is second order ZFC?
> Message-ID:
> <CACWi-GU6BF4W_sADEBq9GZ+qKsvAn-JpneATKYJ0Ua=fHk+o9w at mail.gmail.com>
> Content-Type: text/plain; charset="iso-8859-1"
>
> Thanks to Richard Heck for replying to my question designed to get more
> specific about just what 2nd order systems are in general and in the case
> of ZFC - and what jobs they do or not do.
>
> >
> > Second-order ZFC is the theory, formulated in a second-order language,
> > whose axioms are the second-order versions of the axioms of first-order
> > ZFC. Its theorems are the second-order consequences of those axioms. The
> > problem is now to explain "second-order consequence". But, as always,
> > consequence is truth-preservation, so what we need to know is how to define
> > truth for a second-order language. Since quantification will be handled
> > largely as Tarski taught, all we really need to know is what "instances" a
> > quantified formula has.
> >
>
> This is one of the more common and reasonable ways of talking about second
> order ZFC as a system.
>
> But first note that there is no notion of derivation present in the above
> version. Thus 2nd order ZFC is not even remotely doing the work for f.o.m.
> that first order ZFC does.
>
> Also note that we have no way of even determining whether or not, say, the
> continuum hypothesis CH, is or is not a second order consequence. In fact,
> we easily see that
>
> 1) CH is a second order consequence if and only if CH is true.
> 2) not CH is a second order consequence if and only if CH is false.
>
> This is one of the worst possible states of affairs for a "foundation" for
> mathematics, which makes the above formulation completely unusable for
> various purposes.
>
> But how to fix these fatal flaws?
>
> Easy. Just move to the first order associate, which is something like
> Morse-Kelly class theory, or more meekly, NBG. These are minor variants of
> ordinary first order ZFC.
>
> Boolos's solution was to appeal to plural quantification, the locus
> > classicus for that discussion being his paper "To Be Is To Be a Value of a
> > Variable". Boolos insists, plausibly enough, that there are some sets none
> > of which is an element of itself, but denies, sensibly enough, that there
> > is any set of all the sets that are not elements of themselves. The
> > locution "there are some sets" should not, therefore, be regarded as
> > quantifying over sets.
> >
> > Boolos seems to have regarded plural quantification (i) as perfectly
> > intelligible in its own right and (ii) as a reasonable way of interpreting
> > second-order quantification. ...
> >
>
> I am interested in this idea in principle. But I have never seen a workable
> version of what second order ZFC is based on this idea, that gets around
> what I have said above. E.g., is there now a version of pluralistic ZFC
> where we avoid things like 1),2),, and also where pluralistic ZFC is really
> in some interesting sense more powerful than ordinary ZFC? E.g., something
> really between first and second order ZFC?
>
>
> > Another option is Frege's: regard second-order quantifiers as quantifying
> > over what he called "concepts", which are essentially a kind of function,
> > not regarded as any kind of set. Frege's explanation of what these are
> > appeals to an abstract notion of predication (unsaturatedness), which many
> > have regarded as difficult to understand but which, in my own view, is
> > actually pretty well understood nowadays. On this kind of view, the
> > semantics of a second-order language is itself simply to be given in a
> > higher-order language, as in work by Agust?n Rayo and Gabriel Uzquiano.
> >
>
> Once again, same question. Of course, there are obvious continuations of
> Morse-Kelly involving classes of classes of sets, etcetera.
>
> >
> > There is, of course, an obvious question how it is to be guaranteed that
> > the "second-order domain", if we want to speak that way (Boolos did not),
> > is as "big" as it is supposed to be. There is literature on this question,
> > as well. One option, pursued by Vann McGee (and, in a somewhat similar way,
> > by me) is to appeal to a notion of "open-endedness" that is also found in
> > some of Sol Feferman's work, though I'm sure Sol would not approve of the
> > use we make of it. Here there are more questions than answers, no doubt,
> > but the matter is hardly closed or hopeless.
> >
>
> Roughly in this arena of thought might be Concept Calculus, especially see
> The Eight Supernatural Consistency Proofs for Mathematics, and also the
> Divine Consistency Proof for Mathematics. In these, we never use the
> cumulative hierarchy of sets, and instead focus on objects and classes of
> objects only.
>
> >
> > As Harvey has said, there are features of second-order logic, perhaps
> > illustrated by (4), that make second-order theories useless for
> > foundational purposes *of certain kinds*. There is very nice work by Peter
> > Koellner exploring exactly why and how, but without simply assuming, as
> > Harvey seems to do, that completeness is non-negotiable. I don't myself
> > think completeness is non-negotiable: Partial axiomatization is perfectly
> > possible, in many cases, and will do much of what we want.
> >
> > Actually, I am not at all sure that I am regarding completeness as
> nonnegotiable. I am actually quite interested in whether or not I am doing
> that!
>
> What I regard as nonnegotiable for a foundation of mathematics is that
> there be a "formalism" and that mathematical proofs are modeled as finite
> combinatorial objects - i.e., as certificates.
>
> This amounts, in practice, to spelling out up front just what "substantive
> assumptions" one is making. Yes, there is an issue of where logic stops and
> substantive issues start. But I am still adhering to the idea of
> "certificates".
>
> So if you make a case that "logic" whatever that is, is "open ended", I
> will say that if you act on this open endedness to periodically argue for
> new logical principles, then that is unsatisfactory as a foundation for
> mathematics.
>
> So the very fact that there is some completeness theorem lying around is at
> least very refreshing, since it says that you are not going to be acting on
> any open endedness.
>
> But I can at least imagine that we all agree that we won't act on any
> possible open endedness, and not have a completeness theorem, but still
> claim empirically and otherwise that we have put a large umbrella over
> mathematics.
>
> CAUTION: I have another life where I try to destroy current f.o.m. through
> 45 years of intense revolutionary activity (smile).
>
> Harvey Friedman
> -------------- next part --------------
> An HTML attachment was scrubbed...
> URL: </pipermail/fom/attachments/20130911/de8707d3/attachment-0001.html>
>
> ------------------------------
>
> Message: 3
> Date: Wed, 11 Sep 2013 11:17:01 -0400
> From: Colin McLarty <colin.mclarty at case.edu>
> To: rgheck <rgheck at brown.edu>, Foundations of Mathematics
> <fom at cs.nyu.edu>
> Subject: Re: [FOM] What is second order ZFC?
> Message-ID:
> <CAOzx82qrKKTWKoRSwa2_uUbqxq9_eXGoLt_1DfNkiDaUzJLsmA at mail.gmail.com>
> Content-Type: text/plain; charset="iso-8859-1"
>
> On Tue, Sep 10, 2013 at 10:03 PM, Richard Heck
> <richard_heck at brown.edu> responded
> to Harvey's challenge to say what is second order ZFC, but did not so much
> give an answer as indicate that there are several.
>
> Second-order ZFC is the theory, formulated in a second-order language,
> > whose axioms are the second-order versions of the axioms of first-order
> > ZFC. Its theorems are the second-order consequences of those axioms. The
> > problem is now to explain "second-order consequence".....
> >
> > I take it that the point of raising the question as one about ZFC
> > specifically is that one typically talks about sets when trying to explain
> > what the second-order quantifiers are supposed to mean. But if that is the
> > problem, then it is a very old one, and one to which various responses have
> > been available for some time now.
>
>
> Yes, precisely. There have been various responses around for a very long
> time, because none of them can inspire a consensus. And this is not a
> quibble. It is the whole point of Harvey saying
>
> HF> For any of the usual classical foundational purposes, you need to be
> able
> HF> to get down to finite representations that are completely non
> problematic....
> HF>
> HF> Furthermore, first order logic is apparently the unique vehicle for such
> HF> foundational purposes. (I'm not talking about arbitrary interesting
> HF> foundational purposes).
>
> These various versions have been prominently problematic throughout their
> existence. And one common problem has been to tell whether a given version
> can produce finite representations of proofs or not. That problem
> is highlighted by Richard's answer to Harvey's specific question
>
>
> > HF> 4. Is CH a "theorem of second order ZFC"? [corrected]
> >
> > I don't know. Second-order consequence is very hard to decide.
> >
>
> I think this answer is imprecise. For example, it is not hard to decide CH
> by the ZF axioms -- it is provably impossible. Some definitions of second
> order consequence explicitly rest on ZF, so that deciding second order
> consequence is not hard, but provably impossible on these definitions.
>
> I do not know the issues of decidability for plural quantification. Is
> there a standard theory of that? Frege's option, invoked by Richard,
> of regarding
> second-order quantifiers as quantifying over what Frege called "concepts"
> offers no serious prospect of decidability.
>
> And towards the end of his post Richard offers the following as if it
> disagreed with Harvey:
>
> Nonetheless, there are lots of ways in which logic can be used in the study
> > of mathematics, mind, and world, and one should not confuse unsuitability
> > for one's own purposes with unsuitability tout court. Solipsism, after all,
> > is false.
> >
>
> But Harvey had already said what I quote from him above: "I'm not talking
> about arbitrary interesting foundational purposes." And he is obviously
> not talking about other non-foundational purposes. This is not a point of
> disagreement. Taking it to be a disagreement may be one source
> of confusion in this discussion.
>
> Colin
>
>
>
>
>
> > Richard Heck
> >
> > =====
> >
> > References:
> >
> > @ARTICLE{Boolos:ToBeJPhil,
> > author = {George Boolos},
> > title = {To Be Is To Be a Value of a Variable (Or Some Values of Some
> > Variables)},
> > journal = {Journal of Philosophy},
> > year = {1984},
> > volume = {81},
> > pages = {430--49}
> > }
> >
> > @ARTICLE{RayoUzq:SecondOrder,
> > author = {Agust\'in Rayo and Gabriel Uzquiano},
> > title = {Toward a Theory of Second-Order Consequence},
> > journal = {Notre Dame Journal of Formal Logic},
> > year = {1999},
> > volume = {40},
> > pages = {315--25}
> > }
> >
> > @ARTICLE{McGee:Learn,
> > author = {Vann McGee},
> > title = {How We Learn Mathematical Language},
> > journal = {Philosophical Review},
> > year = {1997},
> > volume = {106},
> > pages = {35--68}
> > }
> >
> > @ARTICLE{Feferman:Unfolding,
> > author = {Solomon Feferman and Thomas Strahm},
> > title = {The Unfolding of Non-finitist Arithmetic},
> > journal = {Annals of Pure and Applied Logic},
> > year = {2000},
> > volume = {104},
> > pages = {75--96},
> > owner = {rgheck},
> > timestamp = {2009.03.24}
> > }
> >
> > @INCOLLECTION{Heck:LFTFT,
> > author = {Richard G. Heck},
> > title = {A Logic for {F}rege's {T}heorem},
> > pages = {267--96},
> > address = {Oxford},
> > publisher = {Clarendon Press},
> > year = {2011},
> > booktitle = {Frege's Theorem}
> > }
> >
> > @INCOLLECTION{HeckMay:**FuncUnsat,
> > author = {Richard G. Heck and Robert May},
> > title = {The Function is Unsaturated},
> > pages = {825--50},
> > address = {Oxford},
> > publisher = {Oxford University Press},
> > year = {2013},
> > editor = {Michael Beaney},
> > booktitle = {The Oxford Handbook of the History of Analytic Philosophy}
> > }
> >
> > @ARTICLE{Koellner:SecondOrder,
> > author = {Peter Koellner},
> > title = {Strong Logics of First and Second Order},
> > journal = {Bulletin of Symbolic Logic},
> > year = {2010},
> > volume = {16},
> > pages = {1--36}
> > }
> >
> > --
> > -----------------------
> > Richard G Heck Jr
> > Romeo Elton Professor of Natural Theology
> > Brown University
> >
> > Website: http://rgheck.frege.org/
> > Blog: http://rgheck.blogspot.com/
> > Amazon: http://amazon.com/author/**richardgheckjr<http://amazon.com/author/richardgheckjr>
> > Google+: https://plus.google.com/**108873188908195388170<https://plus.google.com/108873188908195388170>
> > Facebook: https://www.facebook.com/**rgheck<https://www.facebook.com/rgheck>
> >
> > Check out my books "Reading Frege's Grundgesetze"
> > http://tinyurl.com/**ReadingFregesGrundgesetze<http://tinyurl.com/ReadingFregesGrundgesetze>
> > and "Frege's Theorem":
> > http://tinyurl.com/**FregesTheorem <http://tinyurl.com/FregesTheorem>
> > or my Amazon author page:
> > amazon.com/author/**richardgheckjr<http://amazon.com/author/richardgheckjr>
> >
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
More information about the FOM
mailing list