On a Theorem by Bezboruah & Shepherdson

This paper defends the significance of Bezboruah and Shepherdson's incompleteness result regarding the weak theory ${\sf PA}^-$ against Kreisel's objections, compares it with Pudlák's extension of the Second Incompleteness Theorem, and provides a new proof based on sequence coding insights from Nielsen and Markov.

The Gist

Here is an explanation of Albert Visser's paper, "On a Theorem by Bezboruah & Shepherdson," translated into simple language with creative analogies.

The Big Picture: A Dispute Over a "Great Theorem"

Imagine the world of mathematics has a "Great Theorem" called the Second Incompleteness Theorem. This theorem is like a famous rule in a game: "If a rulebook is complex enough to describe itself, it cannot prove that it doesn't contain a contradiction."

For a long time, mathematicians thought this rule only applied to very complex, powerful rulebooks (like Peano Arithmetic). But in 1976, two mathematicians, Bezboruah and Shepherdson, tried to prove this rule applied even to a very simple, weak rulebook called Q (which is barely more than basic counting).

However, a famous critic named Georg Kreisel said, "Stop! This doesn't count."

Kreisel's argument was like this: "You can't say a simple rulebook 'expresses consistency' if the book is too weak to even prove that 2+2=4 in the right way. The sentence you wrote looks like 'I am consistent,' but in this weak book, it's just a meaningless string of symbols, like a child drawing a picture of a castle and calling it 'The Empire State Building.' It doesn't really mean anything."

Albert Visser (the author of this paper) says: "Kreisel is wrong. The symbols do mean something, even if the book is weak. Bezboruah and Shepherdson were right to publish their result, and it's actually a fascinating technical puzzle."

---

Part 1: The "Apologetic" Paper

Visser starts by looking at the original 1976 paper by Bezboruah and Shepherdson. He notes that they were so intimidated by Kreisel's criticism that they wrote their introduction sounding sorry for even trying. They admitted Kreisel's point might be right, but they said, "Hey, it's still a cool technical challenge to see if we can prove it anyway."

Visser argues that they shouldn't have apologized. He uses a simple analogy:

• The Analogy: Imagine you prove a math fact using a super-powerful computer (ZFC). Someone asks, "Can you prove this without using the 'Choice' button?" You say, "No, because without that button, the sentence means something totally different."
• Visser's Rebuttal: That sounds silly! The sentence "2+2=4" means the same thing whether you use a calculator or a super-computer. The meaning doesn't change just because the tool is weaker. So, Kreisel's objection that the meaning changes in a weak system doesn't hold water.

Part 2: Two Different Ways to Solve the Puzzle

Visser compares two different ways to prove that a weak system can't prove its own consistency.

1. The "Modern" Way (Pudlák): This is like using a high-tech drone to fly over a small village (the weak theory Q) and showing it's part of a bigger city (a stronger theory). If the city can't prove it's consistent, the village can't either. This is a very elegant, high-level approach.
2. The "Old School" Way (Bezboruah & Shepherdson): This is like building a physical model of the village out of LEGO bricks and manually showing that if you try to build a "proof of consistency," the bricks fall apart. It's messy, specific, and requires building a very strange, custom LEGO structure.

Visser says both methods are valid, but they are totally different tools. The "Old School" way is special because it doesn't rely on the high-tech drone; it works by building a specific, weird world where the proof fails.

Part 3: The New Proof (The "Markov Coding" Adventure)

The second half of Visser's paper is where he gets creative. He wants to prove the Bezboruah & Shepherdson result again, but using a different method.

The Metaphor: The Matrix Train
Instead of using the standard way of counting and listing numbers (which is like writing a list on a piece of paper), Visser uses a method based on Matrices (grids of numbers).

• The Setup: Imagine you have two special train cars, Car A and Car B.
  • Car A represents the sentence "If False, then False" (a tautology, or a true statement).
  • Car B represents "False" (a contradiction).
• The Goal: You want to build a train (a proof) that starts with a long string of Car A's and ends with a long string of Car B's. If you can build this train, you have proven a contradiction (that False is True).
• The Trick: Visser builds a "world" (a mathematical model) where this train looks like it exists, but it's actually broken.

How he breaks it:
He creates a world where the "train" is made of two parts glued together:

