Core Gödel (Q6100981)

``This study aims to show how the core logician can furnish an adequate and natural formalization of the metalinguistic reasoning leading to Gödel's celebrated first incompleteness theorem[, which is] one of the most celebrated and intellectually important results in mathematical logic.'' Let (G1) denote Gödel's first incompleteness theorem, and (G2) denote the second incompleteness theorem of Gödel. Let us recall that {\em Ex Falso Quodlibet} (aka {\em Ex Contradictione Quodlibet}) says that every sentence is derivable from falsum (or contradiction); in symbols, \[\mathrm{EFQ}\,\frac{\bot}{\varphi}.\] ``Core logic \(\mathbb{C}\) is included within intuitionistic logic \(\mathbf{I}\) and is distinguished by its eschewal of ex falso quodlibet (EFQ). Likewise, classical core logic \(\mathbb{C}^+\) is included within classical logic \(\mathbf{C}\) and eschews EFQ. In any logic that contains it, the effect of EFQ is to make it the case that in any language governed by that logic there is only one inconsistent theory -- namely, the whole language itself. The main question of interest to the core logician is whether this feature is essential for the derivation of Gödel's celebrated incompleteness theorems. The main question splits into two. \begin{itemize} \item[(i)] Do we need to have inconsistent theories in the {\em object language} `exploding' via EFQ to the whole language, in order to derive (G1) and/or (G2)? \item[(ii)] Do we need to have inconsistent theories in the {\em metalanguage} `exploding' via EFQ to the whole language, in order to derive (G1) and/or (G2)? \end{itemize} ``Our answer to (i) is that all of the formal proofs furnished for the [prerequisite] lemmas on the way to the representability theorem have been core proofs. Representability is an entirely constructive result, and core logic suffices for constructive (intuitionistic) mathematics. ``The answer to the second question is negative: we do {\em not} need EFQ in our metalogic in order to derive (G1) and (G2) -- for the simple reason that one does not need EFQ in order to derive {\em any} mathematical theorem from a consistent set of mathematical axioms. If (G1) and (G2) enjoy constructive proofs, then they have core proofs. But if their proofs involve necessary recourse to strictly classical rules of inference (such as classical reductio ad absurdum, or dilemma), then they at least have classical core proofs. As it happens, (G1) and (G2) are constructively provable; hence core logic \(\mathbb{C}\) suffices for their proof at the metalevel. ``Opponents for whom the matter is not so directly disposed of, however, will try to raise difficulties for the core logician by making out that there are to be found, in the well-known proofs of the incompleteness theorems, what from their point of view appear to be indispensable appeals to EFQ. These appeals are either explicit, or, if merely implicit, nevertheless obvious. I agree that such appeals can be found; the crucial question for us to consider, however, is whether they are {\em indispensable}. They might have been made by formal logicians well versed in a tradition that has reconciled its followers to the use of EFQ, but which has failed to instruct them as to how its use can be avoided altogether. It is also important to be clear about whether the appeals to EFQ take place {\em at the metalogical level} or whether it is a matter of EFQ only being taken to be part of the logic of the object-language.''