The Atheism of the Gaps

First Things ^ | Stephen M. Barr

[The_Reader_David]

I have read through the review article you posted (are you the author, perchance?). It does not in fact address my argument. In more detail I argue as follows: A consistently reasoning mathematician (CRM) who has a mental representation of the Peano postulates provides a construction, which applied to any sound formal system containing a logical equivalent of the Peano postulates will yield that a Goedel statement for that system.

Now, let us suppose that the CRM is computationally equivalent to some formal system. The construction he has provided applies to that formal system. Thus, the construction provided by the CRM proves the Goedel statement for this formal system by specialization. Observe, that specializing from the universally quantified statement does not require identifying which formal system the CRM is equivalent to, only that one exists.

Now, I will freely admit that if one accepts a constructivist philosophy of mathematics, my argument is invalid. (Of course, binding one's reasoning within the strictures of constructivism itself goes a long way to making one imitate a Turing machine.) However, if one accepts classical mathematical reasoning in which it is not necessary to exhibit a thing to show its existence, I think you are left with exactly four possibilities:

• There is no such thing as a CRM with a mental representation of the Peano postulates capable of providing a general construction for Goedel statements of sound formal systems which contain a logical equivalent of the Peano postulates.
• A CRM with a mental representation of the Peano postulates capable of providing a general construction for Goedel statements is somehow computationally equivalent to a sound formal system which does not contain a logical equivalent of the Peano postulates.
• Impredicative quantification over sound formal systems which contain a logical equivalent of the Peano postulates by itself leads to a contradiction. OR
• The assumption that the CRM with a mental representation of the Peano postulates is computationally equivalent to a formal system (or equivalently to a Turing machine) is false.

I find the first three implausible, though I would find a proof of the third intriging if you could provide it. Thus, absent a proof of the third, I hold that this demonstrates the validity of Penrose's original argument.

[sourcery]

Epistemological Constructivism

Introduction to Pancritical Rationalism

I am a Radical Constructivist and a pan-critical rationalist. So of course I think your argument is invalid on its face.

But let me present yet another argument against the dualist thesis:

Godels 1931 paper, "On formally undecidable propostions of Principia Mathematica and related systems" is a formal mathematical proof. Therefore, it is a sequence of statements within a formal axiomatic system known as mathematical logic. Mathematical logic is isomorphic to a formal system that conforms to the Peano axioms. Therefore, one of the following statements must be true with respect to Godel's proof:

1. Godel's Proof represents an existence proof that a formal system subject to Godel's Incompleteness Theorem is competent to prove Godel's Incompleteness Theorem. If so, then the materialists are correct and the dualists are wrong (with respect to the proposition that a human mind is necessarily superior to any Turing machine).
2. Godel's Proof is not a valid proof. If so, then this whole discussion is meaningless.
3. Godel's Proof is actually informal (i.e., it is not a formal proof). Therefore, it is not necessarily the case that it is in a formal system that is itself subject to the Incompleteness Theorem. If so, it is also not necessarily the case that the "proof" is valid: only formal proofs have "unassailable" validity (actually, even formal proofs are only valid in the absolute sense if the formal system to which they belong is also valid in the absolute sense). I assert that either Godel's proof is formal, or else it is not a proof.
4. Godel's Proof is in a formal system that is not subject to the Incompleteness Theorem. I assert this is false, because Godel's Proof is itself based on arithmetic (e.g., the proof relies on a bidirectional isomorphic mapping of metamathematical statements into arithmetic formulae), and arithmetic is the nominal subject of the Incompleteness Theorem!

The Laws of Form

[The_Reader_David]

I will have to consider further the content of your most recent reply. (Though since you are a radical constructivist, we may just be talking at cross purposes, since I am a mathematical Platonist, abeit one with a perference for constructive or intuitionistc proofs when these are available.)

After retiring last night, however, I realized that there is a gap in the argumentation presented in the review article:

|-A implies |-B(A) is an unwarranted assumption. In particular if there were a sound formal system which captured your computational ability, but contained a logical equivalent of ZFC, you would provide a model of |- axiom of choice & |- B(axiom of choice). (I assume here you are of the school of contructivism which rejects AC. If not, substitute Brouwer, the original intuitionist,for yourself.) Belief does not necessarily follow from the existence of a non-subjectively-experienced "axiom" or formally proved statement--a hypothesized formal system which captures your computational power need not be made of propositions and rules of inference supporting a semantics you would consciously accept.