[FOM] What is Second-Order ZFC
Alan Weir
Alan.Weir at glasgow.ac.uk
Fri Sep 13 17:12:48 EDT 2013
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>
>
More information about the FOM
mailing list