PCP is in RE

The syntax half of DescriptiveComplexity.Pcp.pcpOn_iff_cert: the certificate of a match is written as an ∃SO[new] sentence, the logic defining RE.

• the invented values are the slots – the places of the sequence of dominoes – and no other sort is needed, so every quantifier of the kernel is guarded either by ¬old (a slot) or by old (an element of the instance, playing whichever of the three roles the position it sits in asks for);
• the three components of DescriptiveComplexity.Pcp.Cert are the relation variables of a single existential second-order block (DescriptiveComplexity.Pcp.certBlock), the matching being the only one of arity 4;
• the conditions of DescriptiveComplexity.Pcp.CertOK, together with the well-formedness of the instance, are the conjuncts of the first-order kernel.

The deep conjunct is the one saying the matching reflects the lexicographic order of the two parses: eight guarded quantifiers, alternating slot and position, which is why the variables are named by their distance from their binder, exactly as in DescriptiveComplexity.Problems.CodeHalt.Membership.

Nothing here is a machine model: DescriptiveComplexity.pcp_mem_RE is a statement about the logic ∃SO[new], and it is what makes Post's problem reduce to finite satisfiability (DescriptiveComplexity.pcp_le_finsat). RE-hardness of PCP is a different matter – the computation-history dominoes of DescriptiveComplexity.Problems.Pcp.Hardness – and with it Post's problem is RE-complete (DescriptiveComplexity.pcp_RE_complete).

The second-order block

inductive DescriptiveComplexity.Pcp.CertIx : Type

The relation variables of the ∃SO[new] definition of PCP: the order of the slots, the domino at a slot, and the matching between the two parses.

• sle : CertIx

  The order of the slots.

• dm : CertIx

  The domino at a slot.

• mt : CertIx

  The matching between the two parses.

@[instance_reducible]

instance DescriptiveComplexity.Pcp.instDecidableEqCertIx : DecidableEq CertIx

Equations

• DescriptiveComplexity.Pcp.instDecidableEqCertIx x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance DescriptiveComplexity.Pcp.instFintypeCertIx : Fintype CertIx

Equations

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

def DescriptiveComplexity.Pcp.certBlock : SOBlock

The single existential block of the definition.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.Pcp.certLang : FirstOrder.Language

The vocabulary the kernel is written in.

Equations

• DescriptiveComplexity.Pcp.certLang = DescriptiveComplexity.soLang (DescriptiveComplexity.newLang FirstOrder.Language.pcp) [DescriptiveComplexity.Pcp.certBlock]

@[reducible, inline]

abbrev DescriptiveComplexity.Pcp.instSym {n : ℕ} (R : FirstOrder.Language.pcp.Relations n) : certLang.Relations n

A relation symbol of the instance, in the kernel's vocabulary.

Equations

• DescriptiveComplexity.Pcp.instSym R = Sum.inl (Sum.inl R)

@[reducible, inline]

abbrev DescriptiveComplexity.Pcp.oldSym : certLang.Relations 1

The symbol marking the original elements.

Equations

• DescriptiveComplexity.Pcp.oldSym = Sum.inl (Sum.inr FirstOrder.Language.oldSym)

@[reducible, inline]

abbrev DescriptiveComplexity.Pcp.sleSym : certLang.Relations 2

The symbol ordering the slots.

Equations

• DescriptiveComplexity.Pcp.sleSym = Sum.inr ⟨DescriptiveComplexity.Pcp.CertIx.sle, DescriptiveComplexity.Pcp.sleSym._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.Pcp.dmSym : certLang.Relations 2

The symbol giving the domino at a slot.

Equations

• DescriptiveComplexity.Pcp.dmSym = Sum.inr ⟨DescriptiveComplexity.Pcp.CertIx.dm, DescriptiveComplexity.Pcp.dmSym._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.Pcp.mtSym : certLang.Relations 4

The symbol matching the two parses.

Equations

