A Note on Gödel’s First Disjunct Formalised in DTK System

This note clarifies the significance of the proof of Gödel’s first disjunct\r\nobtained through the formalisation of Penrose’s second argument within\r\nthe DTK system. It analyses two formulations of the first disjunct –\r\none general and the other restricted – and dwells on the demonstration\r\nof the restricted version, showing that it yields the following result: if by\r\nF we denote the set of propositions derivable from any formalism and by\r\nK the set of mathematical propositions humanly knowable, then, given\r\ncertain conditions, F necessarily differs from K. Thus it is possible that\r\nK surpasses F but also, on the contrary, that F surpasses K. In the latter\r\ncase, however, the consistency of F is humanly undecidable.