The Trans-Existential Grounding Framework Notes and Explainers

Gödel's theorems, symbol by symbol

Gödel’s Incompleteness Theorems: Complete Symbol-by-Symbol Walkthrough

This note walks through Gödel’s two theorems symbol by symbol. The last part shows how the paper Why Existence Cannot Ground Itself uses the second one.

The proof sketches are simplified. The full proof of the first theorem needs a little more than consistency (ω-consistency, or Rosser’s trick), which a sketch can leave out.


Gödel’s First Incompleteness Theorem

Statement

Let T be a consistent formal system containing elementary arithmetic. Then there exists a sentence G in the language of T such that:
    T ⊬ G  and  T ⊬ ¬G
That is, G is undecidable in T.

Symbol by symbol:

Symbol Meaning
T A formal system (set of axioms + inference rules)
consistent T never proves both P and ¬P for any statement P
formal system A system where proofs are mechanical symbol manipulation
containing elementary arithmetic T can express basic number theory (addition, multiplication, 0, 1, successor)
G The Gödel sentence (constructed below)
⊬ “does not prove” – there’s no valid proof of this in T
¬G “not G” – the negation of G
undecidable Neither provable nor refutable within T

Plain English:

Any consistent system powerful enough to do basic arithmetic contains a true statement that the system cannot prove.


Proof Sketch Step 1

Construct a formula Prov_T(x) expressing "x is provable in T"

What this means:

Gödel showed you can encode the concept “there exists a proof of x in T” as an arithmetic formula. This is possible because:

So Prov_T(x) is a formula in the language of arithmetic that, when given a number, returns true if that number encodes a provable statement.


Proof Sketch Step 2

Use diagonal lemma to construct sentence G such that:
    G ↔ ¬Prov_T(⌜G⌝)
where ⌜G⌝ is the Gödel number of G

Symbol by symbol:

Symbol Meaning
diagonal lemma A technical lemma allowing self-reference
G The sentence being constructed
↔︎ “if and only if” – logical equivalence
¬ “not” – negation
Prov_T(...) “… is provable in T”
⌜G⌝ The Gödel number of G (the numeric code for the sentence G)

What this means:

The diagonal lemma (also called the fixed-point lemma) says: for any formula φ(x), we can construct a sentence S such that S ↔︎ φ(⌜S⌝).

Applied here: We want a sentence that “talks about itself.” We use φ(x) = ¬Prov_T(x), and get:

G ↔︎ ¬Prov_T(⌜G⌝)

The corner brackets ⌜ ⌝: These denote the Gödel number – a way of encoding any formula as a unique natural number. Every symbol gets a number, every sequence of symbols gets a number computed from its parts.


Proof Sketch Step 3

G effectively states "G is not provable in T"

This is the self-referential magic. The sentence G is equivalent to “the sentence with Gödel number ⌜G⌝ is not provable in T.” But ⌜G⌝ IS the Gödel number of G itself. So G says “I am not provable.”

This is the mathematical version of the Liar’s Paradox, but about provability instead of truth.


Proof Sketch Step 4

If T ⊢ G, then T ⊢ Prov_T(⌜G⌝), so T ⊢ ¬G (contradiction)

Symbol by symbol:

Symbol Meaning
T ⊢ G “T proves G”
T ⊢ Prov_T(⌜G⌝) “T proves that G is provable”
T ⊢ ¬G “T proves not-G”

The reasoning:

  1. Assume T proves G (T ⊢ G)
  2. If T proves something, then “T proves it” is true and can be verified arithmetically
  3. So T can prove Prov_T(⌜G⌝) – i.e., T proves “G is provable”
  4. But G says “G is NOT provable” (G ↔︎ ¬Prov_T(⌜G⌝))
  5. So Prov_T(⌜G⌝) is equivalent to ¬G
  6. Therefore T ⊢ ¬G
  7. But we assumed T ⊢ G, so T proves both G and ¬G
  8. This contradicts T being consistent

Conclusion: T cannot prove G.


Proof Sketch Step 5

If T ⊢ ¬G, then T ⊢ Prov_T(⌜G⌝), but then T proves both G and ¬G (inconsistent)

The reasoning:

  1. Assume T proves ¬G (T ⊢ ¬G)
  2. Since G ↔︎ ¬Prov_T(⌜G⌝), we have ¬G ↔︎ Prov_T(⌜G⌝)
  3. So T ⊢ Prov_T(⌜G⌝) – T proves “G is provable”
  4. If T is sound (proves only true things), then G actually IS provable
  5. But we’re assuming T ⊢ ¬G, which says G is NOT provable
  6. Contradiction

