structure SelfReference.TMDescription (Γ : Type) : Type 1

A self-contained description of a Turing machine over the tape alphabet Γ. Bundles the (existential) state type Q, its DecidableEq instance, the underlying TM, and an optional explicit source/encoding source : List Γ used by certain concrete encodings.

• Q : Type
• decEq : DecidableEq self.Q
• machine : TuringMachine.TM self.Q Γ
• source : List Γ

def SelfReference.TMDescription.lang {Γ : Type} (d : TMDescription Γ) : Set (List Γ)

The language L(d) recognized by the Turing machine packaged inside d.

def SelfReference.TMDescription.haltsWithOutput {Γ : Type} (M : TMDescription Γ) (w out : List Γ) : Prop

M.haltsWithOutput w out says that running M.machine on input w reaches a halt configuration after some number of steps n, and at that point the first out.length cells of the tape spell out out. This is the "halt with out on the tape" predicate used to formalize the printing/output behavior of TMs.

structure SelfReference.TMEncoding (Γ : Type) : Type 1

A TMEncoding packages the data Sipser uses to set up the self-reproducing TM construction:

• encode : turns a TM description into its string code ⟨M⟩;
• printTMDesc w : the "printer" machine P_w that on any input halts with w on the tape (printTMDesc_spec);
• q_computable : the function q(w) = ⟨P_w⟩ is computable. This is the formal counterpart of the textbook Lemma giving the computable function q : Σ* → Σ* with q(w) = ⟨P_w⟩.

• encode : TMDescription Γ → List Γ
• printTMDesc : List Γ → TMDescription Γ
• printTMDesc_spec (w input : List Γ) : (self.printTMDesc w).haltsWithOutput input w
• q_computable : TuringMachine.IsComputableFunction fun (w : List Γ) => self.encode (self.printTMDesc w)

def SelfReference.IsMinimalTM {Γ : Type} (enc : TMEncoding Γ) (d : TMDescription Γ) : Prop

IsMinimalTM enc d says d is a minimal Turing machine for its language under the encoding enc: no strictly shorter description d' recognizes the same language. Formally, for every d', |⟨d'⟩| < |⟨d⟩| implies L(d') ≠ L(d).

def SelfReference.MIN_TM {Γ : Type} (enc : TMEncoding Γ) : Set (List Γ)

MIN_TM = {⟨M⟩ | M is a minimal TM}: the set of codes of minimal Turing machines under the encoding enc. This is the language whose Turing-unrecognizability is shown via the Recursion Theorem.

structure SelfReference.SelfRefFramework (Γ : Type) : Type 1

The data needed to build Sipser's self-reproducing TM SELF. Bundles:

• an encoding encode : TMDescription → List Γ;
• the printer-machine constructor printTM together with its halting spec;
• a sequential compose operator that runs A then B (output of A becomes input of B) and whose code is some concatenation combineDesc (encode A) (encode B);
• a "quine helper" quineB that on input input halts with ⟨P_input⟩ ⟨quineB⟩ on the tape. This is exactly the structure used in the proof that some TM SELF prints its own description on every input.

• encode : TMDescription Γ → List Γ
• printTM : List Γ → TMDescription Γ
• printTM_spec (w input : List Γ) : (self.printTM w).haltsWithOutput input w
• compose : TMDescription Γ → TMDescription Γ → TMDescription Γ
• compose_spec (A B : TMDescription Γ) (w mid out : List Γ) : A.haltsWithOutput w mid → B.haltsWithOutput mid out → (self.compose A B).haltsWithOutput w out
• combineDesc : List Γ → List Γ → List Γ
• encode_compose (A B : TMDescription Γ) : self.encode (self.compose A B) = self.combineDesc (self.encode A) (self.encode B)
• quineB : TMDescription Γ
• quineB_spec (input : List Γ) : self.quineB.haltsWithOutput input (self.combineDesc (self.encode (self.printTM input)) (self.encode self.quineB))

def SelfReference.SelfRefFramework.q {Γ : Type} (F : SelfRefFramework Γ) (w : List Γ) : List Γ

The computable map q(w) := ⟨P_w⟩ inside a SelfRefFramework: it sends a string w to the code of the printer-machine that outputs w.

structure SelfReference.SelfRefFrameworkExt (Γ : Type) extends SelfReference.SelfRefFramework Γ : Type 1

An extension of SelfRefFramework exposing a concrete second-stage machine machineB whose halting spec is stated directly in terms of the framework's function q, matching the textbook construction B(input) = ⟨P_q(input)⟩ ⟨machineB⟩.

