**Advisors:** Dominik Kirst and Holger Sturm

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).

- 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 .

- Slides from my initial talk
- Slides from my second talk
- Slides from my final talk
- A memo outlining the completeness proof for IEL
- A (draft) memo giving with an introduction to IEL
- Other memos (possibly in a draft state): Cut Elimination, Soundness of an embedding from IEL , a (small) memo about co-reflection