[FOM] SOL vs. ZFC

Joe Shipman JoeShipman at aol.com
Fri Jun 7 22:53:30 EDT 2013


The reason I am sympathetic to Logicism is that it derives most of mathematics without specifically mathematical axioms, and thereby avoids having to justify axioms and allows mathematical propositions to be "true" in the strongest sense. The axioms for second-order logic developed by Hilbert may fairly be called "logical" rather than "mathematical".

That FOL has some nice properties that SOL lacks doesn't mean SOL isn't logic, it just means that we don't have an algorithm to enumerate logical truths (or "validities" if you don't like using the word truth, but expressing a mathematical proposition as a validity of SOL can reasonably be described as "proving it true"). Since SOL includes FOL, preferring FOL because of its convenient metamathematical properties is like preferring Presburger Arithmetic to Peano Arithmetic because it's a complete theory rather than an undecidable one--fine as a matter of taste, but no reason to discourage people from working in the larger system.

As a foundation for "ordinary mathematics", SOL works just fine, even if logicians and foundational specialists and set theorists have professional reasons for preferring to found mathematics in ZFC+FOL. I'm willing to accept that propositions like Con(Z) cannot be proven from SOL and that the best SOL can do is to prove "V_(omega+omega) models Z", because I'm not demanding that all mathematics be derived from logic, just as much as possible, with those parts being granted greater epistemic certainty.

And I am tired of hearing criticism of SOL as merely "sneaking in set theory in disguise". SOL isn't claiming to answer all mathematical questions that can be asked. That fans of ZFC can't settle the Continuum Hypothesis from their axioms doesn't justify the claim that CH is meaningless because the concept of "arbitrary subset of the natural numbers" is vague. The standard semantics of SOL refers to "all" subsets, and the existence of models which don't include all the subsets doesn't mean that MY concept of "all subsets" is incoherent or vague.

Really, it's a little bit insulting to be told that I shouldn't use SOL to formalize results which can be formalized in SOL because other mathematicians who don't use SOL can't decide what's true about sets.  They can say "we can't agree with each other about CH" but not "and therefore CH has no truth value". I don't know if it's true or false, but I know what it says and what it means.

From a Hilbert-style deductive calculus for SOL, I can prove pretty much anything that follows from the theory of types, which covers almost everything done in mainstream mathematics.

I still don't know whether the critics of SOL are denying that it is powerful enough to get this far, accepting that but criticizing it for being too weak to get further, or saying that it is too strong and proves things that aren't true. Maybe these three groups should argue with each other rather than me, since the criticisms are incompatible.

-- JS

Sent from my iPhone

On Jun 6, 2013, at 10:20 PM, Dustin Wehr <wehr at cs.toronto.edu> wrote:

Tim, Joe,
I think it's a semantic debate, but not a pointless one. Not to
suggest that you think otherwise.
Using my own position as an example: I want the default, most-common
meaning of "formal logic" to be classical FOL, for a number of
disputable, mostly pragmatic and social reasons*, which have probably
been expressed on this forum many times. Logicism, if my limited
understanding of the term is correct, is incompatible with that
position. And so I must disagree with the logicist on the weight of
those reasons, which seems like an interesting, if hairy,
disagreement, making the debate far from pointless (provided, of
course, that the debaters are willing to be logical...).

Dustin

