Admissibility of Cut in LC with Fixed Point Combinator

Author： Bimbó Katalin  

Publisher： Springer Publishing Company

ISSN： 0039-3215

Source： Studia Logica, Vol.81, Iss.3, 2005-12, pp. : 399-423

Disclaimer: Any content in publications that violate the sovereignty, the constitution or regulations of the PRC is not accepted or approved by CNPIEC.

Previous Menu Next

Abstract

The fixed point combinator (Y) is an important non-proper combinator, which is defhable from a combinatorially complete base. This combinator guarantees that recursive equations have a solution. Structurally free logics (LC) turn combinators into formulas and replace structural rules by combinatory ones. This paper introduces the fixed point and the dual fixed point combinator into structurally free logics. The admissibility of (multiple) cut in the resulting calculus is not provable by a simple adaptation of the similar proof for LC with proper combinators. The novelty of our proof—beyond proving the cut for a newly extended calculus–is that we add a fourth induction to the by-and-large Gentzen-style proof.

Related content

Cut-elimination for Weak Grzegorczyk Logic Go

By Goré Rajeev   Ramanayake Revantha  

Studia Logica, Vol. 102, Iss. 1, 2014-02 ,pp. : 1-27 (27)

Springer Publishing Company

Access to resources Recommend Favorite

Combinator Logics

By  

Studia Logica, Vol. 76, Iss. 1, 2004-01 ,pp. : 17-66 (50)

Springer Publishing Company

Access to resources Recommend Favorite

Iterative and fixed point common belief

By Heifetz A.  

Journal of Philosophical Logic, Vol. 28, Iss. 1, 1999-02 ,pp. : 61-79 (19)

Springer Publishing Company

Access to resources Recommend Favorite

Note on Some Fixed Point Constructions in Provability Logic

By Lindström Per  

Journal of Philosophical Logic, Vol. 35, Iss. 3, 2006-06 ,pp. : 225-230 (6)

Springer Publishing Company

Access to resources Recommend Favorite

Tarski's Fixed-Point Theorem And Lambda Calculi With Monotone Inductive Types

By Matthes R.  

Synthese, Vol. 133, Iss. 1-2, 2002-10 ,pp. : 107-129 (23)

Springer Publishing Company

Access to resources Recommend Favorite