Ryan Carpenter : A Consistency Proof for PA, part two

Posted by Ryan Carpenter , part of the Louise Hay Logic Seminar.

At

Sept. 18, 2024, 2 p.m.

In

427 SEO

Abstract

In part one of this talk, we introduced the Tait-style deduction calculus for PA, proved some elementary results, and showed how a proof of CUT-elimination for PA would entail its consistency. In this second part of the talk, we will define an auxiliary theory and proceed through a four-step procedure toward the end of showing that PA admits CUT-elimination for existential sequents, hence establishing its consistency à la Gentzen.