Constructive canonicity for lattice-based fixed point logics

Conradie, Willem; Craig, Andrew; Palmigiano, A.; Zhao, Z.

Constructive canonicity for lattice-based fixed point logics

Conference paper (2017)

Authors

Willem Conradie University of Johannesburg

Andrew Craig University of Johannesburg

A. Palmigiano University of Johannesburg,

Z. Zhao

Canonicity Unified correspondence Lattice-based fixed point logics Logics for categorization

To reference this document use:

http://resolver.tudelft.nl/uuid:3ed598f8-6b19-4bd7-b4fe-bf86632b4668

More Info

expand_more

Published Date

2017

Language

English

Reuse Rights

Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.

Abstract

In the present paper, we prove canonicity results for lattice-based fixed point logics in a constructive meta-theory. Specifically, we prove two types of canonicity results, depending on how the fixed-point binders are interpreted. These results smoothly unify the constructive canonicity results for inductive inequalities, proved in a general lattice setting, with the canonicity results for fixed point logics on a bi-intuitionistic base, proven in a non-constructive setting.

Files

Conradie2017_Chapter_Construct... (pdf)

(pdf | 0.428 Mb)

Unknown license

Download not available