Existential second-order layout of framed structure encodings

On the canonical power structure (Fin B, v.powerStructure a B) for a well-formed input a : EncodedStructure with (frame (encStructure a)).length < B, the Cook–Levin tableau needs the input tape word u = frame (encStructure a) and its length u.length as unary predicates on Fin B.

Because encStructure a = frame (encUnary a.1) ++ (a.2.flatMap frame) and u = frame (encStructure a), every stage of the binary encoding is an application of Turing.MultiTapeTM.frame at some starting offset base. We therefore axiomatize a single stride-2 framing step (FO.frameChunkSentence) in first-order logic using the linear order powerLt on Fin B:

• given a domain formula inDom(j) (j < w.length), a bit formula inBit(j) (w[j] = true), and a unary relation baseRel holding of {base},
• a binary relation mapRel(j, p) tracks p = base + 2 * j for j ≤ w.length, writing true at base + 2 * j and w[j] at base + 2 * j + 1 into outBitRel, and writing the terminator false at base + 2 * w.length while advancing nextBaseRel to {base + 2 * w.length + 1}.

Chaining v.count + 1 instances of frameChunkSentence reconstructs encStructure a and its length, and one final instance reconstructs frame (encStructure a) and its length.

Main definitions

• Cslib.Logic.FO.frameChunkSentence: the first-order sentence axiomatizing a single stride-2 framing step on Fin B.
• Cslib.Logic.Vocabulary.inputVarLanguage: the two unary relation symbols uBitSym and uLenSym representing the framed input word u = frame (encStructure a) and its length on Fin B.
• Cslib.Logic.Vocabulary.layoutESOSentence: the existential second-order sentence over v.powerLanguage.sum inputVarLanguage characterizing u and u.length.

Main results

• Cslib.Logic.FO.nextBase_and_getElem?_frame_of_realize_frameChunkSentence, Cslib.Logic.FO.realize_frameChunkSentence_of_canonical: soundness and completeness of frameChunkSentence on Fin B.
• Cslib.Logic.Vocabulary.realize_layoutESOSentence: for well-formed a with (frame (encStructure a)).length < B, v.layoutESOSentence holds on Fin B iff uLenSym holds solely of (frame (encStructure a)).length and uBitSym agrees with frame (encStructure a) below (frame (encStructure a)).length.

References

• R. Fagin, Generalized first-order spectra and polynomial-time recognizable sets
• N. Immerman, Descriptive Complexity

Generic stride-2 framing sentence

noncomputable def Cslib.Logic.FO.frameChunkSentence {L' : FirstOrder.Language} (r : L'.Relations 2) (inDom inBit : L'.Formula (Fin 1)) (baseRel nextBaseRel : L'.Relations 1) (mapRel : L'.Relations 2) (outBitRel : L'.Relations 1) : L'.Sentence

The first-order sentence axiomatizing a single stride-2 framing step on Fin B: starting at baseRel, the binary relation mapRel(j, p) maps j ≤ w.length to base + 2 * j, writes [true, w[j]] into outBitRel at base + 2 * j and base + 2 * j + 1, writes the terminator false at base + 2 * w.length, and sets nextBaseRel to {base + 2 * w.length + 1}.

