... structures.¹

Gödel I has of course given rise to a rather well-known question with which I'm not concerned herein, viz.,

Q2

Do the mathematical facts revealed by Gödel I imply that people have an ability that can never be matched by machines?

Rather a lot of ink has been devoted to Q2 of late (some of it flowing from my own pen). Roger Penrose [11] [12], for example, has famously argued that Q2 should be answered in the affirmative. Though I've been elsewhere concerned with Q2 (the bulk of my own writing on Q2 can be found in the chapter ``Gödel" in [7]), this question is not my concern in the present paper. I'm not concerned here with whether Gödel I itself implies that minds aren't machines; I'm concerned herein, if you will, with whether the human model-based reasoning that goes into proving Gödel I is beyond computation.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... proof.²

Note as well that I don't focus on Gödel's own original proof of his first incompleteness theorem. Such a focus would entirely preclude the accessibility of this essay.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... function.³

To ease exposition, I ignore the fact that father-of isn't really a function.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... transparent.⁴

The tables used here are pulled from [2].

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... connection:⁵

The following scheme is adapted from [16].

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... -p)).⁶

Notice that since OTTER takes input from an ordinary keyboard, the negation symbol $\neg$ becomes -, $\rightarrow$ becomes ->, $\vee$ becomes |, etc.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... code.⁷

When pondering the following table, and the OTTER code that makes use of it, keep in mind that T(c( $O[\phi],O[\psi]$)) -- which essentially says that the biconditional $\phi \leftrightarrow \psi$ is a theorem of first-order logic -- is represented in OTTER as a conjunction of the two conditionals that make up the biconditional, viz., T(i( $O[\phi],O[\psi]$))& T(i( $O[\psi],O[\phi]$)).

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... of⁸

The part of the theorem that says that if n(x) is a theorem of K4 then a contradiction ensues is the missing part.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... formula.⁹

Also, for cognoscenti: I've compressed the proof by among other things omitting declarative representation of the interconnection between the functor c for the biconditional and the functor i for the conditional.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.