1. A long section of "True" cars.
2. A long section of "False" cars.

In a normal world, you would see the glue in the middle and say, "Hey, this isn't a valid proof because the rules changed in the middle!"
But Visser constructs a weird, non-standard world where the "glue" is invisible. In this world, the train looks like one continuous, valid proof of a contradiction.

The "Markov Coding" Secret:
To make this work, he uses a mathematical trick involving 2x2 grids of numbers (matrices) that act like a secret code for strings.

• Think of it like a Lego set where the pieces snap together in a very specific way.
• He shows that in his weird world, you can snap the "True" pieces and the "False" pieces together to make a "proof."
• However, if you look closely at the math, the "True" part is actually so huge (infinitely huge) that the "False" part gets lost in the noise. The world thinks it's a proof, but it's actually a glitch.

The Conclusion: Why This Matters

Visser concludes that:

1. Kreisel was wrong: Weak theories can express consistency, and we can prove they can't prove it.
2. The result is beautiful: It shows that even in the simplest math systems, there are "traps" where you can trick the system into thinking it has proven something impossible.
3. The new proof is cool: By using these matrix "trains" (Markov coding), Visser gave us a new, clearer way to visualize how these logical traps work. It's like taking a complex magic trick and showing the audience exactly how the hidden compartment works.

In a nutshell: The paper defends an old, slightly ignored mathematical result, argues that a famous critic was too harsh, and then offers a fresh, creative way to prove the result using a clever "matrix train" analogy. It's a celebration of the weird, counter-intuitive nature of logic.

Technical Summary

Here is a detailed technical summary of Albert Visser's paper, "On a Theorem by Bezboruah & Shepherdson."

1. Problem Statement

The paper addresses the validity and significance of the Second Incompleteness Theorem (G2) within very weak arithmetical theories, specifically Robinson's Q and $PA^-$ (the theory of the non-negative part of a discretely ordered commutative ring).

• The Core Conflict: In 1976, Bezboruah and Shepherdson ([BS76]) proved that $PA^-$ cannot prove the consistency of a specific weak theory (BeSh), implying $Q$ cannot prove its own consistency. However, Georg Kreisel argued that this result is "devoid of philosophical interest." Kreisel's objection was that in weak theories like $Q$, the standard consistency formula $con(Q)$ fails to express the actual notion of consistency because $Q$ cannot verify the necessary properties of the provability predicate (specifically the Hilbert-Bernays or Löb conditions).
• The Gap: While modern extensions of G2 (e.g., by Pudlák) show that theories interpreting $S^1_2$ cannot prove their own consistency, the specific case of $Q$ and $PA^-$ remained a subject of debate regarding whether the unprovability of consistency in these weak systems is a meaningful result or merely a technical artifact of weak arithmetization.

2. Methodology

Visser employs a multi-faceted methodological approach:

1. Philosophical Analysis: A critical examination of Kreisel's objection regarding "intensional correctness" and the meaning of consistency formulas in weak theories.
2. Comparative Logic: Contrasting the Bezboruah-Shepherdson (BS) result with Pavel Pudlák's modern extension of G2, which relies on interpretability and definable cuts.
3. Model Construction: Constructing specific non-standard models to demonstrate the existence of "fake" proofs of inconsistency.
4. Algebraic Coding: Utilizing a novel sequence coding based on the Markov coding technique (using the group $SL_2(\mathbb{Z})$) rather than the traditional $\beta$-function used in the original BS paper. This involves:
   • Mapping sequences to matrices in $SL_2(\mathbb{N})$.
   • Using properties of the free monoid and Tarski's "Editors Property" (cancellation laws) to define string operations.
   • Analyzing the growth rates of matrix entries via eigenvalues of specific matrices ($[n]$).

3. Key Contributions

A. Refutation of Kreisel's Objection

Visser argues that Kreisel's claim—that consistency formulas in weak theories lack meaning—is unsound.

• Argument: Meaning should not be relative to the theory in isolation. If a formula $con(Q)$ expresses consistency in a stronger theory (like Peano Arithmetic), it retains that meaning even when viewed from within $Q$. The inability of $Q$ to prove the consistency of $Q$ is a genuine limitation, not a semantic failure.
• Conclusion: The BS theorem is meaningful; the failure of $Q$ to prove its own consistency is a robust technical fact, not a philosophical void.

