First-order projection formulas

A projection chooses a constant or one signed input-relation bit using only numeric information. ProjectionFormula N L α separates the numeric language N from the input language L. Its internal nodes test formulas of N; its leaves are constants or input literals. Consequently neither the choice of input bit nor its polarity can depend on input-relation values.

The syntax is a decision-tree presentation of the mutually exclusive numeric cases in the definition of first-order projections Immerman and Landau, Definition 3.6. Numeric guards may contain quantifiers; quantifier-free interpretations with arbitrary Boolean combinations of input relations are not projections. The numeric vocabulary is a parameter: no interpretation of order or BIT, or machine resource bound, is implicit in this definition.

Main definitions

• Cslib.Logic.FO.InputLiteral, Cslib.Logic.FO.InputLiteral.Realize, Cslib.Logic.FO.InputLiteral.not, Cslib.Logic.FO.InputLiteral.relabel, Cslib.Logic.FO.InputLiteral.toFormula: a constant or a signed relation applied to free variables, its semantics, negation, variable renaming, and formula view.
• Cslib.Logic.FO.ProjectionFormula, Cslib.Logic.FO.ProjectionFormula.not, Cslib.Logic.FO.ProjectionFormula.relabel, Cslib.Logic.FO.ProjectionFormula.subst, Cslib.Logic.FO.ProjectionFormula.IsQF: numeric tests with input literals at the leaves, negation, variable renaming, substitution, and quantifier-freeness.
• Cslib.Logic.FO.ProjectionFormula.toFormula: the ordinary formula over the sum of the two languages.
• Cslib.Logic.FO.ProjectionFormula.select: the literal selected by the numeric structure alone.
• Cslib.Logic.FO.ProjectionFormula.Case, Cslib.Logic.FO.ProjectionFormula.caseGuard, Cslib.Logic.FO.ProjectionFormula.caseLiteral: the leaf cases of a projection formula, their guard formulas, and their output literals.

Main results

• Cslib.Logic.FO.ProjectionFormula.realize_toFormula: realization is that of the selected literal.
• Cslib.Logic.FO.ProjectionFormula.exists_literal: one selected literal works for all input structures.
• Cslib.Logic.FO.ProjectionFormula.existsUnique_case: the numeric cases partition assignments.
• Cslib.Logic.FO.ProjectionFormula.realize_iff_exists_case: disjoint-case normal form.
• Cslib.Logic.FO.ProjectionFormula.realize_subst: truth-preserving substitution.
• Cslib.Logic.FO.ProjectionFormula.realize_relabel: variable renaming preserves realization.

References

• N. Immerman, Descriptive Complexity
• N. Immerman and S. Landau, The Complexity of Iterated Multiplication

inductive Cslib.Logic.FO.InputLiteral (L : FirstOrder.Language) (α : Type u_1) : Type (max u_1 v)

A projection output is a constant or a single input-relation literal. Arguments are variables, so even the address of the input bit is independent of input relations.

• const {L : FirstOrder.Language} {α : Type u_1} (value : Bool) : InputLiteral L α

  A constant truth value.

• rel {L : FirstOrder.Language} {α : Type u_1} {n : ℕ} (symbol : L.Relations n) (args : Fin n → α) (negative : Bool) : InputLiteral L α

  A relation on the given variables, negated exactly when negative is true.

def Cslib.Logic.FO.InputLiteral.Realize {L : FirstOrder.Language} {α : Type u_1} {M : Type u_3} [L.Structure M] : InputLiteral L α → (α → M) → Prop

The truth value of a constant or input literal.

theorem Cslib.Logic.FO.InputLiteral.realize_const {L : FirstOrder.Language} {α : Type u_1} {M : Type u_3} [L.Structure M] (b : Bool) (x : α → M) : (const b).Realize x ↔ b = true

A constant input literal .const b holds if and only if b = true.

theorem Cslib.Logic.FO.InputLiteral.realize_rel_false {L : FirstOrder.Language} {α : Type u_1} {M : Type u_3} [L.Structure M] {n : ℕ} (R : L.Relations n) (args : Fin n → α) (x : α → M) : (rel R args false).Realize x ↔ FirstOrder.Language.Structure.RelMap R fun (i : Fin n) => x (args i)

A positive relation literal .rel R args false holds when R holds on x ∘ args.

theorem Cslib.Logic.FO.InputLiteral.realize_rel_true {L : FirstOrder.Language} {α : Type u_1} {M : Type u_3} [L.Structure M] {n : ℕ} (R : L.Relations n) (args : Fin n → α) (x : α → M) : (rel R args true).Realize x ↔ ¬FirstOrder.Language.Structure.RelMap R fun (i : Fin n) => x (args i)

A negated relation literal .rel R args true holds when R does not hold on x ∘ args.