Note: This step technically requires ω-consistency or soundness. The sketch simplifies this, which is acceptable for exposition.


Proof Sketch Step 6

Therefore: T ⊬ G and T ⊬ ¬G

Neither proving G nor proving ¬G is possible without contradiction. So G is undecidable in T.

Yet G is true (from outside the system, we can see that G really is not provable in T, which is exactly what G claims).


Gödel’s Second Incompleteness Theorem

Statement

Let T be a consistent formal system containing elementary arithmetic. Then:
    T ⊬ Con(T)
where Con(T) expresses the consistency of T.

Symbol by symbol:

Symbol Meaning
Con(T) An arithmetic formula expressing “T is consistent”
T ⊬ Con(T) T cannot prove its own consistency

Plain English:

A consistent system cannot prove it is consistent.


Proof Sketch Step 1

Define Con(T) ≡ ¬Prov_T(⌜0 = 1⌝)

What this means:

“T is consistent” means “T doesn’t prove a contradiction.” We can express this as “T doesn’t prove 0 = 1” (since 0 = 1 is a canonical false statement, and proving it would let you prove anything).

Symbol Meaning
≡ “is defined as”
⌜0 = 1⌝ The Gödel number of the statement “0 = 1”
¬Prov_T(⌜0 = 1⌝) “The statement 0=1 is not provable in T”

Proof Sketch Step 2

Show that T ⊢ (Con(T) → G) where G is the Gödel sentence

What this means:

Within T, you can prove: “If T is consistent, then G is true.”

Why? The First Theorem proof shows: If T ⊢ G, then T is inconsistent. The contrapositive: If T is consistent, then T ⊬ G. And G says “G is not provable in T.” So if T is consistent, then G is true.

This implication can be formalized and proven inside T itself.


Proof Sketch Step 3

If T ⊢ Con(T), then T ⊢ G

Simple modus ponens:


Proof Sketch Step 4

But First Theorem shows T ⊬ G for consistent T

We already proved T cannot prove G without becoming inconsistent.


Proof Sketch Step 5

Therefore: T ⊬ Con(T)

If T could prove Con(T), then T could prove G (by steps 2-3). But T can’t prove G (step 4). Therefore T can’t prove Con(T).

The devastating conclusion: Any system powerful enough to do arithmetic, if consistent, cannot prove its own consistency. Self-validation is impossible.


How the Grounding paper uses this

The paper does not claim that Gödel alone proves a ground outside existence. It uses his second theorem on formal systems inside existence: the laws of physics, written out.

The ladder

T ⊬ Con(T),   T + Con(T) ⊢ Con(T),   T + Con(T) ⊬ Con(T + Con(T)),   …

A consistent system with arithmetic cannot prove its own consistency. A stronger system can prove it, and then its own consistency is open. Taken whole, the ladder is again such a system, or it is no formal system at all. The paper states this as Theorem 1.

The premise

The step from “no system proves it” to “the account lies outside existence” is no part of Gödel. It uses one premise: whatever is one way and not another must have an account. There are no brute facts.

Given the premise, the consistency of the laws needs an account. No formal system gives it, and an endless chain of certificates, taken whole, is a brute fact. So the account lies outside existence. The paper states this as Theorem 2.

One road of three

Gödel is the road that is proved. Two more roads reach the same fork without him: the chain of properties, and the question why asked again and again. Doubt that Gödel applies to the world, and two roads remain. Deny the premise, and all three fall.


Key Symbols Quick Reference

Symbol Name Meaning
T Theory A formal system
⊢ Turnstile “proves”
⊬ Negated turnstile “does not prove”
¬ Negation “not”
↔︎ Biconditional “if and only if”
→ Implication “if… then”
∃ Existential quantifier “there exists”
∀ Universal quantifier “for all”
∩ Intersection “and” for sets
∅ Empty set Nothing
⊆ Subset “is contained in”
⌜ ⌝ Corner quotes Gödel number of
Prov_T(x) Provability predicate “x is provable in T”
Con(T) Consistency statement “T is consistent”
G Gödel sentence Self-referential undecidable statement
E Existence All that is
P Pure potential Trans-existential domain
W Free Will Creative ground
α Alpha Actualization function

The Bottom Line

Gödel proved that a consistent system strong enough for arithmetic cannot prove its own consistency. That much is mathematics, and nobody can attack it.

That existence needs a ground outside itself follows from it given one premise: there are no brute facts. Whoever accepts brute facts has a way out, and the paper names that as the place to attack it.