• encode : TMDescription Γ → List Γ
• printTM : List Γ → TMDescription Γ
• printTM_spec (w input : List Γ) : (self.printTM w).haltsWithOutput input w
• compose : TMDescription Γ → TMDescription Γ → TMDescription Γ
• compose_spec (A B : TMDescription Γ) (w mid out : List Γ) : A.haltsWithOutput w mid → B.haltsWithOutput mid out → (self.compose A B).haltsWithOutput w out
• combineDesc : List Γ → List Γ → List Γ
• encode_compose (A B : TMDescription Γ) : self.encode (self.compose A B) = self.combineDesc (self.encode A) (self.encode B)
• quineB : TMDescription Γ
• quineB_spec (input : List Γ) : self.quineB.haltsWithOutput input (self.combineDesc (self.encode (self.printTM input)) (self.encode self.quineB))
• machineB : TMDescription Γ
• machineB_spec (input : List Γ) : self.machineB.haltsWithOutput input (self.combineDesc (self.q input) (self.encode self.machineB))

theorem SelfReference.exists_self_reproducing_tm {Γ : Type} (F : SelfRefFramework Γ) : ∃ (M : TMDescription Γ), ∀ (w : List Γ), M.haltsWithOutput w (F.encode M)

Self-Reproducing TM (Sipser, Lecture 11). Given a SelfRefFramework F, there exists a TM SELF such that on every input w, SELF halts with ⟨SELF⟩ on the tape. The witness is SELF := compose (printTM ⟨quineB⟩) quineB.

structure SelfReference.TapeOutputFixedPoint {Γ : Type} (encode : TMDescription Γ → List Γ) : Type 1

A "tape-output" fixed-point witness: a TM fixedTM whose output on input is g input ⟨fixedTM⟩. This packages the self-referential ability to depend on one's own code at the tape level, parameterized by an external two-argument map g.

• g : List Γ → List Γ → List Γ
• fixedTM : TMDescription Γ
• fixedTM_spec (input : List Γ) : self.fixedTM.haltsWithOutput input (self.g input (encode self.fixedTM))

structure TuringMachine.TMCoding (Γ : Type) : Type 1

An abstract acceptable indexing ("coding") of Turing machines over alphabet Γ, sufficient to formalize the Recursion / Fixed-point theorems and the MIN_TM unrecognizability proof. It records:

• an index type TMIndex with an encode/decode pair and language assignment;
• a pairing function pair on strings;
• an smn function with the standard s-m-n specification;
• a notion IsComputable of computable index transformations, closed under the needed operations (composition, applying smn, and the diagonal x ↦ smn x x);
• representable: every computable h : TMIndex → TMIndex is "implemented" by some index e₀, i.e. languageOf (smn e₀ x) = languageOf (h x);
• languages_beyond_length: arbitrarily long codes are needed to span all languages — there exist indices whose language differs from all shorter ones;
• recognizable_enumSearch_computable: a recognizable set of codes plus an enumeration witness t that strictly increases code-length yields a computable t.

• TMIndex : Type
• encode : self.TMIndex → List Γ
• languageOf : self.TMIndex → Set (List Γ)
• decode : List Γ → Option self.TMIndex
• decode_encode (M : self.TMIndex) : self.decode (self.encode M) = some M
• pair : List Γ → List Γ → List Γ
• pair_injective (a b c d : List Γ) : self.pair a b = self.pair c d → a = c ∧ b = d
• smn : self.TMIndex → self.TMIndex → self.TMIndex
• smn_spec (e x : self.TMIndex) (w : List Γ) : w ∈ self.languageOf (self.smn e x) ↔ self.pair w (self.encode x) ∈ self.languageOf e
• IsComputable : (self.TMIndex → self.TMIndex) → Prop
• representable (h : self.TMIndex → self.TMIndex) : self.IsComputable h → ∃ (e : self.TMIndex), ∀ (x : self.TMIndex), self.languageOf (self.smn e x) = self.languageOf (h x)
• isComputable_smn_diag : self.IsComputable fun (x : self.TMIndex) => self.smn x x
• isComputable_comp (f g : self.TMIndex → self.TMIndex) : self.IsComputable f → self.IsComputable g → self.IsComputable (f ∘ g)
• isComputable_smn_apply (e : self.TMIndex) : self.IsComputable (self.smn e)
• languages_beyond_length (n : ℕ) : ∃ (M : self.TMIndex), ∀ (M' : self.TMIndex), (self.encode M').length < n → self.languageOf M' ≠ self.languageOf M
• recognizable_enumSearch_computable (P : self.TMIndex → Prop) : IsTuringRecognizable {s : List Γ | ∃ (M : self.TMIndex), self.encode M = s ∧ P M} → ∀ (t : self.TMIndex → self.TMIndex), (∀ (M : self.TMIndex), P (t M) ∧ (self.encode M).length < (self.encode (t M)).length) → self.IsComputable t

