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
Dorota Leszczyńska-Jasion Department of Logic and Cognitive Science, Faculty of Psychology and Cognitive Science, Adam Mickiewicz University, Poznań, Poland

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
Google Scholar

[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
Google Scholar

[3]J. R. Hindley, Basic simple type theory, Cambridge University Press, Cambridge, 1997. https://doi.org/10.1017/CBO9780511608865
Google Scholar

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

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

[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
Google Scholar

[7] S. Negri and J. von Plato, Structural Proof Theory, Cambridge University Press, Cambridge, 2001. https://doi.org/10.1017/CBO9780511527340
Google Scholar

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

[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
Google Scholar

[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
Google Scholar

[11] A. S. Troelstra and H. Schwichtenberg, Basic Proof Theory, Camridge University Press, Cambridge, second edition, 2000. https://doi.org/10.1017/CBO9781139168717
Google Scholar

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