Core Type Theory

Emma van Dijk; David Ripley; Julian Gutierrez

doi:10.18778/0138-0680.2023.19

Authors

Emma van Dijk
David Ripley Monash University, Philosophy Department, SOPHIS, Building 11, Monash University, Clayton, VIC, Australia
Julian Gutierrez Monash University, Department of Data Science & AI, Woodside Building, Monash University, Clayton, VIC, Australia

DOI:

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

Keywords:

core logic, type theory, strong normalization

Abstract

Neil Tennant’s core logic is a type of bilateralist natural deduction system based on proofs and refutations. We present a proof system for propositional core logic, explain its connections to bilateralism, and explore the possibility of using it as a type theory, in the same kind of way intuitionistic logic is often used as a type theory. Our proof system is not Tennant’s own, but it is very closely related, and determines the same consequence relation. The difference, however, matters for our purposes, and we discuss this. We then turn to the question of strong normalization, showing that although Tennant’s proof system for core logic is not strongly normalizing, our modified system is.

References

S. Ayhan, H. Wansing, On synonymy in proof-theoretic semantics: The case of 2Int, Bulletin of the Section of Logic, vol. Online First (2023), DOI: https://doi.org/10.18778/0138-0680.2023.18
Google Scholar DOI: https://doi.org/10.18778/0138-0680.2023.18

H. P. Barendregt, The Lambda Calculus: Its Syntax and Semantics, Elsevier, Amsterdam (1984).
Google Scholar

A. Church, The Calculi of Lambda-Conversion, Princeton University Press, Princeton, New Jersey (1941).
Google Scholar

A. Dı́az-Caro, G. Dowek, A new connective in natural deduction, and its application to quantum computing, [in:] International Colloquium on Theoretical Aspects of Computing, Springer (2021), pp. 175–193, DOI: https://doi.org/10.1007/978-3-030-85315-0_11
Google Scholar DOI: https://doi.org/10.1007/978-3-030-85315-0_11

G. Gentzen, Investigations Into Logical Deduction (1935), [in:] M. E. Szabo (ed.), The Collected Papers of Gerhard Gentzen, North-Holland Publishing Company, Amsterdam (1969), pp. 68–131.
Google Scholar DOI: https://doi.org/10.1016/S0049-237X(08)70822-X

J. Girard, P. Taylor, Y. Lafont, Proofs and Types, Cambridge University Press, Cambridge (1989).
Google Scholar

J. Hindley, J. P. Seldin, Lambda-Calculus and Combinators: an Introduction, Cambridge University Press, Cambridge (2008), DOI: https://doi.org/10.1017/CBO9780511809835
Google Scholar DOI: https://doi.org/10.1017/CBO9780511809835

W. H. Howard, The formulae-as-types notion of construction (1969), [in:] To HB Curry: Essays on combinatory logic, lambda calculus, and formalism, Academic Press (1980), pp. 479–490.
Google Scholar

D. Leivant, Assumption classes in natural deduction, Mathematical Logic Quarterly, vol. 25(1–2) (1979), pp. 1–4, DOI: https://doi.org/10.1002/malq.19790250102
Google Scholar DOI: https://doi.org/10.1002/malq.19790250102

S. Negri, J. von Plato, Structural Proof Theory, Cambridge University Press, Cambridge (2001), DOI: https://doi.org/10.1017/CBO9780511527340
Google Scholar DOI: https://doi.org/10.1017/CBO9780511527340

M. Petrolo, P. Pistone, On paradoxes in normal form, Topoi, vol. 38(3) (2019), pp. 605–617, DOI: https://doi.org/10.1007/s11245-018-9543-7
Google Scholar DOI: https://doi.org/10.1007/s11245-018-9543-7

D. Prawitz, Natural Deduction: A Proof-Theoretical Study, Almqvist and Wiksell, Stockholm (1965).
Google Scholar

D. Ripley, Strong normalization in core type theory, [in:] I. Sedlár, M. Blicha (eds.), The Logica Yearbook 2019, College Publications (2020), pp. 111–130.
Google Scholar

M. H. Sørensen, P. Urzyczyn, Lectures on the Curry-Howard isomorphism, Elsevier (2006).
Google Scholar DOI: https://doi.org/10.1016/S0049-237X(06)80005-4

N. Tennant, Anti-Realism and Logic, Oxford University Press, Oxford (1987).
Google Scholar

N. Tennant, Natural deduction and sequent calculus for intuitionistic relevant logic, Journal of Symbolic Logic, vol. 52(3) (1987), pp. 665–680, DOI: https://doi.org/10.2307/2274355
Google Scholar DOI: https://doi.org/10.1017/S0022481200029674

N. Tennant, Autologic: Proof theory and automated deduction, Edinburgh University Press, Edinburgh (1992).
Google Scholar

N. Tennant, On Paradox without Self-Reference, Analysis, vol. 55(3) (1995), pp. 199–207, DOI: https://doi.org/10.2307/3328581
Google Scholar DOI: https://doi.org/10.1093/analys/55.3.199

N. Tennant, What is Negation?, [in:] D. M. Gabbay, H. Wansing (eds.), Negation, Absurdity, and Contrariety, Kluwer Academic Publishers, Dordrecht (1999), pp. 199–222, DOI: https://doi.org/10.1007/978-94-015-9309-0_10
Google Scholar DOI: https://doi.org/10.1007/978-94-015-9309-0_10

N. Tennant, Ultimate normal forms for parallelized natural deductions, Logic Journal of the IGPL, vol. 10(3) (2002), pp. 299–337, DOI: https://doi.org/doi.org/10.1093/jigpal/10.3.299
Google Scholar DOI: https://doi.org/10.1093/jigpal/10.3.299

N. Tennant, Cut for Core Logic, Review of Symbolic Logic, vol. 5(3) (2012), pp. 450–479, DOI: https://doi.org/10.1017/S1755020311000360
Google Scholar DOI: https://doi.org/10.1017/S1755020311000360

N. Tennant, Core Logic, Oxford University Press, Oxford (2017).
Google Scholar DOI: https://doi.org/10.1093/oso/9780198777892.001.0001

H. Wansing, Proofs, disproofs, and their duals, [in:] L. Beklemishev, V. Goranko, V. Shehtman (eds.), Advances in Modal Logic, vol. 8, College Publications (2010), pp. 483–505.
Google Scholar

H. Wansing, Falsification, natural deduction and bi-intuitionistic logic, Journal of Logic and Computation, vol. 26(1) (2016), pp. 425–450, DOI: https://doi.org/10.1093/logcom/ext035
Google Scholar DOI: https://doi.org/10.1093/logcom/ext035

H. Wansing, A more general general proof theory, Journal of Applied Logic, vol. 25(1) (2017), pp. 23–46, DOI: https://doi.org/10.1016/j.jal.2017.01.002
Google Scholar DOI: https://doi.org/10.1016/j.jal.2017.01.002