theorem TuringMachine.recursion_theorem {Γ : Type} (C : TMCoding Γ) (t : C.TMIndex → C.TMIndex) (ht : C.IsComputable t) : ∃ (R : C.TMIndex), C.languageOf R = C.languageOf (t R)

Recursion Theorem (language form). For any computable transformation t : TMIndex → TMIndex of TM indices, there exists R whose language equals the language of t R. This is the language-level avatar of Sipser's statement that for any TM T there is a TM R such that R on w behaves like T on ⟨w, R⟩.

theorem TuringMachine.fixed_point_theorem {Γ : Type} (C : TMCoding Γ) (f : List Γ → List Γ) (_hf : IsComputableFunction f) (hf_maps_to_valid : ∀ (M : C.TMIndex), ∃ (S : C.TMIndex), C.decode (f (C.encode M)) = some S) (ht_computable : ∀ (t : C.TMIndex → C.TMIndex), (∀ (M : C.TMIndex), C.decode (f (C.encode M)) = some (t M)) → C.IsComputable t) : ∃ (R : C.TMIndex) (S : C.TMIndex), C.decode (f (C.encode R)) = some S ∧ C.languageOf R = C.languageOf S

Fixed-point Theorem (Sipser, Lecture 11, Ex 2). For any computable function f : Σ* → Σ* (with codomain landing in valid encodings), there is a TM R and a TM S with f(⟨R⟩) = ⟨S⟩ and L(R) = L(S). In other words, every computable transformation on TM descriptions has a "fixed point" up to language equality.

def TuringMachine.PrintsAndHalts {Γ Q : Type} [DecidableEq Q] (M : TM Q Γ) (w : List Γ) : Prop

PrintsAndHalts M w says: started on the empty tape, M reaches an accept configuration after some n steps, with cells 0, …, |w|-1 holding the symbols of w and everywhere else the blank symbol. Captures "M halts having printed exactly w".

def TuringMachine.PrintsAndHaltsOnInput {Γ Q : Type} [DecidableEq Q] (M : TM Q Γ) (input w : List Γ) : Prop

Same as PrintsAndHalts but starting from an arbitrary input instead of the blank tape: after some n steps M accepts and the first |w| tape cells contain w.

noncomputable def TuringMachine.printTM {Γ : Type} (blank : Γ) (inputAlpha : Set Γ) (h_blank : blank ∉ inputAlpha) (w : List Γ) : TM (Fin (w.length + 2)) Γ

The concrete printer-machine P_w for a string w: a TM with |w| + 2 states (one per character, plus an accept and a reject state) that on any input writes w[0], w[1], …, w[|w|-1] left-to-right and accepts. This is the explicit construction underlying the computable function q(w) = ⟨P_w⟩.

theorem TuringMachine.printTM_invariant_any_input {Γ : Type} [DecidableEq Γ] (blank : Γ) (inputAlpha : Set Γ) (h_blank : blank ∉ inputAlpha) (w input : List Γ) (k : ℕ) (hk : k ≤ w.length) : ((printTM blank inputAlpha h_blank w).runOnInput input k).state = ⟨k, ⋯⟩ ∧ ((printTM blank inputAlpha h_blank w).runOnInput input k).headPos = ↑k ∧ ∀ (j : ℕ) (hj : j < k), ((printTM blank inputAlpha h_blank w).runOnInput input k).tape ↑j = w[j]

Key loop invariant of printTM: after k ≤ |w| steps on any input, the machine is in state k, the head is at position k, and tape cells 0, …, k-1 already hold the first k symbols of w. Proved by induction on k.

theorem TuringMachine.printTM_haltsWithOutput {Γ : Type} [DecidableEq Γ] (blank : Γ) (inputAlpha : Set Γ) (h_blank : blank ∉ inputAlpha) (w input : List Γ) : ∃ (n : ℕ), (printTM blank inputAlpha h_blank w).isHaltConfig ((printTM blank inputAlpha h_blank w).runOnInput input n) ∧ ((printTM blank inputAlpha h_blank w).runOnInput input n).readTape w.length = w

