This course will study epistemic extensions of theories of formal arithmetic. We will begin by establishing the necessary background in formal theories of arithmetic (such as Peano arithmetic) and Godel's incompleteness theorems. Following this, we will explore extensions of Peano arithmetic that incorporate an operator that is intended to represent the knowledge of an (ideal) mathematician. We will discuss the so-called Knower Paradox that results when the knowledge operator is treated as a predicate, including an extensive discussion of variants of the paradox and the proposed solutions to the paradox. Finally, we will discuss attempts to formalize Godel's disjunction: either there is no algorithm that can capture human mathematical reasoning or there are absolutely undecidable problems. In addition to discussing absolute undecidability, we will also present Feferman's formal theory of truth with a determinate operator. Topics that will be discussed in the course include:
This course offers an excellent opportunity to introduce ESSLLI students to one of the most significant topics in mathematical logic: Gödel's incompleteness theorems. Due to the complexity and depth of these theorems, it is not feasible to cover all aspects, such as Gödel coding and the necessary background in computability theory, within a week. The main objective is to help students begin to grasp the incompleteness theorems and their implications without becoming overwhelmed by the details.