• DescriptiveComplexity.Pcp.mtSym = Sum.inr ⟨DescriptiveComplexity.Pcp.CertIx.mt, DescriptiveComplexity.Pcp.mtSym._proof_1⟩

The extended universe

@[instance_reducible]

noncomputable def DescriptiveComplexity.Pcp.extPcp {A : Type} [FirstOrder.Language.pcp.Structure A] {m : ℕ} : FirstOrder.Language.pcp.Structure (A ⊕ Fin m)

The vocabulary of the instance, read on the extended universe.

Equations

• DescriptiveComplexity.Pcp.extPcp = DescriptiveComplexity.extBase FirstOrder.Language.pcp A m

@[instance_reducible]

noncomputable def DescriptiveComplexity.Pcp.certStr {A : Type} [FirstOrder.Language.pcp.Structure A] {m : ℕ} (ρ : certBlock.Assignment (A ⊕ Fin m)) : certLang.Structure (A ⊕ Fin m)

The structure the kernel is read in: the extended structure together with an assignment of the relation variables.

Equations

• DescriptiveComplexity.Pcp.certStr ρ = (DescriptiveComplexity.newLang FirstOrder.Language.pcp).sumStructure DescriptiveComplexity.Pcp.certBlock.lang (A ⊕ Fin m)

The instance, read on the extended universe

A relation of the instance holds on the extended universe only of original elements, and there of what it holds of in the instance – so at original arguments the kernel reads the instance itself.

@[simp]

theorem DescriptiveComplexity.Pcp.relMap_inl₁ {A : Type} [FirstOrder.Language.pcp.Structure A] {m : ℕ} (R : FirstOrder.Language.pcp.Relations 1) (a : A) : FirstOrder.Language.Structure.RelMap R ![Sum.inl a] ↔ FirstOrder.Language.Structure.RelMap R ![a]

@[simp]

theorem DescriptiveComplexity.Pcp.relMap_inl₂ {A : Type} [FirstOrder.Language.pcp.Structure A] {m : ℕ} (R : FirstOrder.Language.pcp.Relations 2) (a b : A) : FirstOrder.Language.Structure.RelMap R ![Sum.inl a, Sum.inl b] ↔ FirstOrder.Language.Structure.RelMap R ![a, b]

@[simp]

theorem DescriptiveComplexity.Pcp.relMap_inl₃ {A : Type} [FirstOrder.Language.pcp.Structure A] {m : ℕ} (R : FirstOrder.Language.pcp.Relations 3) (a b c : A) : FirstOrder.Language.Structure.RelMap R ![Sum.inl a, Sum.inl b, Sum.inl c] ↔ FirstOrder.Language.Structure.RelMap R ![a, b, c]

The certificate an assignment carries

def DescriptiveComplexity.Pcp.certOf {A : Type} {m : ℕ} (ρ : certBlock.Assignment (A ⊕ Fin m)) : Cert A (Fin m)

The certificate an assignment carries: the relation variables read at the sorts they are meant for – slots among the invented values, dominoes and positions among the original elements.

Equations

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

@[simp]

theorem DescriptiveComplexity.Pcp.certOf_sle {A : Type} {m : ℕ} (ρ : certBlock.Assignment (A ⊕ Fin m)) (s t : Fin m) : (certOf ρ).SLe s t ↔ ρ CertIx.sle ![Sum.inr s, Sum.inr t]

@[simp]

theorem DescriptiveComplexity.Pcp.certOf_dm {A : Type} {m : ℕ} (ρ : certBlock.Assignment (A ⊕ Fin m)) (s : Fin m) (d : A) : (certOf ρ).Dm s d ↔ ρ CertIx.dm ![Sum.inr s, Sum.inl d]

@[simp]

theorem DescriptiveComplexity.Pcp.certOf_mt {A : Type} {m : ℕ} (ρ : certBlock.Assignment (A ⊕ Fin m)) (s : Fin m) (p : A) (s' : Fin m) (p' : A) : (certOf ρ).Mt s p s' p' ↔ ρ CertIx.mt ![Sum.inr s, Sum.inl p, Sum.inr s', Sum.inl p']

