An Investigation into Intuitionistic Logic with Identity

Szymon Chlebowski; Dorota Leszczyńska-Jasion

doi:10.18778/0138-0680.48.4.02

Authors

Szymon Chlebowski Department of Logic and Cognitive Science, Faculty of Psychology and Cognitive Science, Adam Mickiewicz University, Poznań, Poland Author
Dorota Leszczyńska-Jasion Department of Logic and Cognitive Science, Faculty of Psychology and Cognitive Science, Adam Mickiewicz University, Poznań, Poland Author

DOI:

https://doi.org/10.18778/0138-0680.48.4.02

Keywords:

Non-Fregean logics, intuitionistic logic, admissibility of cut, propositional identity, congruence

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.

References

[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] 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]J. R. Hindley, Basic simple type theory, Cambridge University Press, Cambridge, 1997. https://doi.org/10.1017/CBO9780511608865

[4] S. C. Kleene, Introduction to Metamathematics, Amsterdam: North-Holland Publishing Co.; Groningen: P. Noordhoff N.V., 1952.

[5] P. Łukowski, Intuitionistic sentential calculus with identity, Bulletin of the Section of Logic, Vol. 19, No. 3 (1990), pp. 92–99.

[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] S. Negri and J. von Plato, Structural Proof Theory, Cambridge University Press, Cambridge, 2001. https://doi.org/10.1017/CBO9780511527340

[8] S. Negri and J. von Plato, Proof Analysis: a Contribution to Hilbert’s Last Problem, Cambridge University Press, Cambridge, 2011.

[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] 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] A. S. Troelstra and H. Schwichtenberg, Basic Proof Theory, Camridge University Press, Cambridge, second edition, 2000. https://doi.org/10.1017/CBO9781139168717

[12] L. Viganò, Labelled non-classical logics, Kluwer Academic Publishers, Boston, 2000. https://doi.org/10.1007/978-1-4757-3208-5