This is an outdated version published on 2023-08-09. Read the most recent version.

Core Type Theory

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

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

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

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

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

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

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

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

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

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

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

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

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

N. Tennant, Core Logic, Oxford University Press, Oxford (2017).
Google Scholar

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

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

Downloads

Published

2023-08-09

Versions

2023-08-16 (2)
2023-08-09 (1)

How to Cite

van Dijk, E., Ripley, D., & Gutierrez, J. (2023). Core Type Theory. Bulletin of the Section of Logic, 52(2), 145–186. https://doi.org/10.18778/0138-0680.2023.19