An Investigation into Intuitionistic Logic with Identity

Szymon Chlebowski; Dorota Leszczyńska-Jasion

Bulletin of the Section of Logic (2019)

  • Volume: 48, Issue: 4
  • ISSN: 0138-0680

Abstract

top
We define Kripke semantics for propositional intuitionistic logic with Suszko’s identity (ISCI). We propose sequent calculus for ISCI along with cut-elimination theorem. We sketch a constructive interpretation of Suszko’s propositional identity connective.

How to cite

top

Szymon Chlebowski, and Dorota Leszczyńska-Jasion. "An Investigation into Intuitionistic Logic with Identity." Bulletin of the Section of Logic 48.4 (2019): null. <http://eudml.org/doc/295545>.

@article{SzymonChlebowski2019,
abstract = {We define Kripke semantics for propositional intuitionistic logic with Suszko’s identity (ISCI). We propose sequent calculus for ISCI along with cut-elimination theorem. We sketch a constructive interpretation of Suszko’s propositional identity connective.},
author = {Szymon Chlebowski, Dorota Leszczyńska-Jasion},
journal = {Bulletin of the Section of Logic},
keywords = {Non-Fregean logics; intuitionistic logic; admissibility of cut; propositional identity; congruence},
language = {eng},
number = {4},
pages = {null},
title = {An Investigation into Intuitionistic Logic with Identity},
url = {http://eudml.org/doc/295545},
volume = {48},
year = {2019},
}

TY - JOUR
AU - Szymon Chlebowski
AU - Dorota Leszczyńska-Jasion
TI - An Investigation into Intuitionistic Logic with Identity
JO - Bulletin of the Section of Logic
PY - 2019
VL - 48
IS - 4
SP - null
AB - We define Kripke semantics for propositional intuitionistic logic with Suszko’s identity (ISCI). We propose sequent calculus for ISCI along with cut-elimination theorem. We sketch a constructive interpretation of Suszko’s propositional identity connective.
LA - eng
KW - Non-Fregean logics; intuitionistic logic; admissibility of cut; propositional identity; congruence
UR - http://eudml.org/doc/295545
ER -

References

top
  1. [1] S. L. Bloom and R. Suszko, Investigations into the sentential calculus with identity, Notre Dame Journal of Formal Logic, Vol. 13, No. 3 (1972), pp. 289–308. http://dx.doi.org/10.1305/ndjfl/1093890617 
  2. [2] J. G. Granström, Treatise on intuitionistic type theory, Springer Science & Business Media, Dordrecht, 2011. http://dx.doi.org/10.1007/978-94-007-1736-7 
  3. [3]J. R. Hindley, Basic simple type theory, Cambridge University Press, Cambridge, 1997. https://doi.org/10.1017/CBO9780511608865 
  4. [4] S. C. Kleene, Introduction to Metamathematics, Amsterdam: North-Holland Publishing Co.; Groningen: P. Noordhoff N.V., 1952. 
  5. [5] P. Łukowski, Intuitionistic sentential calculus with identity, Bulletin of the Section of Logic, Vol. 19, No. 3 (1990), pp. 92–99. 
  6. [6] S. Negri and J. von Plato, Cut elimination in the presence of axioms, Bulletin of Symbolic Logic, Vol. 4, No. 04 (1998), pp. 418–435. https://doi.org/10.2307/420956 
  7. [7] S. Negri and J. von Plato, Structural Proof Theory, Cambridge University Press, Cambridge, 2001. https://doi.org/10.1017/CBO9780511527340 
  8. [8] S. Negri and J. von Plato, Proof Analysis: a Contribution to Hilbert’s Last Problem, Cambridge University Press, Cambridge, 2011. 
  9. [9] S. Negri, J. von Plato, and T. Coquand, Proof-theoretical analysis of order relations, Archive for Mathematical Logic, Vol. 43, No. 3 (2004), pp. 297–309. https://doi.org/10.1007/s00153-003-0209-8 
  10. [10] R. Suszko, Abolition of the Fregean axiom, [in:] R. Parikh (ed.), Logic Colloquium, pp. 169–239, Berlin, Heidelberg, 1975, Springer. https://doi.org/10.1007/BFb0064874 
  11. [11] A. S. Troelstra and H. Schwichtenberg, Basic Proof Theory, Camridge University Press, Cambridge, second edition, 2000. https://doi.org/10.1017/CBO9781139168717 
  12. [12] L. Viganò, Labelled non-classical logics, Kluwer Academic Publishers, Boston, 2000. https://doi.org/10.1007/978-1-4757-3208-5 

NotesEmbed ?

top

You must be logged in to post comments.