Core Type Theory

Emma van Dijk; David Ripley; Julian Gutierrez

doi:10.18778/0138-0680.2023.19

Authors

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

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 DOI: https://doi.org/10.18778/0138-0680.2023.18

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

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

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 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. 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).

J. Hindley, J. P. Seldin, Lambda-Calculus and Combinators: an Introduction, Cambridge University Press, Cambridge (2008), DOI: https://doi.org/10.1017/CBO9780511809835 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.

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 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 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 DOI: https://doi.org/10.1007/s11245-018-9543-7

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

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.

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

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

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 DOI: https://doi.org/10.1017/S0022481200029674

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

N. Tennant, On Paradox without Self-Reference, Analysis, vol. 55(3) (1995), pp. 199–207, DOI: https://doi.org/10.2307/3328581 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 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 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 DOI: https://doi.org/10.1017/S1755020311000360

N. Tennant, Core Logic, Oxford University Press, Oxford (2017). 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.

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 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 DOI: https://doi.org/10.1016/j.jal.2017.01.002