Classical logic with Mendler induction
Published version
Peer-reviewed
Repository URI
Repository DOI
Change log
Authors
Devesas Campos, Marco
Fiore, Marcelo https://orcid.org/0000-0001-8558-3492
Abstract
We investigate (co-) induction in classical logic under the propositions-as-types paradigm, considering propositional, second-order and (co-) inductive types. Specifically, we introduce an extension of the Dual Calculus with a Mendler-style (co-) iterator and show that it is strongly normalizing. We prove this using a reducibility argument.
Description
Keywords
5003 Philosophy, 4904 Pure Mathematics, 49 Mathematical Sciences, 50 Philosophy and Religious Studies
Journal Title
Journal of Logic and Computation
Conference Name
Journal ISSN
0955-792X
1465-363X
1465-363X
Volume Title
30
Publisher
Oxford University Press (OUP)