Registry · Theorem VII.T07 tau-effective formalized

VII.T07 — Gödel Avoidance Theorem

τ satisfies no internal sentence G with G ↔ ¬Coh_D(G); incompleteness phenomenon does not arise; bounded witness excludes diagonal construction.

Book VII Part 1 Ch. 9

Dependency Graph

Depends on (2)

VII.D15 VII.P04

Lean Formalization

Module: TauLib.BookVII.Meta.Registers

Symbol: Tau.BookVII.Meta.Registers.GdelAvoidanceTheorem