Atomic formulas

noncomputable def DescriptiveComplexity.Pcp.instF₁ {γ : Type} (R : FirstOrder.Language.pcp.Relations 1) (x : γ) : certLang.Formula γ

An atom of a unary relation of the instance.

Equations

• DescriptiveComplexity.Pcp.instF₁ R x = (DescriptiveComplexity.Pcp.instSym R).formula₁ (FirstOrder.Language.var x)

noncomputable def DescriptiveComplexity.Pcp.instF₂ {γ : Type} (R : FirstOrder.Language.pcp.Relations 2) (x y : γ) : certLang.Formula γ

An atom of a binary relation of the instance.

Equations

• DescriptiveComplexity.Pcp.instF₂ R x y = (DescriptiveComplexity.Pcp.instSym R).formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

noncomputable def DescriptiveComplexity.Pcp.instF₃ {γ : Type} (R : FirstOrder.Language.pcp.Relations 3) (x y z : γ) : certLang.Formula γ

An atom of a ternary relation of the instance.

Equations

• DescriptiveComplexity.Pcp.instF₃ R x y z = (DescriptiveComplexity.Pcp.instSym R).formula ![FirstOrder.Language.var x, FirstOrder.Language.var y, FirstOrder.Language.var z]

noncomputable def DescriptiveComplexity.Pcp.oldF {γ : Type} (x : γ) : certLang.Formula γ

x is an original element.

Equations

• DescriptiveComplexity.Pcp.oldF x = DescriptiveComplexity.Pcp.oldSym.formula₁ (FirstOrder.Language.var x)

noncomputable def DescriptiveComplexity.Pcp.eqF {γ : Type} (x y : γ) : certLang.Formula γ

Equality of two variables.

Equations

• DescriptiveComplexity.Pcp.eqF x y = (FirstOrder.Language.var x).equal (FirstOrder.Language.var y)

noncomputable def DescriptiveComplexity.Pcp.sleF {γ : Type} (s t : γ) : certLang.Formula γ

The slot s is at most the slot t.

Equations

• DescriptiveComplexity.Pcp.sleF s t = DescriptiveComplexity.Pcp.sleSym.formula₂ (FirstOrder.Language.var s) (FirstOrder.Language.var t)

noncomputable def DescriptiveComplexity.Pcp.dmF {γ : Type} (s d : γ) : certLang.Formula γ

The domino d sits at the slot s.

Equations

• DescriptiveComplexity.Pcp.dmF s d = DescriptiveComplexity.Pcp.dmSym.formula₂ (FirstOrder.Language.var s) (FirstOrder.Language.var d)

noncomputable def DescriptiveComplexity.Pcp.mtF {γ : Type} (s p s' p' : γ) : certLang.Formula γ

The top index (s, p) is matched with the bottom index (s', p').

Equations

• DescriptiveComplexity.Pcp.mtF s p s' p' = DescriptiveComplexity.Pcp.mtSym.formula ![FirstOrder.Language.var s, FirstOrder.Language.var p, FirstOrder.Language.var s', FirstOrder.Language.var p']

@[simp]

theorem DescriptiveComplexity.Pcp.realize_instF₁ {A : Type} [FirstOrder.Language.pcp.Structure A] {m : ℕ} {ρ : certBlock.Assignment (A ⊕ Fin m)} {γ : Type} (R : FirstOrder.Language.pcp.Relations 1) (x : γ) (v : γ → A ⊕ Fin m) : (instF₁ R x).Realize v ↔ FirstOrder.Language.Structure.RelMap R ![v x]

@[simp]

theorem DescriptiveComplexity.Pcp.realize_instF₂ {A : Type} [FirstOrder.Language.pcp.Structure A] {m : ℕ} {ρ : certBlock.Assignment (A ⊕ Fin m)} {γ : Type} (R : FirstOrder.Language.pcp.Relations 2) (x y : γ) (v : γ → A ⊕ Fin m) : (instF₂ R x y).Realize v ↔ FirstOrder.Language.Structure.RelMap R ![v x, v y]

