Title: Theory / Unimportant / CS / Fundamental / Complexity / Descriptive complexity+14 / Inductive Definition
Tags: fromMath mathToDef mathToSee equivalentHand

Name: A monotone map from relation to relation
Definition: A relation \(\phi\) such that, for all \(S\subseteq T\), \(\phi^\mathcal{A}(S)\subseteq\phi^\mathcal{A}(T)\).
Page: 58
Chapter: 4
Section: 1
Variables: \(R\) a relation symbol.

Smaller0: Least fixed point of \(\phi^{\mathcal A}\)
Greater0: \(\left(\phi^{\mathcal A}\right)^r(\emptyset)\), such that \(\left(\phi^{\mathcal A}\right)^r(\emptyset)=\left(\phi^{\mathcal A}\right)^{r+1}(\emptyset)\)
Page: 59
Chapter: 4
Section: 1
Variables: \(R\) be a relation variable of arity \(k\)
\(\phi(R,x_1,\dots,x_k)\)
\(\mathcal A\) a structure.
Index: 5
Kind: Def
Smaller to greater: equals
Hide middle: yes
Assuming: \(R\) is monotone
Greater1: \(r\) is at most the cardinal power \(k\)
Connect Smaller0: .

Definition: \(FO[\tau]\) with the least-fixed point operator.
Page: 59
Chapter: 4
Section: 1
Notation: \(FO(LFP)[\tau]\)
Index: 5
Kind: Def

Name: The least fixed point of \(\phi\) in the model \(\mathcal A\)
Definition: The least set \(R\) such that \(\phi(R)^{\mathcal A}=R^{\mathcal A}\).
Page: 59
Chapter: 4
Section: 1
Variables: \(R\) be a relation symbol of arity \(k\)
\(\phi(R,x_1,\dots,x_k)\) a monotone formula.
Notation: \((LFP_{Rx}\phi)\)
Index: 5
Kind: Def

Smaller0: \(FO(LFP)[\tau,<]\)
Greater0: \(P\)
Page: 60
Chapter: 4
Section: 1
Variables: \(\tau\) a finite structure
Index: 10
Smaller to greater: =
Hide middle: yes

Q: \(FO(LFP)[<,\tau]\) admits a normal form of the form [...].
A: \(LFP(\phi_{R,x})(y)\) with \(\phi\in FO[<,\tau]\)
Page: 61
Chapter: 4
Section: 1
Index: 11
Kind: Cor

Name: The depth of \(\phi\)
Definition: The number of iterations until the inductive definition \(\phi\) closes.
Page: 61
Chapter: 4
Section: 2
Variables: \(\phi\) an inductive definition
Name2: The closure ordinal of \(\phi\)

Q: [...]
A: the sublanguage of \(FO(LFP)[\tau]\) in wich only fixed point of depth at most \(f(n)\) are included.
Page: 62
Chapter: 4
Section: 2
Index: 16
Kind: Def
Q: [...]
A: \(IND[f(n)][\tau]\)

Smaller0: \(FO[t(n)]\)
Greater0: there exists quantifier free formulas \(M_i\) from \(\mathcal L(\tau)\), a tuple \(c\) of constants and a quantifier block
\[QB=[(Q_1 x_1. M_1)\dots (Q_kx_k. M_k)]\] such that for all \(\mathcal A\in STRUC[\tau]\),
\[\mathcal A\in S\iff \mathcal A\models ([QB]^{t(\parallel A\parallel)}M_0)(c/x)\]
Page: 65
Chapter: 4
Section: 3
Variables: \(t:\mathbb N\to\mathbb N\)
\(S\subseteq STRUC[\tau]\)
Index: 24
Kind: Def
Smaller to greater: iff
Hide middle: yes
Prefix Smaller: \(S\) is a member of

Smaller0: FO(DTC)
Greater0: L
Page: 144
Chapter: 9
Section: 2
Index: 11
Kind: Theo
Smaller to greater: is equal to
Hide middle: yes

Q: [...] are [property].
A: FO(pos TC) and FO(DTC); equivalent to a formula in the same logic with a single application of the operator to quantifier-free formula
Page: 144
Chapter: 9
Section: 3
Variables: \(\tau\) a vocabulary
Index: 12, 15
Kind: Lem
Assuming: \(\tau\) contains the successor relation

Q: BIT is definable in:
-[...]
-[...]
A: FO [+,×]; FO(DTC)[+1]
Page: 147
Chapter: 9
Section: 3
Index: 16
Kind: Prop
Extra: et page 14

Q: [...].
A: The smallest class containing constant, successor, projection, input symbols, closed under composition and primitive recursion
Page: 148
Chapter: 9
Section: 4
Name: The class of primitive recursive function

Smaller0: co-NL
Greater0: FO(pos TC)
Page: 149
Chapter: 9
Section: 5
Index: 20, 22, 23
Kind: Theo, Cor
Smaller to greater: equals
Smallest: NL
Greatest: FO(TC)

