Analysis of Penrose’s Second Argument Formalised in DTK System

This article aims to examine Koellner’s reconstruction of Penrose’s\r\nsecond argument a reconstruction that uses the DTK system to\r\ndeal with Gödel’s disjunction issues. Koellner states that Penrose’s argument\r\nis unsound, because it contains two illegitimate steps. He contends\r\nthat the formulas to which the T-intro and K-intro rules apply are both\r\nindeterminate. However, we intend to show that we can correctly interpret\r\nthe formulas on the set of arithmetic formulas, and that, as a consequence,\r\nthe two steps become legitimate. Nevertheless, the argument remains partially\r\ninconclusive. More precisely, the argument does not reach a result\r\nthat shows there is no formalism capable of deriving all the true arithmetic\r\npropositions known to man. Instead, it shows that, if such formalism exists,\r\nthere is at least one true non-arithmetic proposition known to the human\r\nmind that we cannot derive from the formalism in question. Finally, we\r\nreflect on the idealised character of the DTK system. These reflections\r\nhighlight the limits of human knowledge, and, at the same time, its irreducibility\r\nto computation.