def Cslib.Logic.FO.InputLiteral.not {L : FirstOrder.Language} {α : Type u_1} : InputLiteral L α → InputLiteral L α

Negate a literal, keeping its input address unchanged.

@[simp]

theorem Cslib.Logic.FO.InputLiteral.realize_not {L : FirstOrder.Language} {α : Type u_1} {M : Type u_3} [L.Structure M] (l : InputLiteral L α) (x : α → M) : l.not.Realize x ↔ ¬l.Realize x

The negated literal l.not holds if and only if l does not hold.

def Cslib.Logic.FO.InputLiteral.relabel {L : FirstOrder.Language} {α : Type u_1} {β : Type u_2} (f : α → β) : InputLiteral L α → InputLiteral L β

Rename the variables of an input literal.

@[simp]

theorem Cslib.Logic.FO.InputLiteral.realize_relabel {L : FirstOrder.Language} {α : Type u_1} {β : Type u_2} {M : Type u_3} [L.Structure M] (f : α → β) (l : InputLiteral L α) (x : β → M) : (relabel f l).Realize x ↔ l.Realize (x ∘ f)

Relabeling a literal by f evaluates it under the assignment x ∘ f.

def Cslib.Logic.FO.InputLiteral.toFormula {L : FirstOrder.Language} {α : Type u_1} : InputLiteral L α → L.Formula α

View an input literal as a formula.

@[simp]

theorem Cslib.Logic.FO.InputLiteral.realize_toFormula {L : FirstOrder.Language} {α : Type u_1} {M : Type u_3} [L.Structure M] (l : InputLiteral L α) (x : α → M) : l.toFormula.Realize x ↔ l.Realize x

The formula l.toFormula is realized if and only if l is realized.

theorem Cslib.Logic.FO.InputLiteral.isQF_toFormula {L : FirstOrder.Language} {α : Type u_1} (l : InputLiteral L α) : FirstOrder.Language.BoundedFormula.IsQF l.toFormula

Every input literal is quantifier-free.

