Louise Hay Logic Seminar
Ryan Carpenter
UIC
A Consistency Proof for PA, part two
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.
Wednesday September 18, 2024 at 2:00 PM in 427 SEO