coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Cut Elimination Theorem

From: Daniel Schepler <dschepler AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Cut Elimination Theorem
Date: Wed, 16 May 2018 12:55:54 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=dschepler AT gmail.com; spf=Pass smtp.mailfrom=dschepler AT gmail.com; spf=None smtp.helo=postmaster AT mail-oi0-f41.google.com
Ironport-phdr: 9a23:AO8ApBNbS+X4DINRb4Ul6mtUPXoX/o7sNwtQ0KIMzox0LfT+rarrMEGX3/hxlliBBdydt6ofzbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxlGiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0vRz+s87lkRwPpiCcfNj427mfXitBrjKlGpB6tvgFzz5LIbI2QMvd1Y6HTcs4ARWdZXMlRWSxPDI2/YYUSEeQOIf1Vr5Xhq1YUsReyGRWgCeHpxzRVhnH2x6o60+E5HA/IxgMgGdMOv2rQrN7oKakdTeC1w7fQzTXHcfxWwyr25Y/VfRA6vf6MXax/cdLVyUYxDQPIlVqQqYn/MDOU0uQBqXSU7+1lVe+2jWMstg9/oj+qxsg2i4nJgJoYyl/F9SVlwIY1OMa3RFRnbt6jFZtdsTyROYhuQs46XW1kpCI3xqcFtJO7ZiQG1okryh3FZ/GIboSF5A/oWvyLLjdinn1lfaqyhxas/kikze3xTsy030xLripBi9XMsXEN2wDK5siJRfZx412t2TmI1wDU5eFEJV47mbDHJJ4mx748jpsTsULdES/qgEj6krOae0E+9uWr6+nreKvqqoKfOoNuhQzyL7wimsmlDuQ5NggOUXKb+eO51LD74EL5W6lFjv0onanBtJDVO94bq7W2Aw9QyIkj6hK/Ay2639QfmHkLNEhFdw6fj4j1J1HOJ+j1Auu4g1S1iTtk2/TGPqD6DZjWNXjCkLLhfa5n5EJGyQozy8pf55NOBb0bLvLzQBy5iNuNJRggeyew3uyvXN56z8YVXX+FKq6fKqLb91GSsLEBOe6JMaMcvjfwL7Ae7P7jlXs0gxdJcbKi3ZYPbH2iNvtjKkSdJ3Hrh4FSQi8xogMiQbmy2xW5WjlJaiP3Bvpkv2BpOMedFY7GA7uVrvmE1Sa/EIdRYzkfWF+JGHbsMY6DXqVVMX7AEopaijUBEIOZZco5zxj37V31zrNmKqzf/ShK7cu+hugw3PXakFQJzRIxD8mZ1DvQHWR9n2dNQD5uma4j+ApyzVCM1aU+iPtdR4Re

On Wed, May 16, 2018 at 10:41 AM, Lourdes Del Carmen Gonzalez Huesca
<luglzhuesca AT gmail.com>
wrote:
> I was wondering if there is a formalization of Gentzen's hauptsatz or the
> cut elimination theorem.

I have a formalization of cut elimination for propositional calculus
here:
https://github.com/dschepler/coq-sequent-calculus/blob/master/SequentCalculus.v
. (The SC_proves inductive proposition is a cut-free variant, and
then SC_admits_cut near the bottom is the main result.)
--
Daniel Schepler

[Coq-Club] Cut Elimination Theorem, Lourdes Del Carmen Gonzalez Huesca, 05/16/2018
- Re: [Coq-Club] Cut Elimination Theorem, Carlos Olarte, 05/16/2018
- Re: [Coq-Club] Cut Elimination Theorem, Daniel Schepler, 05/16/2018
  - Re: [Coq-Club] Cut Elimination Theorem, Lourdes Del Carmen Gonzalez Huesca, 05/18/2018