Correctness of printTM: on any input, after exactly |w| steps the printer machine P_w halts (in fact accepts) and the first |w| tape cells (read off by Config.readTape) spell out w. This realizes the haltsWithOutput spec demanded by TMEncoding.

theorem TuringMachine.computable_q_is_computable {Γ : Type} (enc : SelfReference.TMEncoding Γ) : ∃ (q : List Γ → List Γ), IsComputableFunction q ∧ ∀ (w : List Γ), ∃ (Pw : SelfReference.TMDescription Γ), q w = enc.encode Pw ∧ ∀ (input : List Γ), Pw.haltsWithOutput input w

Abstract form of the textbook Lemma: from any TMEncoding enc we get a computable function q : Σ* → Σ* with q(w) = ⟨P_w⟩, where P_w is a TM that on every input halts with w on the tape.

noncomputable def TuringMachine.concreteTMEncoding {Γ : Type} [DecidableEq Γ] (blank : Γ) (inputAlpha : Set Γ) (h_blank : blank ∉ inputAlpha) : SelfReference.TMEncoding Γ

A concrete instance of TMEncoding built from the explicit printTM construction. The encoding of a description is taken to be its stored source field, and printTMDesc w packages the printTM w machine together with source := w, so q(w) = encode(printTMDesc w) = w is the identity, which is clearly computable.

theorem TuringMachine.computable_q {Γ : Type} [DecidableEq Γ] (blank : Γ) (inputAlpha : Set Γ) (h_blank : blank ∉ inputAlpha) : ∃ (q : List Γ → List Γ), IsComputableFunction q ∧ ∀ (w : List Γ), ∃ (Pw : SelfReference.TMDescription Γ), q w = (concreteTMEncoding blank inputAlpha h_blank).encode Pw ∧ ∀ (input : List Γ), Pw.haltsWithOutput input w

Lemma (Computable function q) (Sipser, Lecture 11): instantiated with the concrete encoding. There is a computable q : Σ* → Σ* such that for every w the description P_w := printTMDesc w satisfies q w = ⟨P_w⟩ and on any input P_w halts with w on the tape.

def TuringMachine.IsMinimalIndex {Γ : Type} (C : TMCoding Γ) (M : C.TMIndex) : Prop

Minimality in the TMCoding setting: M is minimal if no strictly shorter-coded index M' has the same language.

def TuringMachine.MIN_TM_Coding {Γ : Type} (C : TMCoding Γ) : Set (List Γ)

MIN_TM = {⟨M⟩ | M is a minimal TM} expressed in the TMCoding framework.

