Title: Theory / Unimportant / CS / Fundamental / Automata / Finite / Pin{ / B Historical results / 09 Logic;
Tags: counterExample récupéré

Name: Omitted
Definition: Logic
Page: 269
Chapter: XVII
Section: 1
Kind: Lem

Definition: \(A\times\{0,1\}^p\times\{0,1\}^q\)
Page: 168
Chapter: IX
Section: 3
Variables: \(A\) an alphabet,
\(p,q\in\mathbb N\)
Notation: \(B_{p,q}\)
Notation2: \(B\)

Name: A marked word
Definition: \((u_0,\dots,u_{p+q})\in B_{p,q}^*\) in which each \(u_1,\dots,u_p\) contains exactly one 1
Page: 168
Chapter: IX
Section: 3
Variables: \(A\) an alphabet,
\(p,q\in\mathbb N\)
Intuition: First element is the word.
Second element correspond to first-order variable
Elements from \(p+1\) to \(p+q\) corresponds to second-order variables

Definition: The set of marked words
Page: 167
Chapter: IX
Section: 3
Variables: \(A\) an alphabet,
\(p,q\in\mathbb N\)
Notation: \(K_{p,q}\)
Index: , 7
Kind: , Prop
Typ: Star-free language
Notation2: \(K\)

Definition: \((b_0,\dots, b_{i-1},b_{i+1},\dots, b_{p+q})\)
Page: 170
Chapter: IX
Section: 3
Variables: \(A\) an alphabet,
\(w=(b_0,\dots,b_{p+q})\in K_{p,q}\),
\(0\le i\le p+q\)
Notation: \(\pi_i(w)\)

Definition: the position of \(b_j\) whose value is \(1\)
Page: 170
Chapter: IX
Section: 3
Variables: \(A\) an alphabet,
\(w=(b_0,\dots,b_{p+q})\in K_{p,q}\),
\(x_j\) a first-order variable
Notation: \(\nu(x_j)\)

Definition: The set of positions of \(b_{p+j}\) equal to \(1\)
Page: 170
Chapter: IX
Section: 3
Variables: \(A\) an alphabet,
\(w=(b_0,\dots,b_{p+q})\in K_{p,q}\),
\(X_j\) a second-order variable
Notation: \(\nu(X_j)\)
Index: 9
Kind: Prop

Definition: The set of \(u\in K_{p,q}\) such that \(u\) satisfies \(\phi(x_1,\dots,x_p,X_1,\dots,X_q)\)
Page: 170
Chapter: IX
Section: 3
Variables: \(A\) an alphabet,
\(\phi(x_1,\dots,x_p,X_1,\dots,X_q)\) a MSO formula
Notation: \(S_{p,q}(\phi)\)
Kind: Prop

Smaller0: \(S_{p,q}(\bigvee\phi_i)\)
Greater0: \(\bigcup S_{p,q}(\phi_i)\)
Page: 169
Chapter: XI
Section: 3
Variables: \(A\) an alphabet
\(\phi_i\) a sequence of formula over \(A\)
Index: 8
Kind: Prop
Smaller to greater: =
Context: Variety

Smaller0: \(S_{p,q}(\bigwedge\phi_i)\)
Greater0: \(\bigcap S_{p,q}(\phi_i)\)
Page: 169
Chapter: XI
Section: 3
Variables: \(A\) an alphabet
\(\phi_i\) a sequence of formula over \(A\)
Index: 8
Kind: Prop
Smaller to greater: =

Smaller0: \(S_{p,q}(\neg\phi)\)
Greater0: \(K_{p,q}\setminus\bigcap S_{p,q}(\phi)\)
Page: 169
Chapter: XI
Section: 3
Variables: \(A\) an alphabet
\(\phi\) a formula over \(A\)
Index: 8
Kind: Prop
Smaller to greater: =

Definition: the set of \(b\in B_{p,q}\) such that \(b_j=1\) and \(b_0=a\)
Page: 169
Chapter: XI
Section: 3
Variables: \(A\) an alphabet
\(a\in A\),
\(p,q\in\mathbb N\)
\(1\le j\le p+q\)
Notation: \(C_{j,a}\)
Index: 9
Kind: Prop

Definition: the set of \(b\in B_{p,q}\) such that \(b_i=b_j=1\)
Page: 169
Chapter: XI
Section: 3
Variables: \(A\) an alphabet
\(p,q\in\mathbb N\)
\(1\le i,j\le p+q\)
Notation: \(C_{i,j}\)
Index: 9
Kind: Prop

Definition: the set of \(b\in B_{p,q}\) such that \(b_i=1\)
Page: 169
Chapter: XI
Section: 3
Variables: \(A\) an alphabet
\(a\in A\),
\(p,q\in\mathbb N\)
\(1\le i\le p+q\)
Notation: \(C_{i}\)
Index: 9
Kind: Prop

Smaller0: \(S_{p,q}(\mathrm a(x_i))\)
Greater0: \(K_{p,q}\cap B^*C_{i,a}B^*\)
Page: 169
Chapter: XI
Section: 3
Variables: \(A\) an alphabet
\(a\in A\),
\(p,q\in\mathbb N\)
\(1\le i\le q\)
Index: 9
Kind: Prop
Smaller to greater: =

Smaller0: \(S_{p,q}(x_i=x_j)\)
Greater0: \(K_{p,q}\cap B^*C_{i,j}B^*\)
Page: 169
Chapter: XI
Section: 3
Variables: \(A\) an alphabet
\(p,q\in\mathbb N\)
\(1\le i,j\le q\)
Index: 9
Kind: Prop
Smaller to greater: =

Smaller0: \(S_{p,q}(x_i<x_j)\)
Greater0: \(K_{p,q}\cap B^*C_{i}B^*C_{j}B^*\)
Page: 169
Chapter: XI
Section: 3
Variables: \(A\) an alphabet
\(p,q\in\mathbb N\)
\(1\le i,j\le q\)
Index: 9
Kind: Prop
Smaller to greater: =

Smaller0: \(S_{p,q}(X_i(x_j))\)
Greater0: \(K_{p,q}\cap B^*C_{i+p,j}B^*\)
Page: 169
Chapter: XI
Section: 3
Variables: \(A\) an alphabet
\(p,q\in\mathbb N\)
\(1\le j\le q\)
\(1\le i\le p\)
Index: 9
Kind: Prop
Smaller to greater: =

Smaller0: \(S_{p-1,q}(\exists x_p\phi)\)
Greater0: \(\pi_{p}(S_{p,q}(\phi))\)
Page: 169
Chapter: XI
Section: 3
Variables: \(A\) an alphabet
\(p,q\in\mathbb N\)
\(1\le j\le q\)
\(1\le i\le p\)
\(\phi(x_1,\dots,x_q,X_1,\dots,X_p)\) a formula
Index: 9
Kind: Prop
Smaller to greater: =

Smaller0: \(S_{p,q-1}(\exists X_p\phi)\)
Greater0: \(\pi_{p+q}(S_{p,q}(\phi))\)
Page: 170
Chapter: XI
Section: 3
Variables: \(A\) an alphabet
\(p,q\in\mathbb N\)
\(1\le j\le q\)
\(1\le i\le p\)
\(\phi(x_1,\dots,x_p,X_1,\dots,X_q)\) a formula
Index: 10
Kind: Prop
Smaller to greater: =

Name: Existential formula
Definition: The set of formulas of the form \(\exists x_1\dots x_k\phi\) with \(\phi\) quantifier free
Page: 172
Chapter: IX
Section: 4.2
Notation: \(\Sigma_1\)

Name: A stutter invariant language
Definition: \(a\sim_La^2\)
Page: 172
Chapter: IX
Section: 5
Variables: \(A\) an alphabet
Context: A language such that, for each letter \(a\in A\)
Definition2: \(xay\in L\iff xaay\in L\) for each words \(x,y\)

Name: An elementary stutter invariant language
Definition: A language of the form \(A^*a_1A^*a_2\dots A^*a_kA^*\) with each \(a_i\) distinct
Page: 173
Chapter: IX
Section: 5
Variables: \(A\) an alphabet