The family layer (issues #18, #19A)

The honest replacement for closure under arbitrary external ℕ-indexed families. A fragment may only be asked to contain the conjunctions and disjunctions that the admissible set itself names.

This file is the syntax boundary. It defines the minimal data a coded family needs and nothing else — no theory decoding, no Sigma1, no definition codes, no KP, no numbering. Those are not merely absent by convention: they are defined in files that import this one, so CodedFamily cannot reach them even in principle. scripts/check_family_cone.lean pins that permanently.

Three details are load-bearing and each was validated against the HF instance before being fixed:

1. decode lands in the structure's own arity — no independent arity field can drift.
2. The enumeration is supplied by the presentation (indexEncodable), keyed on the code, not found by instance search; the syntax a coded family builds therefore depends on the code.
3. IsFamilyCode is a certificate, absorbed into the code subtype rather than carried as a separate hypothesis. Without it any code with any decoding would build a coded family, and "HF has no primitive coded families" would be unstatable.

decodes_unique makes decoding code-determined, which is what the extensionality API below rests on.

Main definitions

• FamilyPresentation: ambient Element, the IsFamilyCode subdomain, and the decoding data.
• CodedFamily, codedIInf, codedISup.

structure FirstOrder.Language.FamilyPresentation (L : Language) : Type (max (max (max u (uCode + 1)) (uIndex + 1)) v)

The family view of a presentation. The only data the syntax layer may consult.

Phrased ambient-style: one Element carrier with IsFamilyCode carving out the subdomain of codes naming infinitary families. The certificate lives in the code subtype rather than in a separate hypothesis, so decodes_unique is unconditional here while remaining vacuous for any presentation whose IsFamilyCode is empty.

• Element : Type uCode

  The elements of A.

• IsFamilyCode : self.Element → Prop

  The certificate that an element names a genuinely infinitary family. This is the predicate that is empty for HF, and the sole source of that emptiness.

• Index : { e : self.Element // self.IsFamilyCode e } → Type uIndex

  The index type a code names. Comes from the code, never fixed at ℕ.

• indexEncodable (c : { e : self.Element // self.IsFamilyCode e }) : Encodable (self.Index c)

  A code-determined enumeration. Data, not a side condition: the iInf constructor is ℕ-indexed, so a family cannot be turned into syntax without one.

• DecodesFamily (n : ℕ) (c : { e : self.Element // self.IsFamilyCode e }) : (self.Index c → L.BoundedFormulaω Empty n) → Prop

  The decoding law: which family a code denotes.

• decodes_unique {n : ℕ} {c : { e : self.Element // self.IsFamilyCode e }} {f g : self.Index c → L.BoundedFormulaω Empty n} : self.DecodesFamily n c f → self.DecodesFamily n c g → f = g

  Functionality. A family code determines its family. Without this, DecodesFamily is an arbitrary Prop and one code may admit many decodings, so decoded_by_code would constrain nothing and codedIInf would not be a function of the code.

@[reducible, inline]

abbrev FirstOrder.Language.FamilyPresentation.FamilyCode {L : Language} (P : L.FamilyPresentation) : Type uCode

The family-code subdomain.

Equations

• P.FamilyCode = { e : P.Element // P.IsFamilyCode e }

structure FirstOrder.Language.CodedFamily {L : Language} (P : L.FamilyPresentation) (n : ℕ) : Type (max (max (max u uCode) uIndex) v)

A coded family: a certified code, its decoded family, and the law tying the two together.

The certificate is no longer a separate field — it is carried by code, which lives in the IsFamilyCode subdomain. CodedFamily.infinitary recovers it.

• code : P.FamilyCode

  The certified family code.

• decode : P.Index self.code → L.BoundedFormulaω Empty n

  The formula family decoded from code.

• decoded_by_code : P.DecodesFamily n self.code self.decode

theorem FirstOrder.Language.CodedFamily.infinitary {L : Language} {P : L.FamilyPresentation} {n : ℕ} (F : CodedFamily P n) : P.IsFamilyCode ↑F.code

The infinitary certificate, recovered from the code's subdomain membership. Kept as a named accessor because "HF has no coded families" is proved by contradicting exactly this.

def FirstOrder.Language.codedIInf {L : Language} {P : L.FamilyPresentation} {n : ℕ} (F : CodedFamily P n) : L.BoundedFormulaω Empty n

The conjunction a coded family names. The encoding is the presentation's, installed locally, so the resulting syntax depends on the code rather than on ambient instance search.

Equations

• FirstOrder.Language.codedIInf F = FirstOrder.Language.BoundedFormulaω.einfWith (P.indexEncodable F.code) F.decode

def FirstOrder.Language.codedISup {L : Language} {P : L.FamilyPresentation} {n : ℕ} (F : CodedFamily P n) : L.BoundedFormulaω Empty n

The disjunction a coded family names.

Equations

• FirstOrder.Language.codedISup F = FirstOrder.Language.BoundedFormulaω.esupWith (P.indexEncodable F.code) F.decode

Acceptance gates

Extensionality

Functionality (decodes_unique) is what makes a coded family determined by its code. Everything below is a consequence.

theorem FirstOrder.Language.CodedFamily.ext {L : Language} {P : L.FamilyPresentation} {n : ℕ} {F G : CodedFamily P n} (h : F.code = G.code) : F = G

Extensionality: a coded family is its code. The decoding law is a Prop, and the decoding is determined by the code, so nothing else can differ.

theorem FirstOrder.Language.CodedFamily.ext_iff {L : Language} {P : L.FamilyPresentation} {n : ℕ} {F G : CodedFamily P n} : F = G ↔ F.code = G.code

The HF family view

HF names no infinitary family, so its family layer is determined by IsFamilyCode := False and everything else is vacuous. Defined here, at the family layer, so the syntax consumers of HF depend on nothing else — in particular not on a full presentation carrying theory decoding or Sigma1.

Element := ℕ matches the ambient HF instance, so (hfAmbient C).toFamilyPresentation is this presentation definitionally (hfAmbient_toFamilyPresentation).

def FirstOrder.Language.hfFamily (L : Language) : L.FamilyPresentation

The HF family view. No code names an infinitary family; the remaining fields are discharged by the empty code subdomain.

Equations

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