theorem Cslib.Logic.FO.nextBase_and_getElem?_frame_of_realize_frameChunkSentence {L' : FirstOrder.Language} {B : ℕ} [L'.Structure (Fin B)] {r : L'.Relations 2} (hlt : ∀ (x : Fin 2 → Fin B), FirstOrder.Language.Structure.RelMap r x ↔ x 0 < x 1) {inDom inBit : L'.Formula (Fin 1)} {baseRel nextBaseRel : L'.Relations 1} {mapRel : L'.Relations 2} {outBitRel : L'.Relations 1} {w : List Bool} {base : ℕ} (hbound : base + (Turing.MultiTapeTM.frame w).length < B) (hdom : ∀ (j : Fin B), inDom.Realize ![j] ↔ ↑j < w.length) (hbit : ∀ (j : Fin B), ↑j < w.length → (inBit.Realize ![j] ↔ w[↑j]? = some true)) (hbase : ∀ (z : Fin B), FirstOrder.Language.Structure.RelMap baseRel ![z] ↔ ↑z = base) (hreal : Fin B ⊨ frameChunkSentence r inDom inBit baseRel nextBaseRel mapRel outBitRel) : (∀ (z : Fin B), FirstOrder.Language.Structure.RelMap nextBaseRel ![z] ↔ ↑z = base + (Turing.MultiTapeTM.frame w).length) ∧ ∀ (p : Fin B), base ≤ ↑p → ↑p < base + (Turing.MultiTapeTM.frame w).length → (FirstOrder.Language.Structure.RelMap outBitRel ![p] ↔ (Turing.MultiTapeTM.frame w)[↑p - base]? = some true)

Soundness of frameChunkSentence: when baseRel holds solely of base and base + (frame w).length < B, any realization of frameChunkSentence forces nextBaseRel to hold solely of base + (frame w).length and outBitRel to agree with frame w on [base, base + (frame w).length).

theorem Cslib.Logic.FO.realize_frameChunkSentence_of_canonical {L' : FirstOrder.Language} {B : ℕ} [L'.Structure (Fin B)] {r : L'.Relations 2} (hlt : ∀ (x : Fin 2 → Fin B), FirstOrder.Language.Structure.RelMap r x ↔ x 0 < x 1) {inDom inBit : L'.Formula (Fin 1)} {baseRel nextBaseRel : L'.Relations 1} {mapRel : L'.Relations 2} {outBitRel : L'.Relations 1} {w : List Bool} {base : ℕ} (hbound : base + (Turing.MultiTapeTM.frame w).length < B) (hdom : ∀ (j : Fin B), inDom.Realize ![j] ↔ ↑j < w.length) (hbit : ∀ (j : Fin B), ↑j < w.length → (inBit.Realize ![j] ↔ w[↑j]? = some true)) (hbase : ∀ (z : Fin B), FirstOrder.Language.Structure.RelMap baseRel ![z] ↔ ↑z = base) (hnext : ∀ (z : Fin B), FirstOrder.Language.Structure.RelMap nextBaseRel ![z] ↔ ↑z = base + (Turing.MultiTapeTM.frame w).length) (hmap : ∀ (j p : Fin B), FirstOrder.Language.Structure.RelMap mapRel ![j, p] ↔ ↑j ≤ w.length ∧ ↑p = base + 2 * ↑j) (hout : ∀ (p : Fin B), base ≤ ↑p → ↑p < base + (Turing.MultiTapeTM.frame w).length → (FirstOrder.Language.Structure.RelMap outBitRel ![p] ↔ (Turing.MultiTapeTM.frame w)[↑p - base]? = some true)) : Fin B ⊨ frameChunkSentence r inDom inBit baseRel nextBaseRel mapRel outBitRel

Completeness of frameChunkSentence: the canonical stride-2 relation mapRel(j, p) ↔ j ≤ w.length ∧ p = base + 2 * j satisfies frameChunkSentence whenever baseRel is {base}, nextBaseRel is {base + (frame w).length}, and outBitRel agrees with frame w on [base, base + (frame w).length).

Prefix decomposition of encStructure a

def Cslib.Logic.Vocabulary.encStructurePrefix {L : FirstOrder.Language} (v : Vocabulary L) (a : EncodedStructure) (m : ℕ) : List Bool

The prefix of encStructure a consisting of frame (encUnary a.1) followed by the framed truth tables of the first m relation symbols of v.

@[simp]

theorem Cslib.Logic.Vocabulary.encStructurePrefix_zero {L : FirstOrder.Language} (v : Vocabulary L) (a : EncodedStructure) : v.encStructurePrefix a 0 = Turing.MultiTapeTM.frame (Turing.MultiTapeTM.encUnary a.1)

theorem Cslib.Logic.Vocabulary.encStructurePrefix_succ {L : FirstOrder.Language} (v : Vocabulary L) (a : EncodedStructure) (i : Fin v.count) : v.encStructurePrefix a (↑i + 1) = v.encStructurePrefix a ↑i ++ Turing.MultiTapeTM.frame (v.table a (v.symbol i))

theorem Cslib.Logic.Vocabulary.encStructurePrefix_count {L : FirstOrder.Language} (v : Vocabulary L) {a : EncodedStructure} (ha : v.WellFormed a) : v.encStructurePrefix a v.count = encStructure a

theorem Cslib.Logic.Vocabulary.length_encStructurePrefix {L : FirstOrder.Language} (v : Vocabulary L) {a : EncodedStructure} {m : ℕ} (hm : m ≤ a.2.length) (hmc : m ≤ v.count) : (v.encStructurePrefix a m).length = tableStart a m

The prefix through the first m tables ends where the table at position m starts (Cslib.Logic.tableStart).

The input variable language and layout ESO sentence

@[reducible, inline]

abbrev Cslib.Logic.Vocabulary.inputVarLanguage : FirstOrder.Language

The language of the two unary relations exposed by layoutESOSentence to the Cook–Levin tableau:

• false (uBitSym): bit p of u = frame (encStructure a), and
• true (uLenSym): the singleton {u.length}.

def Cslib.Logic.Vocabulary.uBitSym : inputVarLanguage.Relations 1

The unary relation symbol uBit(p) in inputVarLanguage.

def Cslib.Logic.Vocabulary.uLenSym : inputVarLanguage.Relations 1

The unary relation symbol uLen(p) in inputVarLanguage.

@[reducible, inline]

abbrev Cslib.Logic.Vocabulary.LayoutVar (count : ℕ) : Type

The index type of internal relation variables quantified by v.layoutESOSentence:

• .inl (.inl m) (m : Fin (v.count + 2)): unary base_m,
• .inl (.inr ()): unary rawBit,
• .inr (.inl m) (m : Fin (v.count + 1)): binary chunkMap_m,
• .inr (.inr ()): binary outerMap.

def Cslib.Logic.Vocabulary.layoutArity (count : ℕ) : LayoutVar count → ℕ

The arities of LayoutVar: 1 on the left summand and 2 on the right summand.

@[reducible, inline]

abbrev Cslib.Logic.Vocabulary.layoutMatrixLanguage {L : FirstOrder.Language} (v : Vocabulary L) : FirstOrder.Language

The combined language of v.layoutESOSentence's first-order matrix.

def Cslib.Logic.Vocabulary.layoutLt {L : FirstOrder.Language} (v : Vocabulary L) : v.layoutMatrixLanguage.Relations 2

Binary < inside v.layoutMatrixLanguage.

def Cslib.Logic.Vocabulary.layoutIsElem {L : FirstOrder.Language} (v : Vocabulary L) : v.layoutMatrixLanguage.Relations 1

Unary < n inside v.layoutMatrixLanguage.

def Cslib.Logic.Vocabulary.layoutInTable {L : FirstOrder.Language} (v : Vocabulary L) (i : Fin v.count) : v.layoutMatrixLanguage.Relations 1

Unary < n ^ v.arity i inside v.layoutMatrixLanguage.

def Cslib.Logic.Vocabulary.layoutTableBit {L : FirstOrder.Language} (v : Vocabulary L) (i : Fin v.count) : v.layoutMatrixLanguage.Relations 1

Unary relation table bit i inside v.layoutMatrixLanguage.

def Cslib.Logic.Vocabulary.layoutUBit {L : FirstOrder.Language} (v : Vocabulary L) : v.layoutMatrixLanguage.Relations 1

Unary uBit inside v.layoutMatrixLanguage.

def Cslib.Logic.Vocabulary.layoutULen {L : FirstOrder.Language} (v : Vocabulary L) : v.layoutMatrixLanguage.Relations 1

Unary uLen inside v.layoutMatrixLanguage.

def Cslib.Logic.Vocabulary.layoutBase {L : FirstOrder.Language} (v : Vocabulary L) (m : Fin (v.count + 2)) : v.layoutMatrixLanguage.Relations 1

Unary base_m (m : Fin (v.count + 2)) inside v.layoutMatrixLanguage.

def Cslib.Logic.Vocabulary.layoutRawBit {L : FirstOrder.Language} (v : Vocabulary L) : v.layoutMatrixLanguage.Relations 1

Unary rawBit inside v.layoutMatrixLanguage.

def Cslib.Logic.Vocabulary.layoutChunkMap {L : FirstOrder.Language} (v : Vocabulary L) (m : Fin (v.count + 1)) : v.layoutMatrixLanguage.Relations 2

Binary chunkMap_m (m : Fin (v.count + 1)) inside v.layoutMatrixLanguage.

def Cslib.Logic.Vocabulary.layoutOuterMap {L : FirstOrder.Language} (v : Vocabulary L) : v.layoutMatrixLanguage.Relations 2

Binary outerMap inside v.layoutMatrixLanguage.

noncomputable def Cslib.Logic.Vocabulary.layoutInRaw {L : FirstOrder.Language} (v : Vocabulary L) : v.layoutMatrixLanguage.Formula (Fin 1)

The domain formula j < rawLen for the outer framing step (base_{v.count + 1} is rawLen).

noncomputable def Cslib.Logic.Vocabulary.layoutMatrix {L : FirstOrder.Language} (v : Vocabulary L) : v.layoutMatrixLanguage.Sentence

The first-order matrix of v.layoutESOSentence:

1. base_0 holds solely of 0,
2. chunk 0 frames encUnary a.1 (inDom = powerIsElem, inBit = ⊤) from base_0 to base_1 into rawBit,
3. for each i : Fin v.count, chunk i + 1 frames table i (inDom = powerInTable i, inBit = powerTableBit i) from base_{i + 1} to base_{i + 2} into rawBit, and
4. the outer chunk frames encStructure a (inDom = layoutInRaw, inBit = rawBit) from base_0 to uLen into uBit.

noncomputable def Cslib.Logic.Vocabulary.layoutESOSentence {L : FirstOrder.Language} (v : Vocabulary L) : ESO.Sentence (v.powerLanguage.sum inputVarLanguage)

The existential second-order sentence over v.powerLanguage.sum inputVarLanguage that forces uLenSym to hold solely of (frame (encStructure a)).length and uBitSym to agree with frame (encStructure a) below (frame (encStructure a)).length.

theorem Cslib.Logic.Vocabulary.realize_layoutESOSentence {L : FirstOrder.Language} (v : Vocabulary L) {a : EncodedStructure} (ha : v.WellFormed a) {B : ℕ} (hB : (Turing.MultiTapeTM.frame (encStructure a)).length < B) (I_in : (b : Bool) → Set (Fin ((fun (x : Bool) => 1) b) → Fin B)) : v.layoutESOSentence.Realize (Fin B) ↔ (∀ (z : Fin B), ![z] ∈ I_in true ↔ ↑z = (Turing.MultiTapeTM.frame (encStructure a)).length) ∧ ∀ (p : Fin B), ↑p < (Turing.MultiTapeTM.frame (encStructure a)).length → (![p] ∈ I_in false ↔ (Turing.MultiTapeTM.frame (encStructure a))[↑p]? = some true)

Characterization of layoutESOSentence: on (Fin B, v.powerStructure a B) for a well-formed input a with (frame (encStructure a)).length < B, an interpretation I_in of inputVarLanguage satisfies v.layoutESOSentence iff I_in true (uLenSym) holds solely of (frame (encStructure a)).length and I_in false (uBitSym) agrees with frame (encStructure a) on all positions < (frame (encStructure a)).length.