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 obtained through the formalisation of Penrose’s second argument within the DTK system. It analyses two formulations of the first disjunct – one general and the other restricted – and dwells on the demonstration of the restricted version, showing that it yields the following result: if by F we denote the set of propositions derivable from any formalism and by K the set of mathematical propositions humanly knowable, then, given certain conditions, F necessarily differs from K. Thus it is possible that K surpasses F but also, on the contrary, that F surpasses K. In the latter case, however, the consistency of F is humanly undecidable.