Numberings of the finitary sentences, and Sigma1 invariance (issue #19A)

Sigma1 is already defined from the weak layer: hfAmbient takes a plain FinitaryCoding and supplies enumerates, so every coding has its own coding-relative Sigma1. What a single coding cannot give is independence — two injective numberings can disagree about which theories are c.e. This file supplies what does:

FinitaryCoding              adequacy, AFinite, and Sigma1 itself      -- any language
FinitaryNumbering           a *bijective* numbering; no effectiveness on its own
ComputablyEquivalent C C'   Sigma1 invariance across numberings       -- the actual content

Read the middle line carefully. FinitaryNumbering is structurally a bijective numbering and nothing more: FinitaryNumbering.ofDenumerable builds one from a bare Denumerable instance, with no computability evidence whatsoever. It is not intrinsically effective, and the name deliberately does not claim to be. Invariance holds only when a ComputablyEquivalent witness is supplied; the numbering alone proves nothing about Sigma1.

The layers do not mix. hfAmbient still takes a plain FinitaryCoding, so numbering data cannot infect the fragment or theory layers. That refusal is enforced by hfAmbient_rejects_numbering, a fail_if_success regression — not merely by the positive examples below, which show only that the weak layer suffices.

The bijectivity simplification

Surjectivity is required, so every natural is a valid sentence code. Acceptable numberings then differ by computable permutations of ℕ, which is a change of bookkeeping, not of mathematics:

• invalid-input bookkeeping becomes provably vacuous — invalid_codes_eq_empty states it explicitly instead of dropping the obligation;
• forward and backward become mutually inverse total computable permutations, so the image of a code set along one is the preimage along the other (forward_image_eq_backward_preimage), and c.e. transport needs only closure under computable preimage — no dovetailing.

The cost is stated by equiv: a FinitaryNumbering exists exactly when L.Sentence is denumerable. That is the intended setting — effective Barwise theory is for recursive languages — and languages outside it keep the weak layer and correctly get no numbering at all.

Main definitions

• CE: genuine computable enumerability, ∃ f, Nat.Partrec f ∧ ∀ n, n ∈ S ↔ (f n).Dom.
• FinitaryNumbering: FinitaryCoding plus surjectivity; decode is its inverse.
• FinitaryNumbering.Sigma1: the production-facing Σ-predicate, relative to a numbering.
• ComputablyEquivalent: the computable translation data (in Type, since it is data).
• AreComputablyEquivalent: its Prop-valued wrapper, an equivalence relation.

Main results

• ComputablyEquivalent.sigma1_iff / AreComputablyEquivalent.sigma1_iff: Sigma1 is numbering-independent. This is the property injectivity alone could not give.
• ComputablyEquivalent.ce_forward_image: c.e. code sets transport along a translation.
• hfAmbient_rejects_numbering: the layer-separation guard.

Computable enumerability

Spelled out rather than taken as an existential over an arbitrary W : ℕ → Set ℕ, which would carry no computability content at all.

def FirstOrder.Language.CE (S : Set ℕ) : Prop

A genuinely c.e. set of naturals: the domain of a partial recursive function. By Nat.Partrec.Code.exists_code these are exactly the domains of Nat.Partrec.Codes, so the Σ-definition codes of hfAmbient are complete for this notion rather than a modelling convenience.

Equations

• FirstOrder.Language.CE S = ∃ (f : ℕ →. ℕ), Nat.Partrec f ∧ ∀ (n : ℕ), n ∈ S ↔ (f n).Dom

theorem FirstOrder.Language.CE.preimage {S : Set ℕ} (hS : CE S) {g : ℕ → ℕ} (hg : Computable g) : CE (g ⁻¹' S)

C.e. sets are closed under computable preimage. With bijective numberings this is all the transport that is needed: image along one translation is preimage along the other.

Bijective numberings

structure FirstOrder.Language.FinitaryNumbering (L : Language) extends L.FinitaryCoding : Type (max u v)

A bijective numbering of the finitary sentences.

FinitaryCoding plus surjectivity, so every natural is a valid sentence code.

This carries no effectiveness. It is a numbering, not an effective one: ofDenumerable builds it from a bare Denumerable instance, and nothing here constrains how enc is computed. Sigma1 is already available from the weak FinitaryCoding layer; what a numbering buys is only the ability to state ComputablyEquivalent, and independence holds only once such a witness is supplied.

• enc : L.Sentence → ℕ
• enc_injective : Function.Injective self.enc
• enc_surjective : Function.Surjective self.enc

  Every natural is a code. This is the invalid-code bookkeeping simplification, and its content is exactly that L.Sentence is denumerable — see FinitaryNumbering.equiv.

def FirstOrder.Language.FinitaryNumbering.ofDenumerable (L : Language) [Denumerable L.Sentence] : L.FinitaryNumbering

The layer is inhabited, exactly when the finitary sentences are denumerable. Without a witness the results below would be conditionally vacuous; with one they are not.

Note what this does not need: no computability hypothesis at all. That is the honest reason the structure is called a numbering rather than an effective coding.

Equations

• FirstOrder.Language.FinitaryNumbering.ofDenumerable L = { enc := ⇑(Denumerable.eqv L.Sentence), enc_injective := ⋯, enc_surjective := ⋯ }

noncomputable def FirstOrder.Language.FinitaryNumbering.equiv {L : Language} (C : L.FinitaryNumbering) : L.Sentence ≃ ℕ

What surjectivity costs, made explicit: a numbering is a denumeration of the finitary sentences.

Equations

• C.equiv = Equiv.ofBijective C.enc ⋯

noncomputable def FirstOrder.Language.FinitaryNumbering.decode {L : Language} (C : L.FinitaryNumbering) (n : ℕ) : L.Sentence

The inverse numbering.

Equations

• C.decode n = ⋯.choose

@[simp]

theorem FirstOrder.Language.FinitaryNumbering.enc_decode {L : Language} (C : L.FinitaryNumbering) (n : ℕ) : C.enc (C.decode n) = n

@[simp]

theorem FirstOrder.Language.FinitaryNumbering.decode_enc {L : Language} (C : L.FinitaryNumbering) (φ₀ : L.Sentence) : C.decode (C.enc φ₀) = φ₀

theorem FirstOrder.Language.FinitaryNumbering.isSentenceCode {L : Language} (C : L.FinitaryNumbering) (n : ℕ) : (hfAmbient C.toFinitaryCoding).IsSentenceCode n

Every natural is a sentence code.

theorem FirstOrder.Language.FinitaryNumbering.invalid_codes_eq_empty {L : Language} (C : L.FinitaryNumbering) : {n : ℕ | ¬(hfAmbient C.toFinitaryCoding).IsSentenceCode n} = ∅

There are no invalid inputs to bookkeep, so no invalid input can contribute a decoded sentence.

Stated rather than dropped: the obligation is real for a general numbering, and this records exactly which hypothesis retires it.

theorem FirstOrder.Language.FinitaryNumbering.decodeSentence_eq {L : Language} (C : L.FinitaryNumbering) (s : (hfAmbient C.toFinitaryCoding).SentenceCode) : (hfAmbient C.toFinitaryCoding).decodeSentence s = (C.decode ↑s).toLω

Ambient sentence decoding is the inverse numbering, transported into Lω₁ω.

def FirstOrder.Language.FinitaryNumbering.Sigma1 {L : Language} (C : L.FinitaryNumbering) (T : L.Theoryω) : Prop

The production-facing Σ-predicate, relative to a numbering.

Definitionally the ambient Sigma1 of the underlying weak coding — the numbering adds nothing to the definition. It exists as a separate name so that consumers state their hypotheses against a numbering, which is what makes AreComputablyEquivalent.sigma1_iff applicable to them.

Equations

• C.Sigma1 T = (FirstOrder.Language.hfAmbient C.toFinitaryCoding).Sigma1 T

theorem FirstOrder.Language.FinitaryNumbering.sigma1_def {L : Language} (C : L.FinitaryNumbering) {T : L.Theoryω} : C.Sigma1 T ↔ (hfAmbient C.toFinitaryCoding).Sigma1 T

Computable equivalence of numberings

The witness structure lives in Type — forward and backward are data, and a structure with a data field cannot be Prop. AreComputablyEquivalent is the Prop-valued public relation.

structure FirstOrder.Language.ComputablyEquivalent {L : Language} (C C' : L.FinitaryNumbering) : Type

The translation data relating two numberings.

Both translations are total computable functions, because both numberings are onto; the specifications say each sends a code to the code of the same sentence under the other numbering. Mutual inversion is then derived, not assumed.

• forward : ℕ → ℕ

  C-codes to C'-codes.

• backward : ℕ → ℕ

  C'-codes back to C-codes.

• forward_computable : Computable self.forward

  The translation is effective. This is where effectiveness enters — not the numbering.

• backward_computable : Computable self.backward

  …and so is its inverse.

• forward_spec (n : ℕ) : self.forward n = C'.enc (C.decode n)

  forward renumbers the sentence, it does not change it.

• backward_spec (n : ℕ) : self.backward n = C.enc (C'.decode n)

  Likewise backward.

@[simp]

theorem FirstOrder.Language.ComputablyEquivalent.decode_forward {L : Language} {C C' : L.FinitaryNumbering} (E : ComputablyEquivalent C C') (n : ℕ) : C'.decode (E.forward n) = C.decode n

@[simp]

theorem FirstOrder.Language.ComputablyEquivalent.decode_backward {L : Language} {C C' : L.FinitaryNumbering} (E : ComputablyEquivalent C C') (n : ℕ) : C.decode (E.backward n) = C'.decode n

@[simp]

theorem FirstOrder.Language.ComputablyEquivalent.backward_forward {L : Language} {C C' : L.FinitaryNumbering} (E : ComputablyEquivalent C C') (n : ℕ) : E.backward (E.forward n) = n

@[simp]

theorem FirstOrder.Language.ComputablyEquivalent.forward_backward {L : Language} {C C' : L.FinitaryNumbering} (E : ComputablyEquivalent C C') (n : ℕ) : E.forward (E.backward n) = n

def FirstOrder.Language.ComputablyEquivalent.refl {L : Language} (C : L.FinitaryNumbering) : ComputablyEquivalent C C

Computable equivalence is reflexive.

Equations

• One or more equations did not get rendered due to their size.

def FirstOrder.Language.ComputablyEquivalent.symm {L : Language} {C C' : L.FinitaryNumbering} (E : ComputablyEquivalent C C') : ComputablyEquivalent C' C

…symmetric — the two translations simply swap roles.

Equations

• E.symm = { forward := E.backward, backward := E.forward, forward_computable := ⋯, backward_computable := ⋯, forward_spec := ⋯, backward_spec := ⋯ }

def FirstOrder.Language.ComputablyEquivalent.trans {L : Language} {C C' C'' : L.FinitaryNumbering} (E : ComputablyEquivalent C C') (F : ComputablyEquivalent C' C'') : ComputablyEquivalent C C''

…and transitive, by composing translations. Computability composes, and the specifications compose through decode_forward / decode_backward.

Equations

• One or more equations did not get rendered due to their size.

Translation preserves sentences

theorem FirstOrder.Language.ComputablyEquivalent.decodeSentence_forward {L : Language} {C C' : L.FinitaryNumbering} (E : ComputablyEquivalent C C') (n : ℕ) : (hfAmbient C'.toFinitaryCoding).decodeSentence ⟨E.forward n, ⋯⟩ = (hfAmbient C.toFinitaryCoding).decodeSentence ⟨n, ⋯⟩

forward maps every code to a code for the same sentence.

theorem FirstOrder.Language.ComputablyEquivalent.decodeSentence_backward {L : Language} {C C' : L.FinitaryNumbering} (E : ComputablyEquivalent C C') (n : ℕ) : (hfAmbient C.toFinitaryCoding).decodeSentence ⟨E.backward n, ⋯⟩ = (hfAmbient C'.toFinitaryCoding).decodeSentence ⟨n, ⋯⟩

…and so does backward.

C.e. transport and invariance

theorem FirstOrder.Language.ComputablyEquivalent.forward_image_eq_backward_preimage {L : Language} {C C' : L.FinitaryNumbering} (E : ComputablyEquivalent C C') (S : Set ℕ) : E.forward '' S = E.backward ⁻¹' S

The translations are inverse bijections, so pushing a code set forward is the same as pulling it back. This is what lets c.e. transport avoid dovetailing.

theorem FirstOrder.Language.ComputablyEquivalent.ce_forward_image {L : Language} {C C' : L.FinitaryNumbering} (E : ComputablyEquivalent C C') {S : Set ℕ} (hS : CE S) : CE (E.forward '' S)

C.e. code sets transport along a translation.

theorem FirstOrder.Language.ComputablyEquivalent.sigma1_of_sigma1 {L : Language} {C C' : L.FinitaryNumbering} (E : ComputablyEquivalent C C') {T : L.Theoryω} (h : C.Sigma1 T) : C'.Sigma1 T

A Σ-definition code for C is turned into one for C' by precomposing its partial-recursive enumeration with backward, then re-coding through Nat.Partrec.Code.exists_code.

theorem FirstOrder.Language.ComputablyEquivalent.sigma1_iff {L : Language} {C C' : L.FinitaryNumbering} (E : ComputablyEquivalent C C') {T : L.Theoryω} : C.Sigma1 T ↔ C'.Sigma1 T

Sigma1 does not depend on which numbering was chosen.

This is the property injectivity alone could not give, and the reason the numbering layer exists separately from FinitaryCoding. Note the hypothesis: the witness E is what carries the content — a numbering by itself proves nothing here.

The public relation

ComputablyEquivalent must live in Type because it stores functions. The relation consumers should quantify over is this Prop-valued wrapper.

def FirstOrder.Language.AreComputablyEquivalent {L : Language} (C C' : L.FinitaryNumbering) : Prop

Two numberings are computably equivalent when some translation witnesses it.

Equations

• FirstOrder.Language.AreComputablyEquivalent C C' = Nonempty (FirstOrder.Language.ComputablyEquivalent C C')

theorem FirstOrder.Language.AreComputablyEquivalent.refl {L : Language} (C : L.FinitaryNumbering) : AreComputablyEquivalent C C

theorem FirstOrder.Language.AreComputablyEquivalent.symm {L : Language} {C C' : L.FinitaryNumbering} (h : AreComputablyEquivalent C C') : AreComputablyEquivalent C' C

theorem FirstOrder.Language.AreComputablyEquivalent.trans {L : Language} {C C' C'' : L.FinitaryNumbering} (h : AreComputablyEquivalent C C') (h' : AreComputablyEquivalent C' C'') : AreComputablyEquivalent C C''

theorem FirstOrder.Language.AreComputablyEquivalent.sigma1_iff {L : Language} {C C' : L.FinitaryNumbering} (h : AreComputablyEquivalent C C') {T : L.Theoryω} : C.Sigma1 T ↔ C'.Sigma1 T

Sigma1 invariance, in propositional form. The public statement of the whole file.

Layer separation, enforced

The positive examples show the weak layer suffices for adequacy and A-finiteness. They do not by themselves prevent numbering data from leaking into those layers, so the actual guard is the fail_if_success regression: hfAmbient must refuse a FinitaryNumbering.

theorem FirstOrder.Language.hfAmbient_rejects_numbering {L : Language} (C : L.FinitaryNumbering) : (hfAmbient C.toFinitaryCoding).AdequateFor L.finitaryFragment

The guard, stating both halves at once: hfAmbient refuses a numbering directly, and the forgetful route through .toFinitaryCoding is what works.

The fail_if_success line is the durable form of the separation claim. If hfAmbient were ever widened to accept numbering data it would start succeeding and this breaks — which the positive examples above would not detect.