Documentation

DescriptiveComplexity.Problems.Epr.Defs

EPR: satisfiability of an `∃∀` sentence #

The Bernays–Schönfinkel–Ramsey class (Lewis 1980): is the given ∃*∀* sentence satisfiable? A sentence of that shape has no function symbols and its quantifier prefix is a block of existentials followed by a block of universals, so it is satisfiable exactly when it has a model with one element per existential variable – a small model, of which the sentence nevertheless speaks exponentially much, since a clause is checked at every assignment of its universal variables. That gap is the whole of the problem's complexity, and it is why the class sits at NEXPTIME rather than at NP.

The encoding #

An instance is a flat description, with no parse tree at all:

evar x marks the existential variables; every other variable of the sentence is universally quantified, so no mark is needed for those;
cl c marks the clauses of the matrix, which is in conjunctive normal form, and inCl c l gives the literals of a clause – a clause is the disjunction of all the literals it names, so nothing is a binary tree;
posL l s and negL l s say that the literal l is the atom of the relation symbol s, positive or negated, and arg l p x gives its argument at the position p; sig s p gives the argument positions of s.

Nothing here is a chain or a tree, so the encoding needs no order of its own – unlike DescriptiveComplexity.FINSAT, whose parse DAG has to be acyclic. That is what a prenex form with a quantifier-free matrix buys.

The semantics #

There is deliberately no decoding into a FirstOrder.Language.Sentence: the relation symbols of the encoded sentence are elements of the instance, so the decoded vocabulary would depend on the instance. Satisfaction is defined on the encoding directly, and being quantifier-free the matrix needs no fixed point: one clause per kind of literal is the whole truth definition.

A model is a finite nonempty type M, an interpretation I : A → (A → M) → Prop reading a symbol and an assignment of argument positions – required to be local, so that I s is a relation of the arity of s rather than of the whole universe – and a witness e for the existential variables. The sentence holds when every assignment of the universal variables satisfies every clause.

Equality is not part of the encoding. The class is NEXPTIME-complete either way, and a reduction that wants equality can carry its own equality symbol with the axioms it needs.

inductive FirstOrder.Language.eprRel :

Relation symbols of the language of encoded ∃*∀* sentences in conjunctive normal form.

evar : eprRel 1
evar x: the variable x is existentially quantified.
cl : eprRel 1
cl c: c is a clause of the matrix.
inCl : eprRel 2
inCl c l: the literal l occurs in the clause c.
posL : eprRel 2
posL l s: the literal l is the positive atom of the symbol s.
negL : eprRel 2
negL l s: the literal l is the negated atom of the symbol s.
arg : eprRel 3
arg l p x: the argument of the literal l at the position p is the variable x.
sig : eprRel 2
sig s p: the relation symbol s has the argument position p.

Instances For

Dependency graph

@[instance_reducible]

instance FirstOrder.Language.instDecidableEqEprRel {a✝ : ℕ} :

DecidableEq (eprRel a✝)

Equations

FirstOrder.Language.instDecidableEqEprRel = FirstOrder.Language.instDecidableEqEprRel.decEq

Dependency graph

def FirstOrder.Language.instDecidableEqEprRel.decEq {a✝ : ℕ} (x✝ x✝¹ : eprRel a✝) :

Decidable (x✝ = x✝¹)

Equations

Instances For

Dependency graph

def FirstOrder.Language.epr :

The relational vocabulary of encoded ∃*∀* sentences: a set of clauses of literals over relation symbols, with the existential variables marked.

Equations

FirstOrder.Language.epr = { Functions := fun (x : ℕ) => Empty, Relations := FirstOrder.Language.eprRel }

Instances For

Dependency graph

instance FirstOrder.Language.instIsRelationalEpr :

Language.epr.IsRelational

Dependency graph

@[reducible, inline]

abbrev FirstOrder.Language.eprEVarSym :

Language.epr.Relations 1

The symbol marking existential variables.

Equations

FirstOrder.Language.eprEVarSym = FirstOrder.Language.eprRel.evar

Instances For

Dependency graph

@[reducible, inline]

abbrev FirstOrder.Language.eprClSym :

Language.epr.Relations 1

The symbol marking clauses.

Equations

FirstOrder.Language.eprClSym = FirstOrder.Language.eprRel.cl

Instances For

Dependency graph

@[reducible, inline]

abbrev FirstOrder.Language.eprInClSym :