@[simp]

theorem DescriptiveComplexity.Pcp.realize_instF₃ {A : Type} [FirstOrder.Language.pcp.Structure A] {m : ℕ} {ρ : certBlock.Assignment (A ⊕ Fin m)} {γ : Type} (R : FirstOrder.Language.pcp.Relations 3) (x y z : γ) (v : γ → A ⊕ Fin m) : (instF₃ R x y z).Realize v ↔ FirstOrder.Language.Structure.RelMap R ![v x, v y, v z]

@[simp]

theorem DescriptiveComplexity.Pcp.realize_oldF {A : Type} [FirstOrder.Language.pcp.Structure A] {m : ℕ} {ρ : certBlock.Assignment (A ⊕ Fin m)} {γ : Type} (x : γ) (v : γ → A ⊕ Fin m) : (oldF x).Realize v ↔ IsOld (v x)

@[simp]

theorem DescriptiveComplexity.Pcp.realize_eqF {A : Type} [FirstOrder.Language.pcp.Structure A] {m : ℕ} {ρ : certBlock.Assignment (A ⊕ Fin m)} {γ : Type} (x y : γ) (v : γ → A ⊕ Fin m) : (eqF x y).Realize v ↔ v x = v y

@[simp]

theorem DescriptiveComplexity.Pcp.realize_sleF {A : Type} [FirstOrder.Language.pcp.Structure A] {m : ℕ} {ρ : certBlock.Assignment (A ⊕ Fin m)} {γ : Type} (s t : γ) (v : γ → A ⊕ Fin m) : (sleF s t).Realize v ↔ ρ CertIx.sle ![v s, v t]

@[simp]

theorem DescriptiveComplexity.Pcp.realize_dmF {A : Type} [FirstOrder.Language.pcp.Structure A] {m : ℕ} {ρ : certBlock.Assignment (A ⊕ Fin m)} {γ : Type} (s d : γ) (v : γ → A ⊕ Fin m) : (dmF s d).Realize v ↔ ρ CertIx.dm ![v s, v d]

@[simp]

theorem DescriptiveComplexity.Pcp.realize_mtF {A : Type} [FirstOrder.Language.pcp.Structure A] {m : ℕ} {ρ : certBlock.Assignment (A ⊕ Fin m)} {γ : Type} (s p s' p' : γ) (v : γ → A ⊕ Fin m) : (mtF s p s' p').Realize v ↔ ρ CertIx.mt ![v s, v p, v s', v p']

Naming the symbols of the instance

Guarded quantifiers

Every quantifier of the kernel ranges over one of the two sorts of the extended universe – the elements of the instance, marked by old, and the slots – and is guarded accordingly. A variable is named by its distance from its binder.

@[reducible, inline]

abbrev DescriptiveComplexity.Pcp.up {γ : Type} (x : γ) : γ ⊕ Unit

A variable of the enclosing scope, seen from inside one guarded quantifier.

Equations

• DescriptiveComplexity.Pcp.up x = Sum.inl x

@[reducible, inline]

abbrev DescriptiveComplexity.Pcp.vr0 {γ : Type} : γ ⊕ Unit

The variable bound by the innermost guarded quantifier.

Equations

• DescriptiveComplexity.Pcp.vr0 = Sum.inr ()

@[reducible, inline]

abbrev DescriptiveComplexity.Pcp.vr1 {γ : Type} : (γ ⊕ Unit) ⊕ Unit

The variable bound one guarded quantifier further out.

Equations

• DescriptiveComplexity.Pcp.vr1 = DescriptiveComplexity.Pcp.up DescriptiveComplexity.Pcp.vr0

@[reducible, inline]

abbrev DescriptiveComplexity.Pcp.vr2 {γ : Type} : ((γ ⊕ Unit) ⊕ Unit) ⊕ Unit

