We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

math.LO

Change to browse by:

References & Citations

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Mathematics > Logic

Title: Unified Correspondence and Proof Theory for Strict Implication

Abstract: The unified correspondence theory for distributive lattice expansion logics (DLE-logics) is specialized to strict implication logics. As a consequence of a general semantic consevativity result, a wide range of strict implication logics can be conservatively extended to Lambek Calculi over the bounded distributive full non-associative Lambek calculus (BDFNL). Many strict implication sequents can be transformed into analytic rules employing one of the main tools of unified correspondence theory, namely (a suitably modified version of) the Ackermann lemma based algorithm $\msf{ALBA}$. Gentzen-style cut-free sequent calculi for BDFNL and its extensions with analytic rules which are transformed from strict implication sequents, are developed.
Comments: This is a Pre-publication version of a submission to the Journal of Logic and Computation
Subjects: Logic (math.LO)
DOI: 10.1093/logcom/exw012
Cite as: arXiv:1604.08822 [math.LO]
  (or arXiv:1604.08822v1 [math.LO] for this version)

Submission history

From: Zhiguang Zhao [view email]
[v1] Fri, 29 Apr 2016 13:30:55 GMT (38kb)

Link back to: arXiv, form interface, contact.