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.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.