6

I think my question is a natural follow up of What would be some major consequences of the inconsistency of ZFC?

Regarding the later question, I agree with the commentaries that probably an inconsistency of ZFC would eventually be solved by technical improvements of the axioms (such as the improvement from the inconsistent axiom of unlimited comprehension to the separation axiom). I would even say that most of mathematical practice would go unchanged independtly of the inconsistency and its solution, as it was the case with Russel's Paradox (with exception, maybe, of areas of mathematics that uses a lot of set theory, such as point-set topology).

I would also like to point that I'm not going to discuss the extreme possibility that first-order PA is inconsistent, discussed here

I'm curious about a intermediate situation between PA and ZFC: full second-order arithmetic, which I will call Z2.

I know that, extending Gentzen's work on the consistency of PA, some consistency results were obtained for certain subsystems of second-order arithmetic (although I couldn't say exactly what). I point out also that there is a consistency proof for Z2 due to Spector, but most people working on foundations of mathematics don't see it as consistency proof in the sense of (extended) Hilbert's Program.

Saying all that, I am interested in the possible consequences of the inconsistency of Z2 because this theory corresponds more or less with Analysis and, unlike set theory, which clearly deals with very high levels of abstraction, deals with what most mathematicians would consider rather concrete objects.

I'm also curious about a possible inconsistency given the foundational role of Z2: as it was discovered in the program of Reverse Mathematics, a surprisingly big amount of usual mathematical practice can be carried out in Z2; or, being more precise, in some of its subsystems.

Of course it is an inherently vague question to ask 'what would be the consequences of the inconsistency of Z2', and indeed I am not sure if this question (at least in the way I put it) is adequate for mathoverflow (in case it isn't, fell free to close it or suggest editions to make it adequate), but I would like to see opinions justified by actual mathematics on what could happen in this case.

PS: Also, I am not sure about what tags I should associate with this question, so I am gladly taking suggestions.

jg1896
  • 2,683
  • 9
  • 24
  • 6
    This is not necessarily directly relevant to your question but Arai has recently claimed an ordinal analysis of full second-order arithmetic. – James Hanson Nov 25 '23 at 20:34
  • @JamesHanson Holy heck that's news to me! How'd I miss that? – Noah Schweber Nov 25 '23 at 20:37
  • 1
    @NoahSchweber It's not directly stated in the abstract that the paper contains it, so it might be easy to miss. – James Hanson Nov 25 '23 at 20:38
  • 2
    To the OP, even Z2 is still far away from the bulk of mathematical practice; to get anything seriously problematic to mathematics-as-practiced (as opposed to blood-pressure-of-logicians-including-me-personally), something like $\mathsf{ATR}_0$ is a more vicious nightmare. – Noah Schweber Nov 25 '23 at 20:39
  • @JamesHanson thank you for sharing! I was not aware of Arai's work – jg1896 Nov 25 '23 at 20:42
  • 5
    Now I’m imagining brochures with cartoon diagrams, like they put in the seat back pockets of airplanes, explaining what to do if a certain mathematical systems are found to be inconsistent… – Sam Hopkins Nov 25 '23 at 20:55
  • 1
    Can you give some details on Spector's result? Are you referring to Spector, Clifford. Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles formulated in current intuitionistic mathematics. Proc. Sympos. Pure Math., Vol. V, pp. 1–27, Amer. Math. Soc., Providence, RI, 1962 ? – Mikhail Katz Nov 27 '23 at 13:22
  • 1
    Yes, its this paper. After Gentzen's proof of the consistency of PA, Gödel in 1958 gave a different one, called Gödels' functional dialectica interpretation (a nice exposition of this proof appears in the textbook of Shoenfield). The main idea of Gödels proof is to reduce the consistency of PA to the consistency of a quantifier-free theory theory of functionals of finite type. Spector's consistency proof for analysis uses the same system + bar recursion. Almost every logician agree that bar recursion is not finitistic in any sense similar to the extendend Hilbert Program. – jg1896 Nov 27 '23 at 13:37

0 Answers0