Classical logic with Mendler induction

descriptionPublicationkeyboard_double_arrow_right Article , Conference object 01 Jan 2020Embargo end date: 16 Sep 2020 United Kingdom English Publisher:Oxford University Press (OUP)Journal:Journal of Logic and Computation, volume 30, pages 77-106 (issn: 0955-792X, eissn: 1465-363X,

Copyright policy )

Authors: Devesas Campos, Marco; Fiore, Marcelo;

doi: 10.1093/logcom/exaa004 , 10.17863/cam.57474

Classical logic with Mendler induction

- Summary
- Subjects
- Metrics

Abstract

AbstractWe 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.

Country

United Kingdom

Related Organizations

University of Cambridge
United Kingdom

Keywords

46 Information and Computing Sciences, 50 Philosophy and Religious Studies, 5003 Philosophy, 49 Mathematical Sciences, 4904 Pure Mathematics

Impact byBIP!

	selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	1
	popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.	Average
	influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	Average
	impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.	Average