Language.epr.Relations 2

The symbol giving the literals of a clause.

Equations

FirstOrder.Language.eprInClSym = FirstOrder.Language.eprRel.inCl

Instances For

Dependency graph

@[reducible, inline]

abbrev FirstOrder.Language.eprPosSym :

Language.epr.Relations 2

The symbol of positive literals.

Equations

FirstOrder.Language.eprPosSym = FirstOrder.Language.eprRel.posL

Instances For

Dependency graph

@[reducible, inline]

abbrev FirstOrder.Language.eprNegSym :

Language.epr.Relations 2

The symbol of negated literals.

Equations

FirstOrder.Language.eprNegSym = FirstOrder.Language.eprRel.negL

Instances For

Dependency graph

@[reducible, inline]

abbrev FirstOrder.Language.eprArgSym :

Language.epr.Relations 3

The symbol giving the arguments of a literal.

Equations

FirstOrder.Language.eprArgSym = FirstOrder.Language.eprRel.arg

Instances For

Dependency graph

@[reducible, inline]

abbrev FirstOrder.Language.eprSigSym :

Language.epr.Relations 2

The symbol giving the signature of a relation symbol.

Equations

FirstOrder.Language.eprSigSym = FirstOrder.Language.eprRel.sig

Instances For

Dependency graph

Reading the encoding #

def DescriptiveComplexity.Epr.EVarG {A : Type} [FirstOrder.Language.epr.Structure A] (x : A) :

The variable x is existentially quantified.

Equations

DescriptiveComplexity.Epr.EVarG x = FirstOrder.Language.Structure.RelMap FirstOrder.Language.eprEVarSym ![x]

Instances For

Dependency graph

def DescriptiveComplexity.Epr.ClauseG {A : Type} [FirstOrder.Language.epr.Structure A] (c : A) :

c is a clause of the matrix.

Equations

DescriptiveComplexity.Epr.ClauseG c = FirstOrder.Language.Structure.RelMap FirstOrder.Language.eprClSym ![c]

Instances For

Dependency graph

def DescriptiveComplexity.Epr.InClG {A : Type} [FirstOrder.Language.epr.Structure A] (c l : A) :

The literal l occurs in the clause c.

Equations

DescriptiveComplexity.Epr.InClG c l = FirstOrder.Language.Structure.RelMap FirstOrder.Language.eprInClSym ![c, l]

Instances For

Dependency graph

def DescriptiveComplexity.Epr.PosG {A : Type} [FirstOrder.Language.epr.Structure A] (l s : A) :

The literal l is the positive atom of the symbol s.

Equations

DescriptiveComplexity.Epr.PosG l s = FirstOrder.Language.Structure.RelMap FirstOrder.Language.eprPosSym ![l, s]

Instances For

Dependency graph

def DescriptiveComplexity.Epr.NegG {A : Type} [FirstOrder.Language.epr.Structure A] (l s : A) :

The literal l is the negated atom of the symbol s.

Equations

DescriptiveComplexity.Epr.NegG l s = FirstOrder.Language.Structure.RelMap FirstOrder.Language.eprNegSym ![l, s]

Instances For

Dependency graph

def DescriptiveComplexity.Epr.ArgG {A : Type} [FirstOrder.Language.epr.Structure A] (l p x : A) :

The argument of the literal l at the position p is the variable x.

Equations

DescriptiveComplexity.Epr.ArgG l p x = FirstOrder.Language.Structure.RelMap FirstOrder.Language.eprArgSym ![l, p, x]

Instances For

Dependency graph

def DescriptiveComplexity.Epr.SigG {A : Type} [FirstOrder.Language.epr.Structure A] (s p : A) :

The relation symbol s has the argument position p.

Equations

DescriptiveComplexity.Epr.SigG s p = FirstOrder.Language.Structure.RelMap FirstOrder.Language.eprSigSym ![s, p]

Instances For

Dependency graph

Satisfaction #

noncomputable def DescriptiveComplexity.Epr.eprVal {A M : Type} [FirstOrder.Language.epr.Structure A] (e u : A → M) :

A → M

The value of a variable: the witness chosen for it if it is existentially quantified, and the assignment being tested otherwise. Every variable the encoding does not mark counts as universally quantified, which is what lets the encoding get away with one mark instead of two.

Equations

DescriptiveComplexity.Epr.eprVal e u x = if DescriptiveComplexity.Epr.EVarG x then e x else u x

