Dissertations, Theses, and Capstone Projects

Date of Degree

9-2021

Document Type

Dissertation

Degree Name

Ph.D.

Program

Computer Science

Advisor

Sergei Artemov

Committee Members

Melvin Fitting

Subash Shankar

Evangelia Antonakos

Subject Categories

Computer Sciences

Abstract

It is a well-known result by G ̈odel in 1933 that the Intuitionistic Logic can be embedded into a system which is essentially equivalent to the modal logic S4. This can be considered to be an attempt to provide a provability semantics to the Intuitionistic Logic. This work had caused some problems: the exact arithmetical meaning of the Intuitionistic Logic and S4, the exact axiomatization of formal provability in formal arithmetic and the standard model of arithmetic. These days the arithmetical interpretation has been extended and generalized to epistemological interpretation for various modal logics, which resulted in various systems of Justification Logic. In Part I (Chapters 2-4) of this dissertation, we are concerned with logical system on provability and Justification Logic.

A resource logic called Linear Logic LL is considered to be a refinement of S4 with explicit distinction of the two fragments: resource-conscious and modal fragments. The embedding result of the Intuitionistic Logic to LL still holds and the former is provided a resource semantics via LL. In Part II (Chapters 5-7), we study variations of LL and relationship between LL and Justification Logic.

In Chapter 2, we report the new technique to realize a wide range of modal logics (epistemic logics) in justification logics. This method is modular and uniform for that range of modal logics. In Chapter 3, we propose a proof system for a basic logic known as the logic of provability in true arithmetic. The logic is basic and fundamental though a decent proof theory had not been explored for the logic. We offer the cut-elimination and some consequences of it: Craig interpolation theorem and definability theorem, and a proof-theoretic proof of the equivalence of the system and the well known system GL with respect to G ̈odel sentences. In Chapter 4, we propose a generalization of the notion of constructive falsity proposed by Artemov 2019. Then, we completely characterize the closed sentences of Peano Arithmetic. Moreover, we locate Rosser sentences, constructive liar sentences and Reflection principles in the hierarchy of the generalized constructive falsity. In Chapter 5, we extend the meaning the modality of linear logic of the inexhaustibility of a proposition to mean additionally common resources sharable among agents in a setting of multi-agent system. Then, we give an extension of linear logic with such a modality using the tool of hypersequent calculus, and show the cut-elimination. We also prove decidability and realizability in terms of justification logic. In Chapter 6, we consider another extension of modality of linear logic where modal formulas s : A mean ‘if s is available, A holds’, called ‘Linear Logic with explicit resources’. Then the usual modality is a special case of the empty resources. We show the cut-elimination and a type of realization theorem of linear logic to the pure fragment, that is, the subsystem of the extension without the original modality. In Chapter 7, we propose a bimodal substructural logic where one modality is the one in Linear Logic and the other is S4 modality which does not satisfy structural rules. We prove the cut-elimination and the realization theorem via the justification counterpart with two sorts of terms. Also, we consider the subsystem which lacks structural rules at all and establish that there occur no self-referentiality of constant specification of proofs. In Chapter 8, we close this thesis.

Download

Share

COinS