License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2021.29
URN: urn:nbn:de:0030-drops-142678
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/14267/
Go to the corresponding LIPIcs Volume Portal

Das, Anupam

On the Logical Strength of Confluence and Normalisation for Cyclic Proofs

pdf-format:
LIPIcs-FSCD-2021-29.pdf (0.9 MB)

Abstract

In this work we address the logical strength of confluence and normalisation for non-wellfounded typing derivations, in the tradition of "cyclic proof theory". We present a circular version CT of Gödel's system T, with the aim of comparing the relative expressivity of the theories CT and T. We approach this problem by formalising rewriting-theoretic results such as confluence and normalisation for the underlying "coterm" rewriting system of CT within fragments of second-order arithmetic.

We establish confluence of CT within the theory RCA₀, a conservative extension of primitive recursive arithmetic and IΣ1. This allows us to recast type structures of hereditarily recursive operations as "coterm" models of T. We show that these also form models of CT, by formalising a totality argument for circular typing derivations within suitable fragments of second-order arithmetic. Relying on well-known proof mining results, we thus obtain an interpretation of CT into T; in fact, more precisely, we interpret level-n-CT into level-(n+1)-T, an optimum result in terms of abstraction complexity.

A direct consequence of these model-theoretic results is weak normalisation for CT. As further results, we also show strong normalisation for CT and continuity of functionals computed by its type 2 coterms.

BibTeX - Entry

@InProceedings{das:LIPIcs.FSCD.2021.29,
  author =	{Das, Anupam},
  title =	{{On the Logical Strength of Confluence and Normalisation for Cyclic Proofs}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{29:1--29:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-191-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{195},
  editor =	{Kobayashi, Naoki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2021/14267},
  URN =		{urn:nbn:de:0030-drops-142678},
  doi =		{10.4230/LIPIcs.FSCD.2021.29},
  annote =	{Keywords: confluence, normalisation, system T, circular proofs, reverse mathematics, type structures}
}

Keywords: confluence, normalisation, system T, circular proofs, reverse mathematics, type structures
Collection: 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)
Issue Date: 2021
Date of publication: 06.07.2021

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI