computationally bounded observers and non-constructive mathematics

[Vaughan Pratt]

Joseph Caballero wrote, " The non-constructive parts of mathematics may be a
useful way to formalize our computational boundeness."

Certainly.  But I see no need to go as far as the uncountable, which as we
know from Cohen is fuzzy and therefore unlikely to add more to our
knowledge of computational boundedness than what can be learned from the
less fuzzy parts of non-constructive mathematics.

Vaughan Pratt

On Thu, Feb 16, 2023 at 5:45 AM <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
>         https://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: Two Queries about Univalent Foundations (JOSEPH SHIPMAN)
>    2. computationally bounded observers and non-constructive
>       mathematics (Jos? Manuel Rodr?guez Caballero)
>    3. 29th WoLLIC 2023 - 3rd Call for Papers (DEADLINE APPROACHING)
>       (Ruy Jose Guerra Barretto de Queiroz)
>
>
> ----------------------------------------------------------------------
>
> Message: 1
> Date: Tue, 14 Feb 2023 13:40:57 -0800
> From: JOSEPH SHIPMAN <joeshipman at aol.com>
> To: tchow at alum.mit.edu
> Cc: FOM at cs.nyu.edu
> Subject: Re: Two Queries about Univalent Foundations
> Message-ID: <F9EE773D-FF93-4266-BE32-A9C4938C8FFA at aol.com>
> Content-Type: text/plain; charset=utf-8
>
> The point of my questions was to see if there was any reason I personally
> should make the effort to learn HoTT or some other flavor of ?univalent
> foundations?. I am not disputing that that system serves valuable purposes
> for other people!
>
> My first question was about logical strength, and my impression that it
> can?t give any more than ZFC plus Grothendieck universes was correct; ZFC
> plus Grothendieck universes seems to be the limit of what is ?publishable
> without remark?, and easily exceeds other mild strengthenings like MK, so I
> don?t have a reason along those lines to learn univalent foundations.
>
> My second question was specifically about whether Homotopy Type Theory has
> given any new INSIGHT into homotopy groups of spheres, where ?allows some
> to be computed that could not previously be computed? is a good proxy for
> ?new insight?. Independently of caring about foundations and logical
> strength, I care about homotopy groups of spheres for purely mathematical
> reasons!
>
> ? JS
>
> Sent from my iPhone
>
> > On Feb 14, 2023, at 11:52 AM, Timothy Y. Chow <tchow at math.princeton.edu>
> wrote:
> >
> > ?Joe Shipman wrote:
> >> I'm sorry, Kevin, but this seems to miss both of the points I was
> making.
> >
> > Technically, yes; but I think Kevin's point is that your questions, or
> at least the first question, somehow misses the point of univalent
> foundations.
> >
> > The second question is fairly straightforward, at least if interpreted
> literally.  UF does not (currently) lead to any faster algorithms for
> computing homotopy groups of spheres.  The way you might hope this would
> play out would be something like this: we take the simplicial set model as
> given, and then compute homotopy groups of spheres "purely synthetically."
> If you take this route, however, then you find that even computing the
> fundamental group is harder than it is classically.
> >
> > While it's not unreasonable to ask for faster algorithms as a benchmark
> for progress, it's not necessarily the only way, or even the best way, to
> understand whether a new theory is giving new insights about old objects.
> For example, does the Lebesgue integral give us faster algorithms for
> numerical integration?  Not that I know of, but in some sense that's not
> the only, or even the best, way of judging whether the Lebesgue integral is
> buying us anything.
> >
> > Your first question, if I understand it correctly, has sort of a boring
> answer.  To begin with, as Kevin said, there isn't a unique UF, because
> there are some optional axioms.  If you limit excluded middle and choice
> then what you get is essentially a subset of classical mathematics.  On the
> other hand, I believe that by strengthening the axioms a bit you get
> something like ZFC + inaccessibles, which then trivially proves something
> not provable in ZFC, namely "ZFC is consistent."  Some of these points are
> elucidated in more detail in this blog post by Andrej Bauer.
> >
> >
> https://math.andrej.com/2014/01/13/univalent-foundations-subsume-classical-mathematics/
> >
> > But again, logical strength is not necessarily the right metric by which
> to judge a new foundation.  Is there any theorem of classical algebraic
> geometry provable using schemes that is unprovable without them?  No.  But
> that's an irrelevant question when it comes to assessing whether schemes
> represent a conceptual advance.
> >
> > In short, I think at the answer to these high-level questions is
> basically the same as they were back in October 2014, when you asked the
> same questions here on FOM.  If you want an example of something people
> wanted to prove before HoTT was around and whose proof was made easier by
> HoTT, then Blakers-Massey still fits the bill.  If you want to know whether
> HoTT or UF is a superior foundation for all of mathematics, as some of its
> enthusiasts claim, then the jury is still out.  Even Jacob Lurie has
> expressed measured skepticism about whether HoTT helps him answer the
> homotopy-theoretic questions that he's interested in.  Outside of algebraic
> topology and algebraic geometry and the world of proof assistants, HoTT has
> not had much impact.
> >
> > Tim
>
>
>
> ------------------------------
>
> Message: 2
> Date: Tue, 14 Feb 2023 20:07:21 -0500
> From: Jos? Manuel Rodr?guez Caballero  <josephcmac at gmail.com>
> To: Foundations of Mathematics <fom at cs.nyu.edu>
> Subject: computationally bounded observers and non-constructive
>         mathematics
> Message-ID:
>         <
> CAA8xVUh_Udh6EzgJe1UgZaiDcTCLmf7mUg7yHq6673bh5PENAA at mail.gmail.com>
> Content-Type: text/plain; charset="utf-8"
>
> Vaughan Pratt wrote:
>
> >  Martin Dowd wrote, "A line segment in 3-dimensional Euclidean space
> > has uncountably many points."
>
> Since no one else has challenged Martin's statement, let me do so here.
>
> [...]
>
> > When your only tools are a straightedge and compass, you don't need
> > anything more than the constructible points, aka real algebraic
> > geometry with only linear and quadratic polynomials.  And if you
> > insist on Euclidean space being topologically complete,  then
> > furthermore you need the limits of sequences of contructible points
> > when those limits exist.
>
> [...]
>
> > When your tools include a smartphone or other computer, you need at
> > most the computable points, and its completion via computable
> > sequences (more constrained than general Cauchy sequences) is likewise
> > countable.
>
>
> Assume the worst-case for the real numbers, that is, that the universe as a
> whole is a computation (physical Church-Turing thesis, due to David Deutsch
> [1] and Stephen Wolfram [2]). I will borrow from Stephen Wolfram the notion
> of the computationally bounded observer that he uses to conceptualize the
> second law of thermodynamics [3].
>
> Let us consider a scientifically relevant mathematical model: the
> continuous-time Markov process that describes births and deaths [4].
> According to the physical Church-Turing thesis, all births and deaths in
> nature are computational processes. Hence, the most realistic model would
> be algorithmic. But, in practice, we can not access the actual algorithm
> because of our computational boundedness. What we do instead is transfer
> our epistemic limitations into ontological idealizations.
>
> Of course, there are constructive versions of probability theory [5]. But
> why should we insist on the construction of all mathematical objects in
> models where the point is precisely that we don't know how to construct the
> phenomenon under study? The non-constructive parts of mathematics may be a
> useful way to formalize our computational boundeness.
>
> Kind regards,
> Jos? M.
>
> References:
> [1] Deutsch, David. "Quantum theory, the Church?Turing principle and the
> universal quantum computer." Proceedings of the Royal Society of London. A.
> Mathematical and Physical Sciences 400.1818 (1985): 97-117.
> [2] Wolfram, Stephen. "Undecidability and intractability in theoretical
> physics." Physical Review Letters 54.8 (1985): 735.
> [3] Computational Foundations for the Second Law of Thermodynamics, Stephen
> Wolfram's Writings, URL:
>
> https://writings.stephenwolfram.com/2023/02/computational-foundations-for-the-second-law-of-thermodynamics/
> [4] Chazottes, J-R., P. Collet, and S. M?l?ard. "Sharp asymptotics for the
> quasi-stationary distribution of birth-and-death processes." Probability
> Theory and Related Fields 164.1-2 (2016): 285-332.
> [5] Chan, Yuen-Kwok. *Foundations of Constructive Probability Theory*. Vol.
> 177. Cambridge University Press, 2021.
> -------------- next part --------------
> An HTML attachment was scrubbed...
> URL: </pipermail/fom/attachments/20230214/07d62510/attachment-0001.html>
>
> ------------------------------
>
> Message: 3
> Date: Thu, 16 Feb 2023 09:30:35 -0300
> From: Ruy Jose Guerra Barretto de Queiroz <ruy at cin.ufpe.br>
> To: Evento WOLLIC <wollic at cin.ufpe.br>
> Subject: 29th WoLLIC 2023 - 3rd Call for Papers (DEADLINE APPROACHING)
> Message-ID:
>         <
> CANSQ7Qhx-3-MRoMuYzbfG8fmtO9Oy78FogCzY9PzKR4O+YZPSw at mail.gmail.com>
> Content-Type: text/plain; charset="utf-8"
>
> DEADLINE APPROACHING
>
> [Please distribute. Apologies for multiple postings]
>
> CALL FOR PAPERS
>
> WoLLIC 2023
> 29th Workshop on Logic, Language, Information and Computation
> 11-14 July, 2023
> Halifax, Nova Scotia, Canada
> Website: https://www.mathstat.dal.ca/wollic2023/
>
> ORGANISATION
> Department of Mathematics and Statistics, Dalhousie University, Canada
> Centro de Inform?tica, Universidade Federal de Pernambuco, Brazil
>
> CALL FOR PAPERS
> WoLLIC is an annual international forum on inter-disciplinary research
> involving formal logic, computing and programming theory, and natural
> language and reasoning. Each meeting includes invited talks and tutorials
> as well as contributed papers. The twenty-ninth WoLLIC will be held at the
> Department of Mathematics and Statistics, Dalhousie University, Canada,
> 11-14 July, 2023.  It is scientifically sponsored by the Association for
> Symbolic Logic (ASL), the Interest Group in Pure and Applied Logics (IGPL),
> the Association for Logic, Language and Information (FoLLI), the European
> Association for Theoretical Computer Science (EATCS) (tbc), European
> Association for Computer Science Logic (EACSL), and the Sociedade
> Brasileira de L?gica (SBL).
>
> LOCATION AND FORMAT
> Halifax (https://www.halifax.ca/) is the capital and largest municipality
> of the Canadian province of Nova Scotia, and the largest municipality in
> Atlantic Canada. (Wikipedia)
> WoLLIC 2023 will be a hybrid event. All invited talks are planned to be
> on-site in order to stimulate discussions and interaction with
> participants.
>
> SCOPE
> Contributions are invited on all pertinent subjects, with particular
> interest in cross-disciplinary topics. Typical but not exclusive areas of
> interest are: foundations of computing, programming and Artificial
> Intelligence (AI); novel computation models and paradigms; broad notions of
> proof and belief; proof mining, type theory, effective learnability and
> explainable AI; formal methods in software and hardware development;
> logical approach to natural language and reasoning; logics of programs,
> actions and resources; foundational aspects of information organization,
> search, flow, sharing, and protection; foundations of mathematics;
> philosophical logic; philosophy of language.
>
> PAPER SUBMISSION
> Proposed contributions should be in English, and consist of a scholarly
> exposition accessible to the non-specialist, including motivation,
> background, and comparison with related works. Articles should be written
> in the LaTeX format of LNCS by Springer (see author's instructions at
> http://www.springer.com/computer/lncs?SGWID=0-164-6-793341-0). They must
> not exceed 12 pages, with up to 5 additional pages for references and
> technical appendices. The paper's main results must not be published or
> submitted for publication in refereed venues, including journals and other
> scientific meetings.
> It is expected that each accepted paper be presented at the meeting by one
> of its authors either in person or via remote connection. (At least one
> author is required to pay a full on-site registration fee before granting
> that the paper will be published in the proceedings.)
> Papers must be submitted electronically at the WoLLIC 2023 EasyChair
> website https://easychair.org/conferences/?conf=wollic2023.
>
> PROCEEDINGS
> The proceedings of WoLLIC 2023, including both invited and contributed
> papers, will be published as a volume in Springer's LNCS series. Due to the
> earlier timeline this year, the proceedings will appear after the workshop.
> In addition, abstracts will be published in the Conference Report section
> of the Logic Journal of the IGPL, and selected contributions will be
> published (after a new round of reviewing) as a special post-conference
> WoLLIC 2023 issue of a scientific journal (to be confirmed).
>
> INVITED SPEAKERS
> Thomas Bolander (Technical University of Denmark)
> Makoto Kanazawa (Hosei University, Japan)
> Magdalena Ortiz (University of Ume?, Sweden)
> Ayb?ke ?zg?n (University of Amsterdam, Netherlands)
> Dusko Pavlovic (University of Hawaii, USA)
> Richard Zach (University of Calgary, Canada)
>
> IMPORTANT DATES
> February 20, 2023: Abstract deadline
> February 27, 2023: Full paper deadline
> May 15, 2023: Author notification
> June 5, 2023: Final version deadline
>
> PROGRAMME COMMITTEE
> Bahareh Afshari (University of Gothenburg, Sweden and University of
> Amsterdam, Netherlands)
> Zena Ariola (University of Oregon, USA)
> Adriana Balan (University Politechnica of Bucharest, Romania)
> Marta B?lkov? (Czech Academy of Sciences, Czech Republic)
> Jos?e Desharnais (Laval University, Canada)
> David Fern?ndez-Duque (Czech Academy of Sciences, Czech Republic)
> Santiago Figueira, Universidad de Buenos Aires, Argentina
> Silvia Ghilezan (University of Novi Sad & Mathematical Institute SASA,
> Serbia)
> Sujata Ghosh (Indian Statistical Institute, India)
> Nina Gierasimczuk (Danish Technical University, Denmark)
> Helle Hvid Hansen (University of Groningen, Netherlands) (co-chair)
> Andreas Herzig (CNRS, University of Toulouse, France)
> Juha Kontinen (University of Helsinki, Finland)
> Roman Kuznets (TU Wien, Austria)
> Martha Lewis (University of Bristol, UK)
> Johannes Marti (University of Oxford, UK)
> George Metcalfe (University of Bern, Switzerland)
> Michael Moortgat (Utrecht University, Netherlands)
> Cl?udia Nalon (University of Brasilia, Brasil)
> Carlos Olarte (Universit? Sorbonne Paris Nord, France)
> Sophie Pinchinat (University of Rennes, France)
> Francesca Poggiolesi (CNRS, University Paris 1 Panth?on-Sorbonne, France)
> Sylvain Pogodalla (INRIA Nancy, France)
> Revantha Ramanayake (University of Groningen, Netherlands)
> Mehrnoosh Sadrzadeh, University College London, UK
> Andre Scedrov (University of Pennsylvania, USA) (co-chair)
> Philip Scott (University of Ottawa, Canada)
> Viorica Sofronie-Stokkermans (University of Koblenz-Landau, Germany)
> Kazushige Terui (Kyoto University, Japan)
> Mladen Vukovi? (University of Zagreb, Croatia)
>
> STEERING COMMITTEE
> Samson Abramsky, Anuj Dawar, Juliette Kennedy, Ulrich Kohlenbach, Daniel
> Leivant, Leonid Libkin, Lawrence Moss, Luke Ong, Valeria de Paiva, Ruy de
> Queiroz, Alexandra Silva, Renata Wassermann.
>
> ADVISORY COMMITTEE
> Johan van Benthem, Joe Halpern, Wilfrid Hodges, Angus Macintyre, Hiroakira
> Ono, Jouko V??n?nen.
>
> ORGANISING COMMITTEE
> Julien Ross  (Dalhousie University)
> Peter Selinger (Dalhousie University) (co-chair)
> Anjolina G. de Oliveira (Univ Federal de Pernambuco, Brasil)
> Ruy de Queiroz (Univ Federal de Pernambuco, Brasil) (co-chair)
>
> SCIENTIFIC SPONSORSHIP
> Interest Group in Pure and Applied Logics (IGPL)
> The Association for Logic, Language and Information (FoLLI)
> Association for Symbolic Logic (ASL) (tbc)
> European Association for Theoretical Computer Science (EATCS) (tbc)
> European Association for Computer Science Logic (EACSL)
> Sociedade Brasileira de L?gica (SBL)
>
> SPECIAL SESSION: SCREENING OF MOVIES ABOUT MATHEMATICIANS
> It is planned to have a special session with the exhibition of a
> documentary film which traces the history of the individuals who worked as
> pioneers in expanding the presence of African Americans in mathematics. "
> 'Journeys of Black Mathematicians' is a film that will inspire African
> American students to continue their studies and consider career paths in
> mathematics." (zalafilms.com) The film is in production, and the filmmaker
> George Csicsery is willing to present either a rough cut if it is ready by
> then, or some sample scenes.
>
> FURTHER INFORMATION
> Contact one of the Co-Chairs of the Organising Committee.
>
> WEB PAGE
> https://www.mathstat.dal.ca/wollic2023/
> -------------- next part --------------
> An HTML attachment was scrubbed...
> URL: </pipermail/fom/attachments/20230216/c8eb34b6/attachment.html>
>
> ------------------------------
>
> Subject: Digest Footer
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/fom
>
>
> ------------------------------
>
> End of FOM Digest, Vol 242, Issue 31
> ************************************
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20230216/99f71237/attachment-0001.html>