theorem TuringMachine.exists_minimal_for_language {Γ : Type} (C : TMCoding Γ) (M : C.TMIndex) : ∃ (M' : C.TMIndex), C.languageOf M' = C.languageOf M ∧ IsMinimalIndex C M'

Every TM index M has a minimal equivalent: there exists M' with the same language as M such that M' is minimal. Proved by strong induction on the code-length, descending to a shorter equivalent whenever M itself is not minimal.

theorem TuringMachine.min_tm_has_arbitrarily_long_elements {Γ : Type} (C : TMCoding Γ) (n : ℕ) : ∃ (B : C.TMIndex), IsMinimalIndex C B ∧ n ≤ (C.encode B).length

MIN_TM contains codes of arbitrarily large length: for every n there is a minimal index B with |⟨B⟩| ≥ n. Combines languages_beyond_length with exists_minimal_for_language (a shorter minimal equivalent could not differ from all length-< n indices).

theorem TuringMachine.min_tm_arbitrarily_long_strict {Γ : Type} (C : TMCoding Γ) (n : ℕ) : ∃ (B : C.TMIndex), IsMinimalIndex C B ∧ n < (C.encode B).length

Strict version of min_tm_has_arbitrarily_long_elements: for every n some minimal index B has |⟨B⟩| > n.

theorem TuringMachine.MIN_TM_not_recognizable {Γ : Type} (C : TMCoding Γ) : ¬IsTuringRecognizable (MIN_TM_Coding C)

MIN_TM is T-unrecognizable (Sipser, Lecture 11, Ex 3). The language of codes of minimal Turing machines is not Turing-recognizable. The proof is by contradiction via the Recursion Theorem: if MIN_TM were recognizable, an enumeration would produce a computable map t sending each M to a strictly longer minimal machine, but then any fixed point R of t from the Recursion Theorem (with L(R) = L(t R)) would witness t R not being minimal — a contradiction.

structure TuringMachine.TMCodingWithCompl (Γ : Type) : Type 1

A TMCoding augmented with a computable "complement" operation compl mapping each index M to an index whose language is the set complement of L(M). Useful for applying the Recursion Theorem to constructions that flip acceptance.

• coding : TMCoding Γ
• compl : self.coding.TMIndex → self.coding.TMIndex
• compl_spec (M : self.coding.TMIndex) : self.coding.languageOf (self.compl M) = (self.coding.languageOf M)ᶜ
• compl_computable : self.coding.IsComputable self.compl

theorem TuringMachine.A_TM_not_decidable_via_recursion_theorem {Γ : Type} (enc : TMEncoding Γ) : ¬IsTuringDecidable (A_TM enc)

A_TM is undecidable — new proof via the Recursion Theorem (Sipser, Lecture 11, Ex 1). Suppose H decided A_TM. Let D be H with its accept and reject states swapped (so D decides the complement of A_TM). By the self-reference property of enc, there is a description d₀ whose computation behaves like running D on ⟨d₀⟩, giving d₀.accepts ↔ ¬ d₀.accepts, contradiction.

def GodelIncompleteness.A_TM_complement {Γ : Type} (enc : TuringMachine.TMEncoding Γ) : Set (List Γ)

The complement \overline{A_{TM}} of the acceptance language A_TM. This language is famously not Turing-recognizable and is the one whose "unprovability" gives Gödel-style results in this development.

structure GodelIncompleteness.FormalProofSystem (Γ : Type) : Type 1

A minimal abstract "formal proof system" over a TM-encoding enc. It picks out a Turing-recognizable set provable ⊆ Σ* of provable statements about TM descriptions, with the soundness assumption that if ⟨d⟩ ∈ provable then d does not accept (the statement "d is non-accepting" is true).

• enc : TuringMachine.TMEncoding Γ
• provable : Set (List Γ)
• sound (d : TuringMachine.TMDesc Γ) : self.enc.encode d ∈ self.provable → ¬d.accepts
• provable_recognizable : TuringMachine.IsTuringRecognizable self.provable

def GodelIncompleteness.FormalProofSystem.isComplete {Γ : Type} (F : FormalProofSystem Γ) : Prop

A FormalProofSystem is complete if every true non-acceptance statement is provable: whenever d does not accept, ⟨d⟩ ∈ provable. Gödel's First Incompleteness Theorem says no sound, recognizable system can be complete in this sense.

theorem GodelIncompleteness.godel_first_incompleteness {Γ : Type} (enc : TuringMachine.TMEncoding Γ) (provable : Set (List Γ)) (h_provable_recognizable : TuringMachine.IsTuringRecognizable provable) (h_sound : ∀ (d : TuringMachine.TMDesc Γ), enc.encode d ∈ provable → ¬d.accepts) : ∃ (d : TuringMachine.TMDesc Γ), ¬d.accepts ∧ enc.encode d ∉ provable

Gödel's First Incompleteness Theorem (Sipser, Lecture 11). For any sound proof system whose set of provable statements about TMs is Turing-recognizable, there is a true statement that is unprovable: there exists a description d such that d does not accept (true statement) yet ⟨d⟩ ∉ provable.

The proof uses the self-reference property of the encoding enc to build d₀ whose machine effectively simulates the recognizer P of provable on ⟨d₀⟩; soundness then forces d₀ to be non-accepting and unprovable.

theorem GodelIncompleteness.true_but_unprovable_statement {Γ : Type} (enc : TuringMachine.TMEncoding Γ) (provable : Set (List Γ)) (h_sound : ∀ (d : TuringMachine.TMDesc Γ), enc.encode d ∈ provable → ¬d.accepts) {QP : Type} [DecidableEq QP] (P : TuringMachine.TM QP Γ) (hP : P.language = provable) : ∃ (d : TuringMachine.TMDesc Γ), ¬d.accepts ∧ enc.encode d ∉ provable

A True but Unprovable Statement (Sipser, Lecture 11). Concrete version of Gödel's theorem: given an explicit TM P whose language is provable and soundness of provable, there is a description d₀ such that (1) d₀ does not accept (the statement ⟨d₀⟩ ∈ \overline{A_{TM}} is true) and (2) ⟨d₀⟩ ∉ provable (it has no proof). The witness d₀ corresponds to Sipser's machine R which on any input obtains its own code, forms the statement φ_U = "⟨R, 0⟩ ∈ \overline{A_{TM}}", and searches for a proof of φ_U.