Countable sums in ZF

[Paul Blain Levy]

On 12/08/2020 06:20, fom-request at cs.nyu.edu wrote:
>
> ------------------------------
>
> Message: 2
> Date: Mon, 10 Aug 2020 17:52:08 -0400 (EDT)
> From: "Timothy Y. Chow" <tchow at math.princeton.edu>
> To: fom at cs.nyu.edu
> Subject: Countable sums in ZF
> Message-ID: <alpine.LRH.2.21.2008101747480.30326 at math.princeton.edu>
> Content-Type: text/plain; format=flowed; charset=US-ASCII
>
> I was surprised to learn recently that the proof of "a positive
> real-valued function on [0,1] has a positive integral" requires countable
> choice (Kanovei and Katz, Real Analysis Exchange 42 (2017), 385-390).

Interesting!  Are there examples of theorems in analysis that are 
(sentences of second order arithmetic and) require Dependent Choice to 
prove, not merely Countable Choice?

Paul

>
> Years ago, on MathOverflow, the following theorem was cited as being
> trickier to prove than it looks: If I_1, I_2, ... are intervals of real
> numbers with lengths that sum to less than 1, then their union cannot be
> all of [0,1].  Is there anything interesting about this theorem from a
> reverse mathematics perspective?
>
> Tim
>
>
> ------------------------------
>
> Message: 3
> Date: Tue, 11 Aug 2020 13:41:22 +0300
> From: Jos? Manuel Rodr?guez Caballero  <josephcmac at gmail.com>
> To: Foundations of Mathematics <fom at cs.nyu.edu>
> Subject: A Candidate Geometrical Formalism for the Foundations of
> 	Mathematics
> Message-ID:
> 	<CAA8xVUiQQyipK-Zz_W7PfESoxvbJfkxxs_438DvSutu-RCfXWA at mail.gmail.com>
> Content-Type: text/plain; charset="utf-8"
>
> Dear FOM members,
>    I think that it will be interesting to know the opinion of mathematicians
> about the proposal of the Wolfram Model as a foundation of mathematics.
> Here is the reference
>
> https://www.wolframphysics.org/bulletins/2020/08/a-candidate-geometrical-formalism-for-the-foundations-of-mathematics-and-physics/
>
>
> and below there is the official abstract concerning this proposal:
>
>   The interplay between logic, metamathematics and the Wolfram model, with
> an emphasis on the relationship between homotopy type theory, (higher)
> topos theory, (higher) category theory and the discrete foundations of
> quantum mechanics and general relativity. Key results will include a new
> interpretation of type spaces and the incompleteness theorems in terms of
> multiway systems and their foliations, a new interpretation of rulial space
> in terms of fibrations of infinity-topoi, interpretations of quantum
> measurement in terms of higher homotopies and the univalence axiom, and the
> beginnings of a rigorous mathematical connection between the quantum
> mechanical properties of the Wolfram model and the categorical quantum
> mechanics framework developed by Coecke and Abramsky. We will also make
> some remarks of a more philosophical flavor regarding possible implications
> of the formal structure of the Wolfram model for the origins of the laws of
> both mathematics and physics.
>
> Best,
> Jose M.
> -------------- next part --------------
> An HTML attachment was scrubbed...
> URL: </pipermail/fom/attachments/20200811/77eb5970/attachment.html>
>
> ------------------------------
>
> Message: 4
> Date: Tue, 11 Aug 2020 11:54:00 +0000
> From: Kapantais Doukas <dkapa at Academyofathens.gr>
> To: Joe Shipman <joeshipman at aol.com>, Foundations of Mathematics
> 	<fom at cs.nyu.edu>
> Subject: RE: Logicism
> Message-ID:
> 	<VI1PR04MB45593E17DDA41326E2EA0133C4450 at VI1PR04MB4559.eurprd04.prod.outlook.com>
> 	
> Content-Type: text/plain; charset="utf-8"
>
> Concerning Joe Shipman's post on "logical"/"mathematical".
>
> I might be misinterpreting something in the question, and if so I apologize, but would the system of Principia Mathematica not be a good candidate? See, for example, systems PM and P in Godel's incompleteness proofs. System P is in fact a simplification. We just add the Peano Axioms to the logic of the Principia (system PM). But as Godel notes (n. 16): "The addition of the Peano Axioms as well as all other modifications introduced in the system PM, merely serves to simplify the proof and is dispensable in principle".
> If PM is a logical system, then some interpretation of some of its "logical" truths are theorems of Peano Arithmetic. At least, this is what note 16 above suggests.
>
> Doukas Kapantais
> RCGP
> Academy of Athens
>
>
> -----Original Message-----
> From: FOM <fom-bounces at cs.nyu.edu> On Behalf Of Joe Shipman
> Sent: Monday, August 10, 2020 7:19 AM
> To: Foundations of Mathematics <fom at cs.nyu.edu>
> Subject: Logicism
>
> There seems to be agreement that some mathematical propositions can be shown to be equivalent to truths of logic, and others can?t, but drawing a line between what is ?logical? and what is ?mathematical? is hard.
>
> I?ve had trouble finding a simple, streamlined development of BASIC logicism. Can anyone provide a source for a presentation of a logical system (by which I mean, at the very least, a computable deductive calculus that generates truths of logic) , and an interpretation of theorems of Peano Arithmetic as logical truths in this system?
>
> ? JS
>
> Sent from my iPhone
>
> ------------------------------
>
> Subject: Digest Footer
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/fom
>
>
> ------------------------------
>
> End of FOM Digest, Vol 212, Issue 7
> ***********************************