Skip to Main Content
Frequently Asked Questions
Submit an ETD
Global Search Box
Need Help?
Keyword Search
Participating Institutions
Advanced Search
School Logo
Files
File List
Dissertation-Final-Draft.pdf (579.22 KB)
ETD Abstract Container
Abstract Header
Justification Logic, Type Theory and the BHK Interpretation
Author Info
DeBoer, Neil J
Permalink:
http://rave.ohiolink.edu/etdc/view?acc_num=osu1598007830055549
Abstract Details
Year and Degree
2020, Doctor of Philosophy, Ohio State University, Mathematical Sciences.
Abstract
We explore two ways of formalizing Kriesel's addendum to the Brouwer-Heyting-Kolmogorov interpretation. To do this we compare Artemov's justification logic with simply typed λ calculus, by introducing a map from justification terms into λ terms, which can be viewed as a method of extracting the computational content of the justification terms. Then we examine the interpretation of Kreisel's addendum in justification logic along with the image of the resulting justification terms under our map. We also present an intuitionistic version of a fragment of first order justification logic, and then we present an adaptation of Fitting's semantics for first order justification logic for our intuitionistic first order justification logic. We prove that our semantics are both sound and complete with respect to our intutionistic logic.
Committee
Timothy Carlson (Advisor)
Christopher Miller (Committee Member)
Neil Tennant (Committee Member)
Pages
131 p.
Subject Headings
Logic
;
Mathematics
Keywords
Justification Logic, Type Theory, BHK Interpretation, Intuitionistic Logic, lambda calculus
Recommended Citations
Refworks
EndNote
RIS
Mendeley
Citations
DeBoer, N. J. (2020).
Justification Logic, Type Theory and the BHK Interpretation
[Doctoral dissertation, Ohio State University]. OhioLINK Electronic Theses and Dissertations Center. http://rave.ohiolink.edu/etdc/view?acc_num=osu1598007830055549
APA Style (7th edition)
DeBoer, Neil.
Justification Logic, Type Theory and the BHK Interpretation.
2020. Ohio State University, Doctoral dissertation.
OhioLINK Electronic Theses and Dissertations Center
, http://rave.ohiolink.edu/etdc/view?acc_num=osu1598007830055549.
MLA Style (8th edition)
DeBoer, Neil. "Justification Logic, Type Theory and the BHK Interpretation." Doctoral dissertation, Ohio State University, 2020. http://rave.ohiolink.edu/etdc/view?acc_num=osu1598007830055549
Chicago Manual of Style (17th edition)
Abstract Footer
Document number:
osu1598007830055549
Download Count:
337
Copyright Info
© 2020, some rights reserved.
Justification Logic, Type Theory and the BHK Interpretation by Neil J DeBoer is licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 3.0 Unported License. Based on a work at etd.ohiolink.edu.
This open access ETD is published by The Ohio State University and OhioLINK.