Christian Hagemeier: Bachelor’s Thesis
Intuitonistic Epistemic Logic in Coq
Advisors: Dominik Kirst and Holger Sturm
Abstract
The relationship between knowledge and truth seems to be settled: Only
truths can be known, therefore knowledge entails truth. This so-called
truth condition is the most seldom contested principle about knowledge
and is therefore also reflected in most epistemic logics, classical or
intuitionistic: The principle K A ⊃ A (read as if A is known, it is
true) is endorsed, while A ⊃ K A is rejected as it seems unreasonable to
conclude that an agent has knowledge of a proposition just because it is
true.
In their seminal paper , Artemov and Protopopescu (2016) propose that a
truly intuitionistic account of knowledge should endorse A ⊃ K A (read
as if A is proven it is known), relying on the constructive reading of
truth as provability. Nevertheless, this does not amount to rejecting
the usual truth condition (K A ⊃ A) completely, as other classically
,but not intuitionistically, equivalent alternatives (e.g. K A ⊃ ¬¬A) to
the classical truth condition can be adopted.
While there is flourishing literature on IEL, so far no attempts have
been made to analyze results about IEL in a constructive setting.
Elaborating on the classical completeness proof, we present the a
constructive proof of quasi-completeness for IEL, which we have
mechanized in the Coq proof assistant. Our second result is a
constructive decidability proof using a proof-search in a cut-free
sequent calculus. We generalize our method of proving cut-elimination
and decidability to the classical modal logic K. We believe that this
method of proving cut-elimination proofs is applicable to an even larger
class of modal logics. With the decidability result we obtain a
constructive proof of finitary completeness for IEL.
Lastly, we discuss two well known epistemic paradoxes and their
connection to IEL. Here we focus on the Church-Fitch paradox of
knowability (Fitch 1963) and Florio’s and Murzi’s paradox of
Idealization Florio and Murzi (2009).
Thesis
- My thesis can be found here (submitted: 12th July 2021).
- The coq development can be found on GitHub or downloaded as a zip file (Coq 8.13.2).
- The CoqDoc can be found here .
Memos and milestones
Legal notice, Privacy policy