Instances For

Dependency graph

def DescriptiveComplexity.Epr.LitTrue {A M : Type} [FirstOrder.Language.epr.Structure A] (I : A → (A → M) → Prop) (v : A → M) (l : A) :

A literal is true: its symbol holds (or fails, for a negated literal) of an assignment of the argument positions matching the environment on the arguments the encoding declares.

Equations

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

Instances For

Dependency graph

def DescriptiveComplexity.Epr.IsWF (A : Type) [FirstOrder.Language.epr.Structure A] :

Well-formedness, folded into the yes-instances as DescriptiveComplexity.FINSAT's is: an atom names one variable at each argument position, and names one at every position of its symbol's signature.

Both are what makes an atom an atom, and both are needed for the small-model property (DescriptiveComplexity.Epr.selfModel_of_eprSatOn): an atom whose arguments are ambiguous, or missing where the signature asks for one, reads differently on a universe the sentence has collapsed than on the instance itself.

Equations

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

Instances For

Dependency graph

def DescriptiveComplexity.Epr.Local {A M : Type} [FirstOrder.Language.epr.Structure A] (I : A → (A → M) → Prop) :

An interpretation is local when the value of a symbol depends only on the arguments its signature declares.

Equations

DescriptiveComplexity.Epr.Local I = ∀ (s : A) (w w' : A → M), (∀ (p : A), DescriptiveComplexity.Epr.SigG s p → w p = w' p) → (I s w ↔ I s w')

Instances For

Dependency graph

def DescriptiveComplexity.Epr.MatrixTrue {A M : Type} [FirstOrder.Language.epr.Structure A] (I : A → (A → M) → Prop) (v : A → M) :

The matrix holds at an environment: every clause has a true literal.

Equations

DescriptiveComplexity.Epr.MatrixTrue I v = ∀ (c : A), DescriptiveComplexity.Epr.ClauseG c → ∃ (l : A), DescriptiveComplexity.Epr.InClG c l ∧ DescriptiveComplexity.Epr.LitTrue I v l

Instances For

Dependency graph

The problem #

def DescriptiveComplexity.Epr.EprSatOn (A : Type) [FirstOrder.Language.epr.Structure A] :

The encoded ∃*∀* sentence is satisfiable: some finite nonempty universe carries a local interpretation of the relation symbols and a witness for the existential variables under which every assignment of the universal variables satisfies every clause.

Finiteness of the model costs nothing: a satisfiable ∃*∀* sentence has a model with one element per existential variable, which is what DescriptiveComplexity.Problems.Epr.Membership proves and uses.

Equations

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

Instances For

Dependency graph

Isomorphism-invariance #

Everything the semantics reads is a relation of the instance, so an isomorphism transports it: the model is carried over unchanged and its interpretation composed with the isomorphism, exactly as for DescriptiveComplexity.FINSAT.

theorem DescriptiveComplexity.Epr.eVarG_map {A B : Type} [FirstOrder.Language.epr.Structure A] [FirstOrder.Language.epr.Structure B] (e : FirstOrder.Language.epr.Equiv A B) (x : A) :

EVarG x ↔ EVarG (e x)

Dependency graph

theorem DescriptiveComplexity.Epr.clauseG_map {A B : Type} [FirstOrder.Language.epr.Structure A] [FirstOrder.Language.epr.Structure B] (e : FirstOrder.Language.epr.Equiv A B) (c : A) :

ClauseG c ↔ ClauseG (e c)

Dependency graph

theorem DescriptiveComplexity.Epr.inClG_map {A B : Type} [FirstOrder.Language.epr.Structure A] [FirstOrder.Language.epr.Structure B] (e : FirstOrder.Language.epr.Equiv A B) (c l : A) :

InClG c l ↔ InClG (e c) (e l)

Dependency graph

theorem DescriptiveComplexity.Epr.posG_map {A B : Type} [FirstOrder.Language.epr.Structure A] [FirstOrder.Language.epr.Structure B] (e : FirstOrder.Language.epr.Equiv A B) (l s : A) :

PosG l s ↔ PosG (e l) (e s)

Dependency graph

theorem DescriptiveComplexity.Epr.negG_map {A B : Type} [FirstOrder.Language.epr.Structure A] [FirstOrder.Language.epr.Structure B] (e : FirstOrder.Language.epr.Equiv A B) (l s : A) :

NegG l s ↔ NegG (e l) (e s)

Dependency graph

theorem DescriptiveComplexity.Epr.sigG_map {A B : Type} [FirstOrder.Language.epr.Structure A] [FirstOrder.Language.epr.Structure B] (e : FirstOrder.Language.epr.Equiv A B) (s p : A) :

SigG s p ↔ SigG (e s) (e p)

Dependency graph

theorem DescriptiveComplexity.Epr.argG_map {A B : Type} [FirstOrder.Language.epr.Structure A] [FirstOrder.Language.epr.Structure B] (e : FirstOrder.Language.epr.Equiv A B) (l p x : A) :

ArgG l p x ↔ ArgG (e l) (e p) (e x)

Dependency graph

def DescriptiveComplexity.Epr.mapI {A B : Type} [FirstOrder.Language.epr.Structure A] [FirstOrder.Language.epr.Structure B] (e : FirstOrder.Language.epr.Equiv A B) {M : Type} (I : A → (A → M) → Prop) :

B → (B → M) → Prop

The interpretation the image carries: read the symbol back through the isomorphism.

Equations

DescriptiveComplexity.Epr.mapI e I s w = I (e.symm s) fun (x : A) => w (e x)

Instances For

Dependency graph

theorem DescriptiveComplexity.Epr.local_mapI {A B : Type} [FirstOrder.Language.epr.Structure A] [FirstOrder.Language.epr.Structure B] (e : FirstOrder.Language.epr.Equiv A B) {M : Type} {I : A → (A → M) → Prop} (h : Local I) :

Local (mapI e I)

Dependency graph

theorem DescriptiveComplexity.Epr.litTrue_map {A B : Type} [FirstOrder.Language.epr.Structure A] [FirstOrder.Language.epr.Structure B] (e : FirstOrder.Language.epr.Equiv A B) {M : Type} {I : A → (A → M) → Prop} {v : A → M} {l : A} (h : LitTrue I v l) :

LitTrue (mapI e I) (fun (y : B) => v (e.symm y)) (e l)

Dependency graph

theorem DescriptiveComplexity.Epr.posG_map' {A B : Type} [FirstOrder.Language.epr.Structure A] [FirstOrder.Language.epr.Structure B] (e : FirstOrder.Language.epr.Equiv A B) (l s : B) :

PosG l s ↔ PosG (e.symm l) (e.symm s)

Dependency graph

theorem DescriptiveComplexity.Epr.negG_map' {A B : Type} [FirstOrder.Language.epr.Structure A] [FirstOrder.Language.epr.Structure B] (e : FirstOrder.Language.epr.Equiv A B) (l s : B) :

NegG l s ↔ NegG (e.symm l) (e.symm s)

Dependency graph

theorem DescriptiveComplexity.Epr.sigG_map' {A B : Type} [FirstOrder.Language.epr.Structure A] [FirstOrder.Language.epr.Structure B] (e : FirstOrder.Language.epr.Equiv A B) (s p : B) :

SigG s p ↔ SigG (e.symm s) (e.symm p)

Dependency graph

theorem DescriptiveComplexity.Epr.argG_map' {A B : Type} [FirstOrder.Language.epr.Structure A] [FirstOrder.Language.epr.Structure B] (e : FirstOrder.Language.epr.Equiv A B) (l p x : B) :

ArgG l p x ↔ ArgG (e.symm l) (e.symm p) (e.symm x)

Dependency graph

theorem DescriptiveComplexity.Epr.isWF_map {A B : Type} [FirstOrder.Language.epr.Structure A] [FirstOrder.Language.epr.Structure B] (e : FirstOrder.Language.epr.Equiv A B) (h : IsWF A) :

Well-formedness transports along an isomorphism.

Dependency graph

theorem DescriptiveComplexity.Epr.eprSatOn_map {A B : Type} [FirstOrder.Language.epr.Structure A] [FirstOrder.Language.epr.Structure B] (e : FirstOrder.Language.epr.Equiv A B) (h : EprSatOn A) :

Satisfiability transports along an isomorphism: the model is carried over unchanged, its interpretation read back through the isomorphism.

Dependency graph

def DescriptiveComplexity.EPR :

DecisionProblem FirstOrder.Language.epr

Satisfiability of an ∃*∀* sentence. The instance is the sentence, in prenex form with a conjunctive-normal-form matrix; the question is whether it has a model.

Equations

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

Instances For

Dependency graph