Title: Theory / Unimportant / CS / Fundamental / Complexity / Computational complexity of Logical Theories - Ferrante, Rackoff
Tags: fromMath mathToDef mathToSee hasSeenConjDef toBinaryRelation examplesSwitchExample1

Name: Elementary recursive function
Definition: A function computable by a TM in time bounded by fixed composition of exponential functions of the length of the input.
Page: 5
Chapter: 1
Kind: Def

Name: \(N^*\)
Definition: Functions \(N\to N\) with finite support.
Page: 5
Chapter: 1
Kind: Def

Name: A pairing function
Definition: A one-one map \(\rho:N\times N\to N\) and the associated structure \(<N,\rho>\).
Page: 5
Chapter: 1
Kind: Def

Name: Positive integers
Page: 8
Chapter: 1
Section: 2
Notation: I

Definition: The elements of \(F\) at most equal to \(k\)
Page: 8
Chapter: 1
Section: 2
Variables: \(k\in Z\)
\(F\) be \(N\) or \(I\)
Notation: \(F_k\)

Definition: A \(n\)-tuple \((a_1,\dots,a_n)\in \prod^n_{k=1} A_k\)
Page: 8
Chapter: 1
Section: 2
Variables: \(n\in N\), \(A_1,\dots,A_k\) sets.
Notation: \(\overline{a_n}\)

Definition: The projection functions from \( \bigtimes^n_{k=1} A_k\) to \(A_i\).
Page: 8
Chapter: 1
Section: 2
Variables: \(n\in N\),
\(A_1,\dots,A_n\) sets
\(i\in I_n\)
Notation: \(\pi_i\)

Name: The index of \(\sim\)
Definition: The number of equivalence classes of \(\sim\).
Page: 9
Chapter: 1
Section: 2
Variables: \(A\) a set
\(\sim\) an equivalence relation on \(A\)

Q: \([...]=[...]\) [...].
A: k-\text{rep}(n); a_l\dots{}a_0; with \(\sum_{i=0}^lk^ia_i\) and \(a_l\ne 0\)
Page: 9
Chapter: 1
Section: 2
Variables: \(n\in N\), \(k\ge 2\)

If \(n<k^{m+1}\), \(k-\text{rep}(n)=a_m\dots{}a_0\)  with \(\sum_{i=0}^m k^ia_i\).
Page: 10
Chapter: 1
Section: 2
Variables: \(n,m\in N\), \(k\ge 2\)
Kind: Def

Definition: The length of \(w\)
Page: 9
Chapter: 1
Section: 2
Variables: \(w\) a word
Notation: \(\ell w\)

Name: Linearly bounded function \(f:\Sigma^*\to\Delta^*\)
Definition: A function \(f:\Sigma^*\to\Delta^*\) such that there exists \(c\in I\) such that \(\ell n(f(w))\le c\ell n(w)\) for all \(w\in \Sigma^+\)
Page: 16
Chapter: 1
Section: 4
Index: 2
Kind: Def

Name: polylin
Definition: TIME-SPACE\((n^{O(1)},n)\)
Page: 16
Chapter: 1
Section: 4
Kind: Def

Page: 16
Definition: \(w\in A\iff f(w)\in B\), \(f\) is logspace and linear bounded.
Chapter: 1
Section: 4
Variables: \(A\subseteq\Sigma^+,B\subseteq\Delta^+\) two languages and \(f:\Sigma^+\to\Delta^+\)
Notation: \(A\le_{log-lin}B\) via \(f\)
Kind: Def

Page: 16
Definition: \(w\in A\iff f(w)\in B\), \(f\) is polylin and linear bounded.
Chapter: 1
Section: 4
Variables: \(A\subseteq\Sigma^+\)
\(B\subseteq\Delta^+\) two languages
\(f:\Sigma^+\to\Delta^+\)
Notation: \(A\le_{p\ell}B\) via \(f\)
Kind: Def

Name: \(q\)-depth of \(F\)
Definition: The quantifier depth of \(F\).
Page: 24
Chapter: 1
Section: 5
Variables: \(F\) a formula
Index: 4
Kind: Def

Name: A norm of \(x\)
Definition: A representation of \(x\) as a finite word, or \(\infty\).
Page: 29
Chapter: 2
Section: 1
Variables: \(x\) a structure or an element belonging to a structure.
Notation: \(||x||\)
Index: 4
Kind: Def

