#матлог #учёба #спецсеминар #не_мехмат #МИАН #ТД

Logic Online Seminar (https://www.mathnet.ru/php/conference.phtml?eventID=9&confid=876&option_lang=eng), Monday 16:00 MSK (UTC+3), Kontur Talk (online only)

22.09.2025 Sergei Artemov (Graduate Center CUNY, https://sartemov.ws.gc.cuny.edu/): Representing and proving the consistency of PA in PA

We prove that the PA-consistency property is provably in PA equivalent to the scheme ConS(PA): for n=0,1,2,..., "n is not a code of a proof of (0=1)." Since the consistency formula Con(PA) is strictly stronger than ConS(PA) in PA, the unprovability of Con(PA) in PA does not settle the question of provability of the consistency, which remained in limbo and has been reduced to finding a finite proof in PA of ConS(PA). Following Hlbert's approach to proving consistency, we offer the general notion of a proof of a sequence of PA-formulas F_1, F_2,..., F_n,... as a pair of a primitive recursive function (selector) s and a proof of "for each n, s(n) is a PA-proof of F_n." We demonstrate that "PA is consistent" is provable in PA. These findings apply to a broad class of formal theories, including ZF.

Reading materials:

S. Artemov, Consistency formula is strictly stronger in PA than PA-consistency (https://doi.org/10.48550/arXiv.2508.20346)
S. Artemov, Serial properties, selector proofs and the provability of consistency, Journal of Logic and Computation, 35(3), April 2025 (https://doi.org/10.1093/logcom/exae034)

➰ ВК