Show simple item record

Core Type Theory

dc.contributor.authorvan Dijk, Emma
dc.contributor.authorRipley, David
dc.contributor.authorGutierrez, Julian
dc.date.accessioned2023-10-12T10:06:02Z
dc.date.available2023-10-12T10:06:02Z
dc.date.issued2023-08-16
dc.identifier.issn0138-0680
dc.identifier.urihttp://hdl.handle.net/11089/48070
dc.description.abstractNeil 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.en
dc.language.isoen
dc.publisherWydawnictwo Uniwersytetu Łódzkiegopl
dc.relation.ispartofseriesBulletin of the Section of Logic;2en
dc.rights.urihttps://creativecommons.org/licenses/by-nc-nd/4.0
dc.subjectcore logicen
dc.subjecttype theoryen
dc.subjectstrong normalizationen
dc.titleCore Type Theoryen
dc.typeOther
dc.page.number145-186
dc.contributor.authorAffiliationRipley, David - Monash University, Philosophy Department, SOPHIS, Building 11, Monash University, Clayton, VIC, Australiaen
dc.contributor.authorAffiliationGutierrez, Julian - Monash University, Department of Data Science & AI, Woodside Building, Monash University, Clayton, VIC, Australiaen
dc.identifier.eissn2449-836X
dc.referencesS. 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.18en
dc.referencesH. P. Barendregt, The Lambda Calculus: Its Syntax and Semantics, Elsevier, Amsterdam (1984).en
dc.referencesA. Church, The Calculi of Lambda-Conversion, Princeton University Press, Princeton, New Jersey (1941).en
dc.referencesA. 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_11en
dc.referencesG. 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.en
dc.referencesJ. Girard, P. Taylor, Y. Lafont, Proofs and Types, Cambridge University Press, Cambridge (1989).en
dc.referencesJ. Hindley, J. P. Seldin, Lambda-Calculus and Combinators: an Introduction, Cambridge University Press, Cambridge (2008), DOI: https://doi.org/10.1017/CBO9780511809835en
dc.referencesW. 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.en
dc.referencesD. Leivant, Assumption classes in natural deduction, Mathematical Logic Quarterly, vol. 25(1–2) (1979), pp. 1–4, DOI: https://doi.org/10.1002/malq.19790250102en
dc.referencesS. Negri, J. von Plato, Structural Proof Theory, Cambridge University Press, Cambridge (2001), DOI: https://doi.org/10.1017/CBO9780511527340en
dc.referencesM. 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-7en
dc.referencesD. Prawitz, Natural Deduction: A Proof-Theoretical Study, Almqvist and Wiksell, Stockholm (1965).en
dc.referencesD. Ripley, Strong normalization in core type theory, [in:] I. Sedlár, M. Blicha (eds.), The Logica Yearbook 2019, College Publications (2020), pp. 111–130.en
dc.referencesM. H. Sørensen, P. Urzyczyn, Lectures on the Curry-Howard isomorphism, Elsevier (2006).en
dc.referencesN. Tennant, Anti-Realism and Logic, Oxford University Press, Oxford (1987).en
dc.referencesN. 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/2274355en
dc.referencesN. Tennant, Autologic: Proof theory and automated deduction, Edinburgh University Press, Edinburgh (1992).en
dc.referencesN. Tennant, On Paradox without Self-Reference, Analysis, vol. 55(3) (1995), pp. 199–207, DOI: https://doi.org/10.2307/3328581en
dc.referencesN. 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_10en
dc.referencesN. 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.299en
dc.referencesN. Tennant, Cut for Core Logic, Review of Symbolic Logic, vol. 5(3) (2012), pp. 450–479, DOI: https://doi.org/10.1017/S1755020311000360en
dc.referencesN. Tennant, Core Logic, Oxford University Press, Oxford (2017).en
dc.referencesH. 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.en
dc.referencesH. 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/ext035en
dc.referencesH. 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.002en
dc.contributor.authorEmailvan Dijk, Emma - emmavandijk168@gmail.com
dc.contributor.authorEmailRipley, David - davewripley@gmail.com
dc.contributor.authorEmailGutierrez, Julian - julian.gutierrez@monash.edu
dc.identifier.doi10.18778/0138-0680.2023.19
dc.relation.volume52


Files in this item

Thumbnail
Name:
145-186_van_Dijk,_Ripley,_Guti ...
Size:
1.846Mb
Format:
PDF
View/Open

This item appears in the following Collection(s)

Show simple item record

https://creativecommons.org/licenses/by-nc-nd/4.0
Except where otherwise noted, this item's license is described as https://creativecommons.org/licenses/by-nc-nd/4.0