Smaller0: \(A\) is \(H\)-bounded
Greater0: \((Q_1 x_1\le m_1)\dots(Q_k x_k\le m_k) F(\overline x_k)\) with \(H(n+k-i,i-1,m_{i-1})\le m_i\)
Page: 30
Chapter: 2
Section: 1
Variables: \(A\) a structure and \(H:N\times N\times (\Sigma^*\cup\{\infty\})\to \Sigma^*\cup\{\infty\}\)
Kind: Theo
Hide middle: yes
Prefix Greater: \(Q_1 x_1\dots Q_kx_ k F(\overline x_k)\) is equivalent to
Extra: n ?

Q: [...] means [...].
A: \((A,\overline a_k)\equiv_{n,k}(B,\overline b_k)\); for all formulas \(F(\overline x_k)\) of q-depth at most \(n\), \((A,\overline a_k)\) satisfies \(F\) iff \((B,\overline b_k)\) satisfies \(F\)
Page: 33
Chapter: 2
Section: 1
Variables: \(n,k\in N\)
\(C\) a class of structure
\(A,B\in C\)
\(\overline a_k\in A^k\)
\(\overline b_k\in B^k\).
Kind: Def

Page: 33
Definition: \((A,\overline a_k)\equiv_{n,k}(B,\overline b_k)\)
Chapter: 2
Section: 1
Variables: \(n,k\in N\),
\(\mathbf C\) a class of structure,
\(A,B\in C\),
\(\overline a_k\in A^k\),
\(\overline b_k\in B^k\).
Notation: \(\overline a_k\equiv_{n}\overline b_k\)
Equivalence: An equivalence relation on the class \(\mathcal C\)

Smaller0: \((A,\overline a_k)\equiv _{n+1}(B,\overline b_k)\)
Greater0: -for every \(a_{k+1}\in A\), there exists some \(b_{k+1}\in B\) such that \((A,\overline a_{k+1})\equiv_n(B,\overline b_{k+1})\)
and
--for every \(b_{k+1}\in B\), there exists some \(a_{k+1}\in A\) such that \((A,\overline a_{k+1})\equiv_n(B,\overline b_{k+1})\)
Page: 34
Chapter: 2
Section: 1
Variables: \(n,k\in N\),
\(\mathbf C\) a class of structure,
\(A,B\in C\),
\(\overline a_k\in A^k\), \(\overline b_k\in B^k\).
Kind: Theo
Smaller to greater: iff
Hide middle: yes

Smaller0: \((A,\overline a_k)E_{0,k}(B,\overline b_k)\implies(A,\overline a_k)\equiv_{0}(B,\overline b_k)\)
Greater0: -\((A,\overline a_k)E_{n,k}(B,\overline b_k)\) implies \((A,\overline a_k)\equiv_{n}(B,\overline b_k)\) for every \(n,k\in N\), \(A,B\in\mathcal C\) and
-Every structure in \(\mathcal C\) is \(H\)-bounded
Page: 34
Chapter: 2
Section: 1
Variables: \(\mathcal C\) a class of structure,
\(H:N\times N\times (\Sigma^*\cup\{\infty\})\to \Sigma^*\cup\{\infty\}\),
\((E_{n,k})\) be equivalence relations on pairs \((A,\overline a_k)\).
Index: 3
Kind: Theo
Smaller to greater: implies
Hide middle: yes
Smaller1: if \((A,\overline a_k)E_{n+1,k} (B,\overline b_k)\), \(1\le i\le k\), then for all \(a_{k+1}\in A\) there exists a \(b_{k+1}\in B\) such that \(b_{k+1}\le H(n,k,\max b_i)\) and \((A,\overline a_{k+1}) E_{n,k+1}(B,\overline b_{k+1})\)
Greater to smaller: is implied by
Prefix Smaller: for all \(A,B\in C\), \(\overline a_k\in A^k\), \(\overline b_k\in B^k\)

