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

Antonella Corradini*, Sergio Galvan

*Corresponding author

Research output: Contribution to journalArticlepeer-review

Abstract

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.
Original languageEnglish
Pages (from-to)N/A-N//A
Number of pages11
JournalLogic and Logical Philosophy
Volume2024
DOIs
Publication statusPublished - 2024

Keywords

  • 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.

Fingerprint

Dive into the research topics of 'A Note on Gödel’s First Disjunct Formalised in DTK System'. Together they form a unique fingerprint.

Cite this