TY - JOUR
T1 - A Note on Gödel’s First Disjunct Formalised in DTK System
AU - Corradini, Antonella
AU - Galvan, Sergio
PY - 2024
Y1 - 2024
N2 - 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.
AB - 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.
KW - Penrose’s second argument, Gödel’s disjunction, DT system, DTK system, computational model of mind, arguments in favour of the first horn of Gödel’s disjunction.
KW - Penrose’s second argument, Gödel’s disjunction, DT system, DTK system, computational model of mind, arguments in favour of the first horn of Gödel’s disjunction.
UR - http://hdl.handle.net/10807/297268
U2 - 10.12775/LLP.2024.025
DO - 10.12775/LLP.2024.025
M3 - Article
SN - 1425-3305
VL - 2024
SP - N/A-N//A
JO - Logic and Logical Philosophy
JF - Logic and Logical Philosophy
ER -