inductive Cslib.Logic.FO.ProjectionFormula (N : FirstOrder.Language) (L : FirstOrder.Language) (α : Type u_1) : Type (max (max (max u u_1) v) v')

A first-order projection formula: numeric tests may choose between input literals, but input values cannot occur in the tests. N and L are separate vocabularies.

• leaf {N : FirstOrder.Language} {L : FirstOrder.Language} {α : Type u_1} (literal : InputLiteral L α) : ProjectionFormula N L α

  A constant or a single signed input bit.

• branch {N : FirstOrder.Language} {L : FirstOrder.Language} {α : Type u_1} (guard : N.Formula α) (yes no : ProjectionFormula N L α) : ProjectionFormula N L α

  Test a numeric formula, independently of the input relations.

def Cslib.Logic.FO.ProjectionFormula.toFormula {N : FirstOrder.Language} {L : FirstOrder.Language} {α : Type u_1} : ProjectionFormula N L α → (N.sum L).Formula α

Translate numeric tests and input literals to the sum language.

noncomputable def Cslib.Logic.FO.ProjectionFormula.select {N : FirstOrder.Language} {L : FirstOrder.Language} {α : Type u_1} {M : Type u_3} [N.Structure M] (x : α → M) : ProjectionFormula N L α → InputLiteral L α

Choose the output literal using only the numeric structure and the variable assignment. There is deliberately no L.Structure M parameter.

theorem Cslib.Logic.FO.ProjectionFormula.realize_toFormula {N : FirstOrder.Language} {L : FirstOrder.Language} {α : Type u_1} {M : Type u_3} [N.Structure M] [L.Structure M] (p : ProjectionFormula N L α) (x : α → M) : p.toFormula.Realize x ↔ (select x p).Realize x

The output of a projection is exactly one literal selected without inspecting the input relations. This statement holds for every interpretation of the input vocabulary.

theorem Cslib.Logic.FO.ProjectionFormula.realize_toFormula_leaf {N : FirstOrder.Language} {L : FirstOrder.Language} {α : Type u_1} {M : Type u_3} [N.Structure M] [L.Structure M] (l : InputLiteral L α) (x : α → M) : (leaf l).toFormula.Realize x ↔ l.Realize x

A leaf is realized as its literal.

theorem Cslib.Logic.FO.ProjectionFormula.realize_toFormula_branch {N : FirstOrder.Language} {L : FirstOrder.Language} {α : Type u_1} {M : Type u_3} [N.Structure M] [L.Structure M] (guard : N.Formula α) (yes no : ProjectionFormula N L α) (x : α → M) : (branch guard yes no).toFormula.Realize x ↔ guard.Realize x ∧ yes.toFormula.Realize x ∨ ¬guard.Realize x ∧ no.toFormula.Realize x

A branch is realized as its first or second subtree, as its numeric guard holds or not.

theorem Cslib.Logic.FO.ProjectionFormula.exists_literal {N : FirstOrder.Language} {L : FirstOrder.Language} {α : Type u_1} {M : Type u_3} [N.Structure M] (p : ProjectionFormula N L α) (x : α → M) : ∃ (l : InputLiteral L α), ∀ (x_1 : L.Structure M), p.toFormula.Realize x ↔ l.Realize x

A single literal works for every interpretation of the input relations. The existential choice precedes the input structure: the selected literal cannot depend on input bits.

def Cslib.Logic.FO.ProjectionFormula.not {N : FirstOrder.Language} {L : FirstOrder.Language} {α : Type u_1} : ProjectionFormula N L α → ProjectionFormula N L α

Negate the output, leaving all numeric tests unchanged.

@[simp]

theorem Cslib.Logic.FO.ProjectionFormula.select_not {N : FirstOrder.Language} {L : FirstOrder.Language} {α : Type u_1} {M : Type u_3} [N.Structure M] (p : ProjectionFormula N L α) (x : α → M) : select x p.not = (select x p).not

Selecting a literal from p.not negates the literal selected from p.

def Cslib.Logic.FO.ProjectionFormula.relabel {N : FirstOrder.Language} {L : FirstOrder.Language} {α : Type u_1} {β : Type u_2} (f : α → β) : ProjectionFormula N L α → ProjectionFormula N L β

Rename every free variable in numeric tests and input literals.

@[simp]

theorem Cslib.Logic.FO.ProjectionFormula.select_relabel {N : FirstOrder.Language} {L : FirstOrder.Language} {α : Type u_1} {β : Type u_2} {M : Type u_3} [N.Structure M] (f : α → β) (p : ProjectionFormula N L α) (x : β → M) : select x (relabel f p) = InputLiteral.relabel f (select (x ∘ f) p)

Selecting a literal from p.relabel f relabels the literal selected under x ∘ f.

theorem Cslib.Logic.FO.ProjectionFormula.realize_relabel {N : FirstOrder.Language} {L : FirstOrder.Language} {α : Type u_1} {β : Type u_2} {M : Type u_3} [N.Structure M] [L.Structure M] (f : α → β) (p : ProjectionFormula N L α) (x : β → M) : (relabel f p).toFormula.Realize x ↔ p.toFormula.Realize (x ∘ f)

Relabeling a projection formula by f evaluates its formula under x ∘ f.

@[simp]

theorem Cslib.Logic.FO.ProjectionFormula.realize_not {N : FirstOrder.Language} {L : FirstOrder.Language} {α : Type u_1} {M : Type u_3} [N.Structure M] [L.Structure M] (p : ProjectionFormula N L α) (x : α → M) : p.not.toFormula.Realize x ↔ ¬p.toFormula.Realize x

The formula of p.not holds if and only if the formula of p does not hold.

def Cslib.Logic.FO.ProjectionFormula.subst {N : FirstOrder.Language} {L : FirstOrder.Language} {α : Type u_1} {β : Type u_2} {N' : FirstOrder.Language} {L' : FirstOrder.Language} (guard : N.Formula α → N'.Formula β) (literal : InputLiteral L α → ProjectionFormula N' L' β) : ProjectionFormula N L α → ProjectionFormula N' L' β

Substitute numeric tests and input literals independently. In particular, replacing each input literal by a projection preserves the one-input-bit restriction.

theorem Cslib.Logic.FO.ProjectionFormula.realize_subst {N : FirstOrder.Language} {L : FirstOrder.Language} {α : Type u_1} {β : Type u_2} {M : Type u_3} {N' : FirstOrder.Language} {L' : FirstOrder.Language} {M' : Type u_4} [N.Structure M] [L.Structure M] [N'.Structure M'] [L'.Structure M'] (guard : N.Formula α → N'.Formula β) (literal : InputLiteral L α → ProjectionFormula N' L' β) (x : α → M) (y : β → M') (hguard : ∀ (g : N.Formula α), (guard g).Realize y ↔ g.Realize x) (hliteral : ∀ (l : InputLiteral L α), (literal l).toFormula.Realize y ↔ l.Realize x) (p : ProjectionFormula N L α) : (subst guard literal p).toFormula.Realize y ↔ p.toFormula.Realize x

Correct substitutions of numeric tests and input literals preserve truth. The source and target structures need not have the same universe or vocabulary.

def Cslib.Logic.FO.ProjectionFormula.IsQF {N : FirstOrder.Language} {L : FirstOrder.Language} {α : Type u_1} : ProjectionFormula N L α → Prop

All numeric tests are quantifier-free. The vocabulary is still a parameter; this property alone does not select the classical numeric vocabulary or exclude BIT.

theorem Cslib.Logic.FO.ProjectionFormula.isQF_leaf {N : FirstOrder.Language} {L : FirstOrder.Language} {α : Type u_1} (l : InputLiteral L α) : (leaf l).IsQF

Every leaf projection formula is quantifier-free.

theorem Cslib.Logic.FO.ProjectionFormula.IsQF.branch {N : FirstOrder.Language} {L : FirstOrder.Language} {α : Type u_1} {guard : N.Formula α} {yes no : ProjectionFormula N L α} (hguard : FirstOrder.Language.BoundedFormula.IsQF guard) (hyes : yes.IsQF) (hno : no.IsQF) : (ProjectionFormula.branch guard yes no).IsQF

A branch of quantifier-free subformulas with a quantifier-free guard is quantifier-free.

theorem Cslib.Logic.FO.ProjectionFormula.IsQF.toFormula {N : FirstOrder.Language} {L : FirstOrder.Language} {α : Type u_1} {p : ProjectionFormula N L α} (h : p.IsQF) : FirstOrder.Language.BoundedFormula.IsQF p.toFormula

Quantifier-free numeric tests give a quantifier-free ordinary formula. Quantifier-freeness of an arbitrary ordinary formula does not ensure it is a projection: it can mix input bits.

theorem Cslib.Logic.FO.ProjectionFormula.IsQF.not {N : FirstOrder.Language} {L : FirstOrder.Language} {α : Type u_1} {p : ProjectionFormula N L α} (h : p.IsQF) : p.not.IsQF

Negating a quantifier-free projection formula preserves quantifier-freeness.

theorem Cslib.Logic.FO.ProjectionFormula.IsQF.relabel {N : FirstOrder.Language} {L : FirstOrder.Language} {α : Type u_1} {β : Type u_2} {p : ProjectionFormula N L α} (h : p.IsQF) (f : α → β) : (ProjectionFormula.relabel f p).IsQF

Relabeling a quantifier-free projection formula preserves quantifier-freeness.

theorem Cslib.Logic.FO.ProjectionFormula.IsQF.subst {N : FirstOrder.Language} {L : FirstOrder.Language} {α : Type u_1} {β : Type u_2} {N' : FirstOrder.Language} {L' : FirstOrder.Language} {p : ProjectionFormula N L α} (h : p.IsQF) (guard : N.Formula α → N'.Formula β) (literal : InputLiteral L α → ProjectionFormula N' L' β) (hguard : ∀ (g : N.Formula α), FirstOrder.Language.BoundedFormula.IsQF g → FirstOrder.Language.BoundedFormula.IsQF (guard g)) (hliteral : ∀ (l : InputLiteral L α), (literal l).IsQF) : (ProjectionFormula.subst guard literal p).IsQF

Substituting quantifier-free guards and quantifier-free projections into a quantifier-free projection formula preserves quantifier-freeness.

def Cslib.Logic.FO.ProjectionFormula.Case {N : FirstOrder.Language} {L : FirstOrder.Language} {α : Type u_1} : ProjectionFormula N L α → Type

The finitely many leaf occurrences of a projection formula. Distinct occurrences remain distinct even when they carry the same literal.

@[instance_reducible]

noncomputable instance Cslib.Logic.FO.ProjectionFormula.instFintypeCase {N : FirstOrder.Language} {L : FirstOrder.Language} {α : Type u_1} (p : ProjectionFormula N L α) : Fintype p.Case

A projection formula has finitely many leaf cases.

def Cslib.Logic.FO.ProjectionFormula.caseGuard {N : FirstOrder.Language} {L : FirstOrder.Language} {α : Type u_1} (p : ProjectionFormula N L α) : p.Case → N.Formula α

The conjunction of numeric tests on the path to a leaf.

def Cslib.Logic.FO.ProjectionFormula.caseLiteral {N : FirstOrder.Language} {L : FirstOrder.Language} {α : Type u_1} (p : ProjectionFormula N L α) : p.Case → InputLiteral L α

The literal at a leaf occurrence.

theorem Cslib.Logic.FO.ProjectionFormula.existsUnique_case {N : FirstOrder.Language} {L : FirstOrder.Language} {α : Type u_1} {M : Type u_3} [N.Structure M] (p : ProjectionFormula N L α) (x : α → M) : ∃! c : p.Case, (p.caseGuard c).Realize x

The numeric cases form a partition, including on empty structures whenever an assignment of the free variables exists.

theorem Cslib.Logic.FO.ProjectionFormula.realize_iff_exists_case {N : FirstOrder.Language} {L : FirstOrder.Language} {α : Type u_1} {M : Type u_3} [N.Structure M] [L.Structure M] (p : ProjectionFormula N L α) (x : α → M) : p.toFormula.Realize x ↔ ∃ (c : p.Case), (p.caseGuard c).Realize x ∧ (p.caseLiteral c).Realize x

A projection is the disjunction of its mutually exclusive numeric cases, each conjoined with one constant or signed input literal.