* e.g.
--I don't want outsiders, especially non-mathematicians, to have the
impression that there is poor consensus about what constitutes formal
logic amongst people who are familiar with it (not an argument for
classical FOL specifically, but for a fixed default meaning of "formal
logic").
--I want to be able to explain, to smart people without much
background in math, things like the notion of
truth-with-respect-to-an-interpretation, and how formal logic makes as
much sense for reasoning about objects in the "real world" as it does
for reasoning about typical mathematical objects. For me currently,
those considerations somewhat preclude my adopting intuitionistic FOL.
Meanwhile, by rejecting Logicism, it seems I am giving up nothing in
my ability to discuss and reason about truth with respect to specific
or incompletely-defined structures. To be clear, those previous two
reasons are not enough to make a good case against Logicism; I simply
thought it would be odd for me to be completely vague about what I
meant by "pragmatic and social reasons".


On Thu, Jun 6, 2013 at 6:57 PM,  <fom-request at cs.nyu.edu> wrote:
> Send FOM mailing list submissions to
>        fom at cs.nyu.edu
> 
> To subscribe or unsubscribe via the World Wide Web, visit
>        http://www.cs.nyu.edu/mailman/listinfo/fom
> or, via email, send a message with subject or body 'help' to
>        fom-request at cs.nyu.edu
> 
> You can reach the person managing the list at
>        fom-owner at cs.nyu.edu
> 
> When replying, please edit your Subject line so it is more specific
> than "Re: Contents of FOM digest..."
> 
> 
> Today's Topics:
> 
>   1. Re: SOL vs. ZFC (Joe Shipman)
>   2. Re: Psychological basis of Intuitionism (Colin McLarty)
>   3. Re: SOL vs. ZFC (Jos? Ferreir?s Dom?nguez)
>   4. Proof Theory in Lisbon (Fernando Ferreira)
>   5. Re: SOL vs. ZFC (Timothy Y. Chow)
>   6. Call for Expression of Interest - WWTF Vienna Research Groups
>      for Young Investigators (Thomas Krennwallner)
>   7. Re: Psychological basis of Intuitionism (sambin at math.unipd.it)
> 
> 
> ----------------------------------------------------------------------
> 
> Message: 1
> Date: Wed, 5 Jun 2013 22:21:15 -0400
> From: Joe Shipman <JoeShipman at aol.com>
> To: "tchow at alum.mit.edu" <tchow at alum.mit.edu>,  Foundations of
>        Mathematics <fom at cs.nyu.edu>
> Cc: "fom at cs.nyu.edu" <fom at cs.nyu.edu>
> Subject: Re: [FOM] SOL vs. ZFC
> Message-ID: <D666F19F-0BD9-4ED7-9EC9-8BBE9F544808 at aol.com>
> Content-Type: text/plain;       charset=us-ascii
> 
> It's not a pointless semantic debate if we care about which statements of arithmetic are "true". SOL will not only guarantee the meaningfulness of statements of arithmetic, it will recognize a distinction between Con(PA) which is a consequence of logical validities and can be thought of as unqualifiedly "true", and Con(Z) which is a consequence of set existence axioms that are not part of "logic".
> 
> The question of "justifying the axioms" then goes away for most math because logic comes "for free". Although SOL makes no ontological commitments, that is not necessary when you can characterize a mathematical object up to isomorphism by a single sentence.
> 
> -- JS
> 
> Sent from my iPhone
> 
> On Jun 4, 2013, at 5:07 PM, "Timothy Y. Chow" <tchow at alum.mit.edu> wrote:
> 
> Joe Shipman wrote:
> 
>> I am motivated by the question "how much of mathematics is logic in disguise?". If second order logic in the standard formalism is really "logic", then logic can express almost all of the mathematics anyone cares about, and the question reduces to which axioms can plausibly be described as "logical".
> [...]
>> but Logicism gets pretty far and I wonder why it seems to be unpopular.
> 
> A large part of the answer is historical.  The original efforts to carry out the logicist program (e.g., by Dedekind and Frege) ran into difficulties because of the paradoxes.  Hilbert also didn't like logicism. It doesn't take much to make a philosophy unpopular.
> 
> One could ask why more people haven't tried to revive logicism.  I think part of the answer is that many people see it as a somewhat pointless semantic debate, over what you consider to be "logic."
> 
> I imagine that only a minority of FOM readers take Alain Badiou seriously, but for those who do, I'll remark that the only way I've been able to make sense of Badiou's philosophy is to hypothesize that he regards much of set theory as "logic" and that since logic applies universally, we should expect set-theoretic concepts such as forcing extensions to show up in the real world, and not just in mathematics papers.  So I personally think of Badiou as a kind of logicist, though I doubt he would describe himself in those terms.
> 
> Tim
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
> 
> 
> ------------------------------
> 
> Message: 2
> Date: Thu, 6 Jun 2013 00:11:01 -0400
> From: Colin McLarty <colin.mclarty at case.edu>
> To: Foundations of Mathematics <fom at cs.nyu.edu>
> Subject: Re: [FOM] Psychological basis of Intuitionism
> Message-ID:
>        <CAOzx82okU-rEKGcZx-S_aoo6AkO5A5_dOY74rSoeHsq6VmyjMQ at mail.gmail.com>
> Content-Type: text/plain; charset="iso-8859-1"
> 
> Steve,
> 
> I am not sure exactly what you mean by the question.  But could you answer
> your question by reading the 18th century mathematicians who actually did
> it?
> 
> best, Colin
> 
> On Wed, Jun 5, 2013 at 10:42 AM, Steve Stevenson <steve at clemson.edu> wrote:
> 
>> On Tue, Jun 4, 2013 at 9:41 AM, Andrej Bauer <andrej.bauer at andrej.com>
>> wrote:
>>> If mathematics is the art of hypothetical reasoning, surely then we must
>>> develop mathematics which is open to all possibilities, including the
>> one in
>>> which mathematics has an independent and objective nature, and moreover
>>> allows for existence without construction.
>> 
>> I am asking a different question. Suppose you're an 18th Century
>> geometer and want to develop a non-Euclidean geometry. Since there are
>> no known such, how do you think about reformulating the parallel line
>> axiom? Once you've put a theory together, how do you communicate this
>> insight without show your colleagues how to construct such a geometry?
>> 
>> --
>> D. E. (Steve) Stevenson, PhD
>> Emeritus Associate Professor
>> School of Computing, Clemson University
>> 
>> "Those that know, do. Those that understand, teach," Aristotle.
>> _______________________________________________
>> FOM mailing list
>> FOM at cs.nyu.edu
>> http://www.cs.nyu.edu/mailman/listinfo/fom
> -------------- next part --------------
> An HTML attachment was scrubbed...
> URL: </pipermail/fom/attachments/20130606/bf4b6194/attachment-0001.html>
> 
> ------------------------------
> 
> Message: 3
> Date: Thu, 6 Jun 2013 09:33:50 +0200
> From: Jos? Ferreir?s Dom?nguez <josef at us.es>
> To: fom at cs.nyu.edu
> Subject: Re: [FOM] SOL vs. ZFC
> Message-ID: <C571F022-0A76-4296-B624-78D6CE3DDB21 at us.es>
> Content-Type: text/plain; charset=us-ascii
> 
> Let me add something: when I wrote, "The standard semantics of SOL must be Henkin semantics", that was an oversimplification. Proof theorists have long been employing SOL in ways that are perfectly Ok, as far as I can see, but different from Henkin's. The key is just the rejection of any special status to "full" semantics, plus the arguments why this goes too far from logic.
> 
> Again, there's no problem in working with hybrid systems. But the realization that SOL set-theoretically interpreted can support quite a lot of mathematics is no insight into logic and its connections with mathematics.
> 
> Best, Jose
> 
> Prof. Jose Ferreiros
> Departamento de Filosofia y Logica
> Universidad de Sevilla
> http://personal.us.es/josef/
> 
> 
> 
> 
> 
> 
> ------------------------------
> 
> Message: 4
> Date: Thu, 6 Jun 2013 09:50:12 +0100
> From: Fernando Ferreira <ferferr at cii.fc.ul.pt>
> To: Foundations of Mathematics <fom at cs.nyu.edu>
> Subject: [FOM] Proof Theory in Lisbon
> Message-ID: <7B8EF147-3947-4AA1-A1FC-E69298D3F9F5 at cii.fc.ul.pt>
> Content-Type: text/plain; charset="iso-8859-1"
> 
> SECOND ANNOUNCEMENT
> 
> Proof Theory in Lisbon: a one-day workshop
> 
> Just before the Logic Colloquium 2013 (?vora, Portugal) there will be a one-day workshop in Proof Theory in Lisbon. The main event of the workhop is a three-part lecture by Jean-Louis Krivine on his classical realizability of set theory, with new proofs of relative consistency results. Please have a look at
> 
> http://www.ciul.ul.pt/~ferferr/ProofTheoryinLisbon.htm
> 
> for information. The workshop includes the following participants: Jean-Louis Krivine, Ulrich Kohlenbach, Fernando Ferreira, Jaime Gaspar, Ali Enayat, Benno ven den Berg, Gilda Ferreira, Daniel Durante and Alexander Kreuzer.
> 
> Fernando Ferreira and Jaime Gaspar
> 
> 
> 
> Fernando Ferreira
> Departamento de Matem?tica
> Faculdade de Ci?ncias
> Universidade de Lisboa
> Campo Grande, Edif?cio C6, Gabinete 6.2.8
> P-1749-016 Lisboa
> Portugal
> 
> http://www.ciul.ul.pt/~ferferr/
> 
> 
> 
> 
> 
> ------------------------------
> 
> Message: 5
> Date: Thu, 6 Jun 2013 13:49:57 -0400 (EDT)
> From: "Timothy Y. Chow" <tchow at alum.mit.edu>
> To: Foundations of Mathematics <fom at cs.nyu.edu>
> Subject: Re: [FOM] SOL vs. ZFC
> Message-ID: <alpine.LFD.2.03.1306061343070.17050 at alum.mit.edu>
> Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed
> 
> On Wed, 5 Jun 2013, Joe Shipman wrote:
>> It's not a pointless semantic debate if we care about which statements
>> of arithmetic are "true". SOL will not only guarantee the meaningfulness
>> of statements of arithmetic, it will recognize a distinction between
>> Con(PA) which is a consequence of logical validities and can be thought
>> of as unqualifiedly "true", and Con(Z) which is a consequence of set
>> existence axioms that are not part of "logic".
>> 
>> The question of "justifying the axioms" then goes away for most math
>> because logic comes "for free".
> 
> It's hard for me to imagine that this line of argumentation---i.e., X is
> true because X is logic and logic is true---would convince many people
> today when it comes to, say, X = Con(PA).  There's such a widespread
> feeling that logical truth is what you get by syntactic manipulation that
> you'd be fighting an uphill battle to convince people that Con(PA) is
> logically true.
> 
> Tim
> 
> 
> ------------------------------
> 
> Message: 6
> Date: Thu, 6 Jun 2013 21:44:05 +0200
> From: Thomas Krennwallner <tkren at kr.tuwien.ac.at>
> Subject: [FOM] Call for Expression of Interest - WWTF Vienna Research
>        Groups  for Young Investigators
> Message-ID: <B38BDA9A-5650-4A00-BEEA-CFA9BEDFF32E at kr.tuwien.ac.at>
> Content-Type: text/plain; charset=us-ascii
> 
> [Apologies for cross-posting]
> 
> WWTF Vienna Research Groups for Young Investigators
> Call 2013 - Cognitive Sciences
> 
> Call for Expressions of Interest
> ---------------------------------
> 
> The Faculty of Informatics at the Vienna University of Technology is
> looking for outstanding young researchers from abroad to set up and
> manage an independent research group as part of the Vienna Science and
> Technology Fund's (WWTF) VRGYI Call 2013 - Cognitive Sciences.
> 
> Applications are sought from researchers who have recently completed
> their PhD (2-8 years ago) with an excellent research track
> record. Selected candidates will, together with an experienced
> researcher of the Faculty of Informatics as a proponent, prepare a
> proposal to be submitted to the WWTF VRSYI Call 2013 - Cognitive
> Sciences. This call focuses on cognitive processes in humans, animals
> and/or machines.
> 
> Should this proposal be successful, the proposed project will be
> funded to the amount of 1.5 million EUR by the Vienna Science and
> Technology Fund (WWTF) for a period of 6 - 8 years. The Vienna
> University of Technology will also contribute to the funding of the
> project. During this time the successful candidate(s) will set up and
> manage his or her own research group as a group leader. He or she will
> receive a tenure-track position, which will be later transformed into
> a tenured position subject to a positive overall assessment, including
> - amongst other things - an interim evaluation of the project.
> 
> Application procedure:
> ----------------------
> 
> Applications should be sent to the responsible contact person
> (proponent) of the respective host lab, institute or group. The
> application should consist of
> 
> -   CV (including a list of publications)
> -   a brief outline of the intended research project
> 
> *** Deadline: June 15, 2013 ***
> 
> Unconventional research careers will also be taken into
> consideration. Female applicants are explicitly encouraged to apply.
> 
> Among the possible hosting groups of the Faculty of Informatics at the
> Vienna University of Technology is the Knowledge Based Systems Group
> (Institute of Information Systems), which has research expertise in
> Knowledge Representation and Reasoning, Computational Logic and
> Complexity, Declarative Problem Solving, Intelligent Agents, and
> Mobile Robots. Intended research projects need to be a synergetic fit
> with these topics and research competence of the group.
> 
> For more information, see
> 
> http://www.informatik.tuwien.ac.at/aktuelles/736
> http://www.wwtf.at/programmes/ci/index.php?lang=EN
> http://www.kr.tuwien.ac.at/research/index.html
> 
> Contact:
> 
> Prof. Gerald Steinhardt
> Dean of the Faculty of Informatics,
> Vienna University of Technology
> dekan at informatik.tuwien.ac.at
> phone: +43-1-58801-18001
> 
> Prof. Thomas Eiter
> Head of the Institute of Information Systems,
> Vienna University of Technology
> thomas.eiter at tuwien.ac.at
> phone: +43-1-58801-18460
> 
> 
> ------------------------------
> 
> Message: 7
> Date: Thu, 06 Jun 2013 22:05:34 +0200
> From: sambin at math.unipd.it
> To: Foundations of Mathematics <fom at cs.nyu.edu>, "Kreinovich, Vladik"
>        <vladik at utep.edu>
> Cc: sambin at math.unipd.it
> Subject: Re: [FOM] Psychological basis of Intuitionism
> Message-ID: <20130606220534.20327x83ncmmm3y8 at webmail.math.unipd.it>
> Content-Type: text/plain; charset=ISO-8859-1; DelSp="Yes";
>        format="flowed"
> 
> 
> @ Steve
> Since you used the word "intuitionism" in the title of a post in FOM,
> I understood that you meant intuitionism in the sense of FOM, that is,
> the foundational school started by L.E.J.Brouwer at the beginning of
> last century. After you spoke about "psychological mechanisms", it
> seems to me that a better title for your questions would have been:
> "Psychological basis of intuition". On this topic I have little to
> say. Except for the remark  that non-euclidean geometries started to
> be really accepted when somebody (Beltrami, Riemann) built models of
> them.
> 
> I am a declared intuitionist since over 30 years.  My psychological
> reasons are that I feel deeply uneasy with anything I "must" assume
> without experiencing it in some way.
> 
> @ Andrej
> About solipsism: If you read the two papers of mine mentioned in my
> previous post, you will see that the main distinction of my view from
> Brouwer's is precisely that I consider social communication as
> essential for the construction of any abstraction (this was only
> hinted in my first post). So it is the opposite of solipsism.
> 
> In the same time, however, I believe math should be something more
> than social hallucination. That would be really solipsism, although
> collective. In the second paper I mentioned this is made clear by
> insisting on the fact that mathematics is made of abstraction *and* of
> application.
> 
> About my minimalist approach: I like it because it shows how much you
> can do with so little assumptions. Moreover, minimalism in assumptions
> goes together with maximalism in conceptual distinctions. Again for
> the purpose of communication, I believe it is convenient to build a
> foundation which is compatible with as many other foundational
> attitudes as possible. This btw proves that I am ready to accept other
> attitudes.
> 
> Using my minimalist approach in an actual development of topology, new
> mathematical structures have emerged which were hidden under stronger
> assumptions. This I believe is at least 7 years ahead of times (as it
> happened with other novelties of mine), not just 2 steps.
> 
> About  independent and objective nature of mathematics: Andrej, all of
> us are free to believe what we prefer. This is a fact, and it's not up
> to me! But if you like to believe, as most mathematicians and
> philosophers of mathematics do, that mathematics has an "independent
> and objective nature" as you say, then in my opinion you should
> explain where this comes from, on which basis we can say this, or
> other equivalent questions. Since nobody has been able to give proper
> answers, such a belief does not seem to me a foundation, but just
> begging the question (of what a foundation of mathematics is). I
> myself find this assumption so strong, and unfounded, that I feel very
> uneasy when I meet it. That is why I prefer the minimalist approach. I
> feel better from that perspective, since I can give a rationale for
> the various foundational  assumptions.
> 
> @ Vladik
> It is not nice to charge a colleague of being dogmatic and old
> fashioned before reading the papers he suggests. Understanding your
> remarks as a question, my answer is that it all depends on what one
> means by construction. My version of constructivism is not scholastic.
> In my opinion, construction should not be limited to what is reducible
> to Turing  computability (which indeed would be dogmatic).
> 
> Best regards to all
> Giovanni
> 
> 
> 
> 
> ----------------------------------------------------------------
> This message was sent using IMP, the Internet Messaging Program.
> 
> 
> 
> 
> ------------------------------
> 
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
> 
> 
> End of FOM Digest, Vol 126, Issue 12
> ************************************
_______________________________________________
FOM mailing list
FOM at cs.nyu.edu
http://www.cs.nyu.edu/mailman/listinfo/fom


More information about the FOM mailing list