Constructive canonicity of inductive inequalities

Willem Conradie; Alessandra Palmigiano

doi:10.23638/LMCS-16(3:8)2020

Constructive canonicity of inductive inequalities

Willem Conradie
, Alessandra Palmigiano

Ethics, Governance and Society

Research output: Contribution to Journal › Article › Academic › peer-review

Abstract

We prove the canonicity of inductive inequalities in a constructive meta-theory, for classes of logics algebraically captured by varieties of normal and regular lattice ex-pansions. This result encompasses Ghilardi-Meloni’s and Suzuki’s constructive canonicity results for Sahlqvist formulas and inequalities, and is based on an application of the tools of unified correspondence theory. Specifically, we provide an alternative interpretation of the language of the algorithm ALBA for lattice expansions: nominal and conominal variables are respectively interpreted as closed and open elements of canonical extensions of normal/regular lattice expansions, rather than as completely join-irreducible and meet-irreducible elements of perfect normal/regular lattice expansions. We show the correctness of ALBA with respect to this interpretation. From this fact, the constructive canonicity of the inequalities on which ALBA succeeds follows by an adaptation of the standard argument. The claimed result then follows as a consequence of the success of ALBA on inductive inequalities.

Original language	English
Article number	8
Pages (from-to)	8:1-8:39
Number of pages	39
Journal	Logical Methods in Computer Science
Volume	16
Issue number	3
DOIs	https://doi.org/10.23638/LMCS-16(3:8)2020
Publication status	Published - 5 Aug 2020

Funding

2010 Mathematics Subject Classification: 03B45, 06D50, 06D10, 03G10, 06E15. Key words and phrases: modal logic, Sahlqvist theory, algorithmic correspondence theory, constructive canonicity, lattice theory. 1 Supported by the National Research Foundation of South Africa, Grant number 81309, and the financial assistance of the Faculty of Science of the University of the Witwatersrand. 2 Supported by the NWO Vidi grant 016.138.314, by the NWO Aspasia grant 015.008.054, and by a Delft Technology Fellowship awarded in 2013. 1 Supported by the National Research Foundation of South Africa, Grant number 81309, and the financial assistance of the Faculty of Science of the University of the Witwatersrand.2 Supported by the NWO Vidi grant 016.138.314, by the NWO Aspasia grant 015.008.054, and by a Delft Technology Fellowship awarded in 2013.

Funders	Funder number
University of the Witwatersrand, Johannesburg
Nederlandse Organisatie voor Wetenschappelijk Onderzoek	015.008.054, 016.138.314
National Research Foundation	81309

UN SDGs

This output contributes to the following UN Sustainable Development Goals (SDGs)

SDG 10 Reduced Inequalities

Keywords

Algorithmic correspondence theory
Constructive canonicity
Lattice theory
Modal logic
Sahlqvist theory

Access to Document

10.23638/LMCS-16(3:8)2020

https://lmcs.episciences.org/6694

Persistent URL (handle)

Persistent link

Cite this

@article{6ae750e96257493d8319abaf2a6da610,

title = "Constructive canonicity of inductive inequalities",

abstract = "We prove the canonicity of inductive inequalities in a constructive meta-theory, for classes of logics algebraically captured by varieties of normal and regular lattice ex-pansions. This result encompasses Ghilardi-Meloni{\textquoteright}s and Suzuki{\textquoteright}s constructive canonicity results for Sahlqvist formulas and inequalities, and is based on an application of the tools of unified correspondence theory. Specifically, we provide an alternative interpretation of the language of the algorithm ALBA for lattice expansions: nominal and conominal variables are respectively interpreted as closed and open elements of canonical extensions of normal/regular lattice expansions, rather than as completely join-irreducible and meet-irreducible elements of perfect normal/regular lattice expansions. We show the correctness of ALBA with respect to this interpretation. From this fact, the constructive canonicity of the inequalities on which ALBA succeeds follows by an adaptation of the standard argument. The claimed result then follows as a consequence of the success of ALBA on inductive inequalities.",

keywords = "Algorithmic correspondence theory, Constructive canonicity, Lattice theory, Modal logic, Sahlqvist theory",

author = "Willem Conradie and Alessandra Palmigiano",

year = "2020",

month = aug,

day = "5",

doi = "10.23638/LMCS-16(3:8)2020",

language = "English",

volume = "16",

pages = "8:1--8:39",

journal = "Logical Methods in Computer Science",

issn = "1860-5974",

publisher = "Technischen Universitat Braunschweig",

number = "3",

}

TY - JOUR

T1 - Constructive canonicity of inductive inequalities

AU - Conradie, Willem

AU - Palmigiano, Alessandra

PY - 2020/8/5

Y1 - 2020/8/5

N2 - We prove the canonicity of inductive inequalities in a constructive meta-theory, for classes of logics algebraically captured by varieties of normal and regular lattice ex-pansions. This result encompasses Ghilardi-Meloni’s and Suzuki’s constructive canonicity results for Sahlqvist formulas and inequalities, and is based on an application of the tools of unified correspondence theory. Specifically, we provide an alternative interpretation of the language of the algorithm ALBA for lattice expansions: nominal and conominal variables are respectively interpreted as closed and open elements of canonical extensions of normal/regular lattice expansions, rather than as completely join-irreducible and meet-irreducible elements of perfect normal/regular lattice expansions. We show the correctness of ALBA with respect to this interpretation. From this fact, the constructive canonicity of the inequalities on which ALBA succeeds follows by an adaptation of the standard argument. The claimed result then follows as a consequence of the success of ALBA on inductive inequalities.

AB - We prove the canonicity of inductive inequalities in a constructive meta-theory, for classes of logics algebraically captured by varieties of normal and regular lattice ex-pansions. This result encompasses Ghilardi-Meloni’s and Suzuki’s constructive canonicity results for Sahlqvist formulas and inequalities, and is based on an application of the tools of unified correspondence theory. Specifically, we provide an alternative interpretation of the language of the algorithm ALBA for lattice expansions: nominal and conominal variables are respectively interpreted as closed and open elements of canonical extensions of normal/regular lattice expansions, rather than as completely join-irreducible and meet-irreducible elements of perfect normal/regular lattice expansions. We show the correctness of ALBA with respect to this interpretation. From this fact, the constructive canonicity of the inequalities on which ALBA succeeds follows by an adaptation of the standard argument. The claimed result then follows as a consequence of the success of ALBA on inductive inequalities.

KW - Algorithmic correspondence theory

KW - Constructive canonicity

KW - Lattice theory

KW - Modal logic

KW - Sahlqvist theory

UR - https://www.scopus.com/pages/publications/85090779479

UR - https://www.scopus.com/pages/publications/85090779479#tab=citedBy

U2 - 10.23638/LMCS-16(3:8)2020

DO - 10.23638/LMCS-16(3:8)2020

M3 - Article

AN - SCOPUS:85090779479

SN - 1860-5974

VL - 16

SP - 8:1-8:39

JO - Logical Methods in Computer Science

JF - Logical Methods in Computer Science

IS - 3

M1 - 8

ER -

Constructive canonicity of inductive inequalities

Abstract

Funding

UN SDGs

Keywords

Access to Document

Persistent URL (handle)

Other files and links

Fingerprint

Cite this