B. Comparison with Pudlák's Theorem

Visser clarifies the relationship between the BS result and Pudlák's modern G2:

• Pudlák's Result: Relies on the fact that $Q$ interprets $S^1_2$ on a definable cut. If $Q$ proved $con(Q)$, it would interpret $S^1_2 + con(Q)$, leading to inconsistency.
• Distinction: The BS result is not a consequence of Pudlák's theorem.
  • Scope: Pudlák's method cannot prove that $R$ (Robinson's arithmetic) does not prove $con(R)$ because $R$ does not interpret $S^1_2$. Conversely, BS methods cannot prove that $EA$ (Elementary Arithmetic) does not prove $con(EA)$.
  • Mechanism: BS relies on constructing a model with a specific "proof" of inconsistency that exists in the model but is not a valid proof in the standard sense (due to missing the transition point between axioms and conclusions). Pudlák relies on interpretability and $\Pi^0_1$-persistence.

C. New Proof via Markov Coding

Visser provides a new, independent proof of the BS theorem using Markov coding (based on $SL_2(\mathbb{Z})$) instead of the $\beta$-function.

• The Construction:
  • He constructs non-standard models $M$ and $N$ (where $N$ is an elementary end-extension of $M$).
  • He defines a matrix $\beta = [n]^a [m]^b$ where $a \in M \setminus N$ and $b \in N \setminus M$.
  • Using the properties of the sequence $s_{n,m}$ (related to Chebyshev polynomials and eigenvalues), he proves that the element $x_1$ (corresponding to the "switch" point in the proof sequence) is not in the generated submodel $K$.
• The Result: In the model $K$, the sequence $\beta$ appears to be a valid Hilbert-style proof of $\bot$ (falsum) because the "cut" where the axioms end and the conclusion begins is missing from the model's perspective. Thus, $K \models \neg con(BeSh)$.
• Significance: This proves that $PA^-$ (plus true universal sentences) does not prove $con(BeSh)$, and consequently, $Q$ does not prove $con(Q)$ under Markov coding.

4. Key Results

1. Theorem 3.5 (Re-stated): Under $\beta$-function coding, $PA^-$ does not prove the consistency of the weak theory BeSh. Consequently, $Q$ does not prove $con(Q)$.
2. Theorem 4.1 (New): Under Markov coding, $PA^-$ (augmented with all true universal sentences) does not prove the consistency of BeSh.
3. Theorem 3.4 (Pudlák): If a c.e. theory $U$ interprets $Q + con(U)$, then $U$ is inconsistent.
4. Open Question 3.6: Whether the Bezboruah-Shepherdson model satisfies all true universal sentences (Visser suggests it likely does not, but the model is rich enough to contain true universal sentences).
5. Open Question 3.7: Whether elements can be "adjoined" to the Bezboruah-Shepherdson inconsistency proof to extend it further within the model.

5. Significance

• Restoration of a Neglected Result: The paper rescues the Bezboruah-Shepherdson theorem from unjustified neglect caused by Kreisel's influential criticism, demonstrating its technical depth and philosophical relevance.
• Clarification of G2 Variants: It establishes that there are distinct "flavors" of the Second Incompleteness Theorem. The "Interpretability" version (Pudlák) and the "Model-Theoretic/Sequence Coding" version (Bezboruah-Shepherdson) are complementary but not reducible to one another.
• Technical Innovation: The introduction of Markov coding ($SL_2(\mathbb{Z})$) for sequence encoding in weak arithmetic provides a new tool for metamathematics. It avoids the complexities of the $\beta$-function and offers a fresh perspective on how sequence properties interact with weak theories like $PA^-$.
• Didactic Value: The construction of models where "inconsistency proofs" exist but are structurally flawed (missing the transition point) provides a clear visualization of the difference between universal sentences and $\Pi^0_1$ sentences, and the limits of weak theories in verifying their own consistency.

In summary, Visser validates the Bezboruah-Shepherdson theorem as a significant, independent result in the landscape of incompleteness, refutes the philosophical objections against it, and modernizes the proof using algebraic coding techniques.