Dissertations, Theses, and Capstone Projects

Date of Degree

10-2014

Document Type

Dissertation

Degree Name

Ph.D.

Program

Computer Science

Advisor

Sergei Artemov

Subject Categories

Computer Sciences | Logic and Foundations of Mathematics | Mathematics

Keywords

BHK Semantics, Constructive Semantics, Justification Logic, Prehistoric Graph, Provability Semantics, Self-referentiality

Abstract

This thesis explores self-referentiality in the framework of justification logic. In this framework initialed by Artemov, the language has formulas of the form t:F, which means "the term t is a justification of the formula F." Moreover, terms can occur inside formulas and hence it is legal to have t:F(t), which means "the term t is a justification of the formula F about t itself." Expressions like this is not only interesting in the semantics of justification logic, but also, as we will see, necessary in applications of justification logic in formalizing constructive contents implicitly carried by modal and intuitionistic logics.

Works initialed by Artemov and followed by Brezhnev and others have successfully extracted constructive contents packaged by modality in many modal logics. Roughly speaking, they offer methods of substituting modalities by terms in various justification logics, and then computing the exact structure of each term. After performing these methods, each formula prefixed by a modality becomes a formula prefixed by a term, which intuitively stands for the justification of the formula being prefixed. In terminology of this framework, we say that modal logics are "realized" in justification logics.

Within the family of justification logics, the Logic of Proofs LP is perhaps the most important member. As Artemov showed, this logic is not only complete w.r.t. to arithmetical semantics about proofs, but also accommodates the modal logic S4 via realization. Combined with Godel's modal embedding from intuitionistic propositional logic IPC to S4, the Logic of Proofs LP serves as an intermedium via which IPC receives its provability semantics, also known as Brouwer-Heyting-Kolmogorov semantics, or BHK semantics.

This thesis presents the candidate's works in two directions. (1) Following Kuznets'result that self-referentiality is necessary for the realization of several modal logics including S4, we show that it is also necessary for BHK semantics. (2) We find a necessary condition for a modal theorem to require self-referentiality in its realization, and using this condition to derive many interesting properties about self-referentiality.

Download

Share

COinS