Name: A formula in conjunctive normal form
Definition: \((Q_1P_1^{a_1})\dots(Q_kP_k^{a_k})(\forall \overline x)\bigwedge_{i}\bigvee_j \alpha_{i,j}\), with \(\alpha_{i,j}\) atomic
Page: 151
Chapter: 9
Section: 6
Index: 26
Kind: Def

Name: A Horn formula
Definition: A formula of the form \((Q_1P_1^{a_1})\dots(Q_kP_k^{a_k})(\forall \overline x)\bigwedge_{i}\alpha_{i,0}\lor\bigvee_j \neg\alpha_{i,j}\), with \(\alpha_{i,j}\) positive atomic or false.
Page: 151
Chapter: 9
Section: 6
Index: 26
Kind: Def

Name: A Krom formula
Definition: A formula of the form \((Q_1P_1^{a_1})\dots(Q_kP_k^{a_k})(\forall \overline x)\bigwedge_{i}(\alpha_{i,0}\lor\alpha_{i,1})\), with \(\alpha_{i,j}\) atomic or negation of an atomic formula.
Page: 151
Chapter: 9
Section: 6
Index: 26
Kind: Def

Name: Horn-SAT
Definition: The restriction of SAT to HORN formulas
Page: 152
Chapter: 9
Section: 6
Index: 27
Kind: Def

Name: Krom-SAT
Definition: The restriction of SAT to Krom formulas
Page: 152
Chapter: 9
Section: 6
Index: 27
Kind: Def

Question: Horn-SAT is
Answer: \(P\)-complete via quantifier-free reduction.
Page: 152
Chapter: 9
Section: 6
Index: 27
Kind: Prop

Question: 2-SAT is
Answer: \(NL\)-complete via quantifier-free reduction.
Page: 152
Chapter: 9
Section: 6
Index: 27
Kind: Prop

Definition: Set of properties definable by iterating the simultaneous FO-definition of a set of \(c\) relations of arity \(k\), \(t(n)\) times, for some \(c\in\mathbb N\).
Page: 160
Chapter: 10
Section: 2
Variables: \(f:\mathbb N\to\mathbb N\), \(k\in\mathbb N\)
Notation: \(ITER[f(n),\text{ arity }k]\)
Index: 9
Kind: Def

Definition: \(\bigcup_{k\in\mathbb N}\text{ITER}[f(n),\text{ arity }k]\).
Page: 160
Chapter: 10
Section: 2
Variables: \(f:\mathbb N\to\mathbb N\)
Notation: \(ITER[f(n)]\)
Index: 9
Kind: Def

Definition: \(\bigcup_{c\in\mathbb N}\text{ITER}[2^{cn^k},\text{ arity }k]\).
Page: 160
Chapter: 10
Section: 2
Variables: \(f:\mathbb N\to\mathbb N\)
Notation: \(\text{ITER}[\text{arity }k]\)
Index: 9
Kind: Def

Definition: \((\phi^{\mathcal A})^r(\emptyset)\) if \((\phi^{\mathcal A})^r(\emptyset)=(\phi^{\mathcal A})^{r+1}(\emptyset)\), and \(\emptyset\) otherwise.
Page: 161
Chapter: 10
Section: 2
Variables: \(\tau\) a vocabulary,
\(\mathcal A\) a \(\tau\)-structure
\(k\in\mathbb N\), \(R\) a relation symbol of arity \(k\),
\(\phi\) a \(FO[\tau,R,x_1,\dots,x_k]\)-formula.
Notation: \((\text{PFP}_{R,x_1,\dots,x_k})^{\mathcal A}\)
Index: 12
Kind: Def

\(f\) is parallel-time constructible implies, the following are equal:
-\(\text{CRAM}[f(n)]\)
-\(\text{ITER}[f(n)]\)
-\(\text{FO}[f(n)]\)
Page: 161
Chapter: 10
Section: 2
Variables: \(f:\mathbb N\to\mathbb N\)
Index: 13
Kind: Theo

Name: FO-VAR\([f(n),v]\)
Definition: The queries in \(\text{FO}[f(n)]\), with \(v\) first-order variables and some constant number of additional boolean variables.
Page: 163
Chapter: 10
Section: 2
Variables: \(f:\mathbb N\to\mathbb N\)
\(v\in\mathbb N\)
Index: 14
Kind: Def

Name: \(VAR[v+1]\)
Definition: \(\bigcup_{c=1}^\infty \text{FO-VAR}\left[2^{cn^v},v+1\right]\).
Page: 163
Chapter: 10
Section: 2
Variables: \(v\in\mathbb N\)
Index: 14
Kind: Def
Extra: +1 ?

Smaller0: \(\text{VAR}[k+1]\)
Greater0: \(\text{ITER}[\text{arity }k]\)
Page: 163
Chapter: 10
Section: 2
Variables: \(k\in\mathbb N\)
Index: 16
Kind: Theo
Smaller to greater: equals
Greatest: \(\text{DSPACE}[n^k]\)

Smaller0: \(f\) is primitive recursive
Greater0: \(f\) is computable in logspace
Page: 149
Chapter: 9
Section: 4
Variables: \(f\) a partial function
Index: 18
Kind: Theo
Smaller to greater: iff
Hide middle: yes