Geodesic
Core Type Theory
Bulletin of the Section of Logic, Tome 52 (2023) no. 2, pp. 145-186.

Voir la notice de l'article provenant de la source Library of Science

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.
Keywords: core logic, type theory, strong normalization 
@article{BSL_2023_52_2_a1,
     author = {van Dijk, Emma and Ripley, David and Gutierrez, Julian},
     title = {Core {Type} {Theory}},
     journal = {Bulletin of the Section of Logic},
     pages = {145--186},
     publisher = {mathdoc},
     volume = {52},
     number = {2},
     year = {2023},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/BSL_2023_52_2_a1/}
}
TY  - JOUR
AU  - van Dijk, Emma
AU  - Ripley, David
AU  - Gutierrez, Julian
TI  - Core Type Theory
JO  - Bulletin of the Section of Logic
PY  - 2023
SP  - 145
EP  - 186
VL  - 52
IS  - 2
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/BSL_2023_52_2_a1/
LA  - en
ID  - BSL_2023_52_2_a1
ER  - 
%0 Journal Article
%A van Dijk, Emma
%A Ripley, David
%A Gutierrez, Julian
%T Core Type Theory
%J Bulletin of the Section of Logic
%D 2023
%P 145-186
%V 52
%N 2
%I mathdoc
%U http://geodesic.mathdoc.fr/item/BSL_2023_52_2_a1/
%G en
%F BSL_2023_52_2_a1
van Dijk, Emma; Ripley, David; Gutierrez, Julian. Core Type Theory. Bulletin of the Section of Logic, Tome 52 (2023) no. 2, pp. 145-186. http://geodesic.mathdoc.fr/item/BSL_2023_52_2_a1/

[1] 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

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

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

[4] 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

[5] 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.

[6] J. Girard, P. Taylor, Y. Lafont, Proofs and Types, Cambridge University Press, Cambridge (1989).

[7] J. Hindley, J. P. Seldin, Lambda-Calculus and Combinators: an Introduction, Cambridge University Press, Cambridge (2008) | DOI

[8] 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.

[9] D. Leivant, Assumption classes in natural deduction, Mathematical Logic Quarterly, vol. 25(1–2) (1979), pp. 1–4 | DOI

[10] S. Negri, J. von Plato, Structural Proof Theory, Cambridge University Press, Cambridge (2001) | DOI

[11] M. Petrolo, P. Pistone, On paradoxes in normal form, Topoi, vol. 38(3) (2019), pp. 605–617 | DOI

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

[13] 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.

[14] M. H. Sørensen, P. Urzyczyn, Lectures on the Curry-Howard isomorphism, Elsevier (2006).

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

[16] N. Tennant, Natural deduction and sequent calculus for intuitionistic relevant logic, Journal of Symbolic Logic, vol. 52(3) (1987), pp. 665–680 | DOI

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

[18] N. Tennant, On Paradox without Self-Reference, Analysis, vol. 55(3) (1995), pp. 199–207 | DOI

[19] 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

[20] N. Tennant, Ultimate normal forms for parallelized natural deductions, Logic Journal of the IGPL, vol. 10(3) (2002), pp. 299–337 | DOI

[21] N. Tennant, Cut for Core Logic, Review of Symbolic Logic, vol. 5(3) (2012), pp. 450–479 | DOI

[22] N. Tennant, Core Logic, Oxford University Press, Oxford (2017).

[23] 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.

[24] H. Wansing, Falsification, natural deduction and bi-intuitionistic logic, Journal of Logic and Computation, vol. 26(1) (2016), pp. 425–450 | DOI

[25] H. Wansing, A more general general proof theory, Journal of Applied Logic, vol. 25(1) (2017), pp. 23–46 | DOI