The variable bound two guarded quantifiers further out.

Equations

• DescriptiveComplexity.Pcp.vr2 = DescriptiveComplexity.Pcp.up DescriptiveComplexity.Pcp.vr1

@[reducible, inline]

abbrev DescriptiveComplexity.Pcp.vr3 {γ : Type} : (((γ ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit

The variable bound three guarded quantifiers further out.

Equations

• DescriptiveComplexity.Pcp.vr3 = DescriptiveComplexity.Pcp.up DescriptiveComplexity.Pcp.vr2

@[reducible, inline]

abbrev DescriptiveComplexity.Pcp.vr4 {γ : Type} : ((((γ ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit

The variable bound four guarded quantifiers further out.

Equations

• DescriptiveComplexity.Pcp.vr4 = DescriptiveComplexity.Pcp.up DescriptiveComplexity.Pcp.vr3

@[reducible, inline]

abbrev DescriptiveComplexity.Pcp.vr5 {γ : Type} : (((((γ ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit

The variable bound five guarded quantifiers further out.

Equations

• DescriptiveComplexity.Pcp.vr5 = DescriptiveComplexity.Pcp.up DescriptiveComplexity.Pcp.vr4

@[reducible, inline]

abbrev DescriptiveComplexity.Pcp.vr6 {γ : Type} : ((((((γ ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit

The variable bound six guarded quantifiers further out.

Equations

• DescriptiveComplexity.Pcp.vr6 = DescriptiveComplexity.Pcp.up DescriptiveComplexity.Pcp.vr5

@[reducible, inline]

abbrev DescriptiveComplexity.Pcp.vr7 {γ : Type} : (((((((γ ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit

The variable bound seven guarded quantifiers further out.

Equations

• DescriptiveComplexity.Pcp.vr7 = DescriptiveComplexity.Pcp.up DescriptiveComplexity.Pcp.vr6

noncomputable def DescriptiveComplexity.Pcp.exOldF {γ : Type} (φ : certLang.Formula (γ ⊕ Unit)) : certLang.Formula γ

∃ x, old x ∧ φ: a quantifier over the elements of the instance.

Equations

• DescriptiveComplexity.Pcp.exOldF φ = FirstOrder.Language.Formula.iExs Unit (DescriptiveComplexity.Pcp.oldF DescriptiveComplexity.Pcp.vr0 ⊓ φ)

noncomputable def DescriptiveComplexity.Pcp.allOldF {γ : Type} (φ : certLang.Formula (γ ⊕ Unit)) : certLang.Formula γ

∀ x, old x → φ: a quantifier over the elements of the instance.

Equations

• DescriptiveComplexity.Pcp.allOldF φ = FirstOrder.Language.Formula.iAlls Unit (FirstOrder.Language.BoundedFormula.imp (DescriptiveComplexity.Pcp.oldF DescriptiveComplexity.Pcp.vr0) φ)

noncomputable def DescriptiveComplexity.Pcp.exNewF {γ : Type} (φ : certLang.Formula (γ ⊕ Unit)) : certLang.Formula γ

∃ s, ¬old s ∧ φ: a quantifier over the slots.

Equations

• DescriptiveComplexity.Pcp.exNewF φ = FirstOrder.Language.Formula.iExs Unit (FirstOrder.Language.BoundedFormula.not (DescriptiveComplexity.Pcp.oldF DescriptiveComplexity.Pcp.vr0) ⊓ φ)

noncomputable def DescriptiveComplexity.Pcp.allNewF {γ : Type} (φ : certLang.Formula (γ ⊕ Unit)) : certLang.Formula γ

∀ s, ¬old s → φ: a quantifier over the slots.

Equations

• DescriptiveComplexity.Pcp.allNewF φ = FirstOrder.Language.Formula.iAlls Unit ((FirstOrder.Language.BoundedFormula.not (DescriptiveComplexity.Pcp.oldF DescriptiveComplexity.Pcp.vr0)).imp φ)

theorem DescriptiveComplexity.Pcp.exists_inr_of_not_isOld {A : Type} {m : ℕ} {x : A ⊕ Fin m} (h : ¬IsOld x) : ∃ (j : Fin m), x = Sum.inr j

@[simp]

theorem DescriptiveComplexity.Pcp.realize_exOldF {A : Type} [FirstOrder.Language.pcp.Structure A] {m : ℕ} {ρ : certBlock.Assignment (A ⊕ Fin m)} {γ : Type} (φ : certLang.Formula (γ ⊕ Unit)) (v : γ → A ⊕ Fin m) : (exOldF φ).Realize v ↔ ∃ (a : A), φ.Realize (Sum.elim v fun (x : Unit) => Sum.inl a)

@[simp]

theorem DescriptiveComplexity.Pcp.realize_allOldF {A : Type} [FirstOrder.Language.pcp.Structure A] {m : ℕ} {ρ : certBlock.Assignment (A ⊕ Fin m)} {γ : Type} (φ : certLang.Formula (γ ⊕ Unit)) (v : γ → A ⊕ Fin m) : (allOldF φ).Realize v ↔ ∀ (a : A), φ.Realize (Sum.elim v fun (x : Unit) => Sum.inl a)

@[simp]

theorem DescriptiveComplexity.Pcp.realize_exNewF {A : Type} [FirstOrder.Language.pcp.Structure A] {m : ℕ} {ρ : certBlock.Assignment (A ⊕ Fin m)} {γ : Type} (φ : certLang.Formula (γ ⊕ Unit)) (v : γ → A ⊕ Fin m) : (exNewF φ).Realize v ↔ ∃ (j : Fin m), φ.Realize (Sum.elim v fun (x : Unit) => Sum.inr j)

@[simp]

theorem DescriptiveComplexity.Pcp.realize_allNewF {A : Type} [FirstOrder.Language.pcp.Structure A] {m : ℕ} {ρ : certBlock.Assignment (A ⊕ Fin m)} {γ : Type} (φ : certLang.Formula (γ ⊕ Unit)) (v : γ → A ⊕ Fin m) : (allNewF φ).Realize v ↔ ∀ (j : Fin m), φ.Realize (Sum.elim v fun (x : Unit) => Sum.inr j)

Well-formedness of the instance

The shapes that repeat

The conditions on the certificate

What the kernel says

The assignment a certificate induces

Read back by DescriptiveComplexity.Pcp.certOf, this is the identity definitionally, which is what makes the round trip a rfl.

def DescriptiveComplexity.Pcp.certAssign {A : Type} {m : ℕ} (c : Cert A (Fin m)) : certBlock.Assignment (A ⊕ Fin m)

The assignment a certificate induces.

Equations

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

@[simp]

theorem DescriptiveComplexity.Pcp.certOf_certAssign {A : Type} {m : ℕ} (c : Cert A (Fin m)) : certOf (certAssign c) = c

The theorems

theorem DescriptiveComplexity.pcp_sigmaSONewDefinable : SigmaSONewDefinable PCP

PCP is definable in ∃SO[new]: the invented values are the slots of the sequence of dominoes, and the kernel says that they carry a match – with the common word never written down, only the matching between the two ways of cutting it into blocks.

theorem DescriptiveComplexity.pcp_mem_RE : RE.Mem PCP

PCP is in RE. The certificate is a sequence of dominoes together with a matching between the two parses of the word it spells – a finite object, but no function of the instance bounds its length: that is exactly the difference between Σ₁ and ∃SO[new], and between NP and RE.

theorem DescriptiveComplexity.pcp_le_finsat : Nonempty (RelOrderedFOReduction PCP FINSAT)

PCP first-order-reduces to finite satisfiability. No new hardness work is needed: DescriptiveComplexity.finsat_hard_of_sigmaSONewDefinable is proved for an arbitrary source vocabulary, so putting a problem in RE reduces it to DescriptiveComplexity.FINSAT at once.