Q: If [...]
then: [...].
A: -\(\mathcal C\) is \(H\)-bounded,
-for every \(n\in N^+\), \(A\in\mathcal C\), there is some structure \(A'\in \mathcal C\) such that \(A' E_{n,0} A\) and \(||A'||\le h(n)\); -\(\mathcal C\) is \((h,H)\)-bounded
Page: 36
Chapter: 2
Section: 1
Variables: \(\mathbf C\) a class of structure,
\(H:N\times N\times (\Sigma^*\cup\{\infty\})\to \Sigma^*\cup\{\infty\}\),
\(h:N\to \Sigma^*\cup\{\infty\}\),
\((E_{n,k})\) be equivalence relations on pairs \((A,\overline a_k)\).
Index: 4
Kind: Theo

Name: The theory of \(A\)
Definition: The set of \(\tau\)-sentences satisfied by \(A\).
Page: 22
Chapter: 1
Section: 5
Variables: \(\tau\) a vocabulary
\(A\) a \(\tau\)-structure
Abbreviation: \(\text{TH}(A)\)

Name: A sentence satisfiable in \(C\)
Definition: A sentence \(F\) such that there is some \(A\in \mathcal C\) which satisfies \(F\).
Page: 22
Chapter: 1
Section: 5
Variables: \(\tau\) a vocabulary, \(\mathcal C\) a set of \(\tau\)-structure

Definition: The set of \(\tau\)-sentences satisfiable in \(\mathcal C\).
Page: 22
Chapter: 1
Section: 5
Variables: \(\tau\) a vocabulary, \(\mathcal C\) a set of \(\tau\)-structure.
Notation: \(\texttt{SAT}(\mathcal C)\)

Name: The theory of \(\mathcal C\)
Definition: The set of \(\tau\)-sentences satisfied by every model of \(\mathcal C\).
Page: 22
Chapter: 1
Section: 5
Variables: \(\tau\) a vocabulary,
\(\mathcal C\) a set of \(\tau\)-structure.
Abbreviation: \(\texttt{TH}(\mathcal C)\)

Smaller0: \(A\) and \(B\) are equivalent on every atomic formulas
Greater0: they are \(\cong_0\)-equivalent
Page: 37
Chapter: 2
Section: 1
Variables: \(\tau\) a vocabulary,
\((A,\overline a_k),(B,\overline b_k)\) two \(\tau\)-structures with \(k\) constants
Index: 5
Kind: Lem
Hide middle: yes

Definition: The number of \(\equiv_{n,k}\) equivalence classes.
Page: 38
Chapter: 2
Section: 1
Variables: \(\tau\) a vocabulary, \(\mathcal C\) a class of \(\tau\)-structures , \(n,k\in N\).
Notation: \(M(n,k)\)
Index: 7
Kind: Def

Question: \(M(n,k)\) is
Answer: at most \(2^{\dots^{2^{(n+k)^c} } } \) with height \(n+1\) and some constant \(c\).
Page: 38
Chapter: 2
Section: 1
Variables: \(\tau\) a vocabulary, \(\mathcal C\) a class of \(\tau\)-structures , \(n,k\in N\)
Index: 8
Kind: Lem

Name: Structure with \(M(n,k)\) bounded above by an elementary recursive function and undecidable theory
Page: 45
Chapter: 2
Example: For \(S\subseteq\mathbb N\), let \(\tilde S\) an equivalence relation on \(N\) that contains at most one class of each size, and \(0\) class of size \(i\) if \(i\not\in S\). The structure \(A_S=<N,=,\tilde S,0>\)

Name: \((h,H)\) bounded structure
Definition: if \(F\) is a sentence of q-depth \(\le n\), then \(F\in\text{ SAT}(\mathcal C)\iff F\) is true in some structure in \(\mathcal C\) of norm \(\le h(n)\) and
Page: 32
Chapter: 2
Section: 1
Variables: \(h:N\to \Sigma^*\cup\{\infty\}\),
\(H:N\times N\times (\Sigma^*\cup\{\infty\})\to \Sigma^*\cup\{\infty\}\)
Kind: Def
Definition2: for every \(A\in \mathcal C\), \(A\) is \(H\)-bounded.
Conjdef: A structure \(\mathcal C\) such that for every \(n\in N\)

Name: \(H\)-bounded structure
Definition: for every \(n,k\in N\),
Page: 30
Chapter: 2
Section: 1
Variables: \(H:N\times N\times (\Sigma^*\cup\{\infty\})\to \Sigma^*\cup\{\infty\}\)
Kind: Def
Definition2: \(m\in\Sigma^*\cup\{\infty\}\),
Conjdef: A structure \(A\) such that
Definition3: \(\overline a_K\in A^K\) with \(a_i\le m\),
Definition4: and formula \(F(\overline x_{k+1})\) of q-depth \(\le n\), the following is true:
Definition5: if \((A,\overline a_k)\) satisfies \(\exists x_{k+1}F(\overline x_{k+1})\),
Definition6: there exists \(a_{k+1}\le H(n,k,m)\),
Definition7: \((A,\overline a_{k+1})\) satisfies \(F(\overline x_{k+1})\).
Hide remaining def: yes