Plain first-order definability of a decision problem

The bottom of every ladder in this library: a problem is first-order definable when a single sentence decides it on finite structures. The two variants are the usual ones, and are named as everywhere else here – DescriptiveComplexity.FODefinableFree is the order-free notion, DescriptiveComplexity.FODefinable the order-invariant one, whose sentence may mention a linear order on the universe but whose truth value may not depend on which one.

Nothing is proved first-order definable by these notions – they exist to be refuted. Every logic of this library extends first-order logic, so a problem shown here to escape it (DescriptiveComplexity.EVEN, in DescriptiveComplexity.Problems.Even) separates first-order logic from all of them unconditionally, with no complexity-theoretic assumption. The refutations themselves are Ehrenfeucht–Fraïssé arguments (DescriptiveComplexity.Games.Ehrenfeucht).

def DescriptiveComplexity.FODefinableFree {L : FirstOrder.Language} [L.IsRelational] (P : DecisionProblem L) : Prop

A decision problem is order-free first-order definable if a single sentence over its own vocabulary decides it on nonempty finite structures.

Equations

• DescriptiveComplexity.FODefinableFree P = ∃ (φ : L.Sentence), ∀ (A : Type) [inst : L.Structure A] [Finite A] [Nonempty A], P.Holds A ↔ A ⊨ φ

def DescriptiveComplexity.FODefinable {L : FirstOrder.Language} [L.IsRelational] (P : DecisionProblem L) : Prop

A decision problem is FO(≤) definable if a single sentence over the ordered expansion of its vocabulary decides it on nonempty finite ordered structures. As everywhere in this library, the equivalence is required for every linear order, so the notion is order-invariant: the sentence sees the order, the problem does not.

Equations

• DescriptiveComplexity.FODefinable P = ∃ (φ : (L.sum FirstOrder.Language.order).Sentence), ∀ (A : Type) [inst : L.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A], P.Holds A ↔ A ⊨ φ

theorem DescriptiveComplexity.foDefinableFree_congr {L : FirstOrder.Language} [L.IsRelational] {P Q : DecisionProblem L} (h : ∀ (A : Type) [inst : L.Structure A] [Finite A], P.Holds A ↔ Q.Holds A) : FODefinableFree P ↔ FODefinableFree Q

Order-free first-order definability only depends on the finite instances of a problem.

theorem DescriptiveComplexity.foDefinable_congr {L : FirstOrder.Language} [L.IsRelational] {P Q : DecisionProblem L} (h : ∀ (A : Type) [inst : L.Structure A] [Finite A], P.Holds A ↔ Q.Holds A) : FODefinable P ↔ FODefinable Q

FO(≤) definability only depends on the finite instances of a problem.

theorem DescriptiveComplexity.FODefinableFree.foDefinable {L : FirstOrder.Language} [L.IsRelational] {P : DecisionProblem L} (h : FODefinableFree P) : FODefinable P

An order-free first-order definition is in particular an order-invariant one: the order symbol is simply not used.