Epistemic paradox and explicit modal logic

The dissertation presents a unified treatment of what I refer to as the epistemic paradoxes (i.e. the Knower Paradox of Montague and Kaplan [76] and Fitch's Paradox of Knowability [27]) in the context of a quantified extension of Artemov's [3] Logic of Proofs [LP]. The system adopted is a modified form of Fitting's [32] Quantified Logic of Proofs [QLP] and contains not only so-called explicit modalities (i.e. statements of the form t : &phiv with intended interpretation of "t denotes a proof of &phiv") but also first-order quantifiers intended to range over proofs or informal justifications. This allows for a formalization of a justification-based notion of knowledge via statements of the form (&exist x)x : &phiv.The first chapter seeks to motivate the use of explicit modalities for reasoning about knowledge and informal provability relative to the tradition of epsitemic logic. The second chapter contains a consolidated treatment of the syntax and arithmetic and semantics of LP and QLP . A relational semantics for QLP is developed and several new results are presented (valid and invalid forms of explicit Barcan and converse Barcan formulas). The third chapter focuses on the reconstruction of the Knower Paradox in QLP. The central observation is that by analyzing the K(x) predicate employed by Montague and Kaplan in terms of proof quantification by replacing K( 4 ) with (&existx) : &phiv, we realize that an additional logic principle is required for the derivation of the Knower. This principle -- which is similar to a form of Universal Generalization for proofs anticipated by Godel [37] -- is examined both proof theoretically and through the use of an arithmetic semantics for QLP. The fourth chapter focuses on the reconstruction of the Knowability Paradox in QLP. The central observation is the so-called Knowability Principle on which the paradox is based -- i.e. the claim that if &phiv is true, then it is possible to know &phiv -- is most appropriately formulated via the use of proof quantifiers as (&existx)x : &phiv &rarr &phiv as opposed to the use of propositional possibility and knowledge operators.