fixed-point logic

For a relational signature X, FO[PFP](X) is the set of formulas formed from X using first-order connectives and predicates, second-order variables as well as a partial fixed point operator $\backslash operatorname\{PFP\}$ used to form formulas of the form $[\backslash operatorname\{PFP\}\_\{\backslash vec\{x\},P\}\; \backslash varphi]\backslash vec\{t\}$, where $P$ is a second-order variable, $\backslash vec\{x\}$ a tuple of first-order variables, $\backslash vec\{t\}$ a tuple of terms and the lengths of $\backslash vec\{x\}$ and $\backslash vec\{t\}$ coincide with the arity of $P$.

Let {{mvar|k}} be an integer, $x,\; y$ be vectors of {{mvar|k}} variables, {{mvar|P}} be a second-order variable of arity {{mvar|k}}, and let {{mvar|φ}} be an FO(PFP,X) function using {{mvar|x}} and {{mvar|P}} as variables. We can iteratively define $(P\_i)\_\{i\backslash in\; N\}$ such that $P\_0(x)=false$ and $P\_i(x)=\backslash varphi(P\_\{i-1\},x)$ (meaning {{mvar|φ}} with $P\_\{i-1\}$ substituted for the second-order variable {{mvar|P}}). Then, either there is a fixed point, or the list of $(P\_i)$s is cyclic.Ebbinghaus and Flum, p. 121

$[\backslash operatorname\{PFP\}\_\{P,x\}\; \backslash varphi\; (y)]$ is defined as the value of the fixed point of $(P\_i)$ on {{mvar|y}} if there is a fixed point, else as false.Ebbinghaus and Flum, p. 121 Since {{mvar|P}}s are properties of arity {{mvar|k}}, there are at most $2^\{n^k\}$ values for the $P\_i$s, so with a polynomial-space counter we can check if there is a loop or not.Immerman 1999, p. 161

It has been proven that on ordered finite structures, a property is expressible in FO(PFP,X) if and only if it lies in PSPACE.{{Cite book|last1=Abiteboul|first1=S.|last2=Vianu|first2=V.|title=[1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science |chapter=Fixpoint extensions of first-order logic and datalog-like languages |chapter-url=http://dx.doi.org/10.1109/lics.1989.39160|year=1989|pages=71–79|publisher=IEEE Comput. Soc. Press|doi=10.1109/lics.1989.39160|isbn=0-8186-1954-6|s2cid=206437693}}

Since the iterated predicates involved in calculating the partial fixed point are not in general monotone, the fixed-point may not always exist.

FO(LFP,X), least fixed-point logic, is the set of formulas in FO(PFP,X) where the partial fixed point is taken only over such formulas {{mvar|φ}} that only contain positive occurrences of {{mvar|P}} (that is, occurrences preceded by an even number of negations). This guarantees monotonicity of the fixed-point construction (That is, if the second order variable is {{mvar|P}}, then $P\_i(x)$ always implies $P\_\{i+1\}(x)$).

Due to monotonicity, we only add vectors to the truth table of {{mvar|P}}, and since there are only $n^k$ possible vectors we will always find a fixed point before $n^k$ iterations. The Immerman-Vardi theorem, shown independently by Immerman{{Cite journal|last=Immerman|first=Neil|year=1986|title=Relational queries computable in polynomial time|journal=Information and Control|language=en|volume=68|issue=1–3|pages=86–104|doi=10.1016/s0019-9958(86)80029-8|doi-access=free}} and Vardi,{{Cite book|last=Vardi|first=Moshe Y.|chapter=The complexity of relational query languages (Extended Abstract) |title=Proceedings of the fourteenth annual ACM symposium on Theory of computing - STOC '82|date=1982|publisher=ACM|isbn=978-0897910705|location=New York, NY, USA|pages=137–146|citeseerx=10.1.1.331.6045|doi=10.1145/800070.802186|s2cid=7869248}} shows that FO(LFP,X) characterises P on all ordered structures.

The expressivity of least-fixed point logic coincides exactly with the expressivity of the database querying language Datalog, showing that, on ordered structures, Datalog can express exactly those queries executable in polynomial time.Ebbinghaus and Flum, p. 242

Another way to ensure the monotonicity of the fixed-point construction is by only adding new tuples to $P$ at every stage of iteration, without removing tuples for which $P$ no longer holds. Formally, we define $\backslash operatorname\{IFP\}(\backslash phi\_\{P,x\})$ as $\backslash operatorname\{PFP\}(\backslash psi\_\{P,x\})$ where $\backslash psi(P,x)=\backslash phi(P,x)\backslash vee\; P(x)$.

This inflationary fixed-point agrees with the least-fixed point where the latter is defined. Although at first glance it seems as if inflationary fixed-point logic should be more expressive than least fixed-point logic since it supports a wider range of fixed-point arguments, in fact, every FO[IFP](X)-formula is equivalent to an FO[LFP](X)-formula. Yuri Gurevich and Saharon Shelah, Fixed-pointed extension of first order logic, Annals of Pure and Applied Logic 32 (1986) 265--280.

While all the fixed-point operators introduced so far iterated only on the definition of a single predicate, many computer programs are more naturally thought of as iterating over several predicates simultaneously. By either increasing the arity of the fixed-point operators or by nesting them, every simultaneous least, inflationary or partial fixed-point can in fact be expressed using the corresponding single-iteration constructions discussed above.Ebbinghaus and Flum, pp. 179, 193

Rather than allow induction over arbitrary predicates, transitive closure logic allows only transitive closures to be expressed directly.

FO[TC](X) is the set of formulas formed from X using first-order connectives and predicates, second-order variables as well as a transitive closure operator $\backslash operatorname\{TC\}$ used to form formulas of the form $[\backslash operatorname\{TC\}\_\{\backslash vec\{x\},\backslash vec\{y\}\}\; \backslash varphi]\backslash vec\{s\}\backslash vec\{t\}$, where $\backslash vec\{x\}$ and $\backslash vec\{y\}$ are tuples of pairwise distinct first-order variables, $\backslash vec\{t\}$ and $\backslash vec\{s\}$ tuples of terms and the lengths of $\backslash vec\{x\}$, $\backslash vec\{y\}$, $\backslash vec\{s\}$ and $\backslash vec\{t\}$ coincide.

TC is defined as follows: Let {{mvar|k}} be a positive integer and $u,v,x,y$ be vectors of {{mvar|k}} variables. Then $\backslash mathsf\{TC\}(\backslash phi\_\{u,v\})(x,y)$ is true if there exist {{mvar|n}} vectors of variables $(z\_i)$ such that $z\_1=x,\; z\_n=y$, and for all

Over ordered structures, FO[TC] characterises the complexity class NL.{{Cite book|last=Immerman|first=Neil|title=Proceedings of the fifteenth annual ACM symposium on Theory of computing - STOC '83 |chapter=Languages which capture complexity classes |date=1983|chapter-url=http://dx.doi.org/10.1145/800061.808765|pages=347–354|location=New York, New York, USA|publisher=ACM Press|doi=10.1145/800061.808765|isbn=0897910990|s2cid=7503265}} This characterisation is a crucial part of Immerman's proof that NL is closed under complement (NL = co-NL).{{Cite journal|last=Immerman|first=Neil|date=1988|title=Nondeterministic Space is Closed under Complementation|url=http://dx.doi.org/10.1137/0217058|journal=SIAM Journal on Computing|volume=17|issue=5|pages=935–938|doi=10.1137/0217058|issn=0097-5397}}

FO[DTC](X) is defined as FO(TC,X) where the transitive closure operator is deterministic. This means that when we apply $\backslash operatorname\{DTC\}(\backslash phi\_\{u,v\})$, we know that for all {{mvar|u}}, there exists at most one {{mvar|v}} such that $\backslash phi(u,v)$.

We can suppose that $\backslash operatorname\{DTC\}(\backslash phi\_\{u,v\})$ is syntactic sugar for $\backslash operatorname\{TC\}(\backslash psi\_\{u,v\})$ where $\backslash psi(u,v)=\backslash phi(u,v)\backslash wedge\; \backslash forall\; x\; (x=v\; \backslash vee\; \backslash neg\; \backslash phi(u,x))$.

Over ordered structures, FO[DTC] characterises the complexity class L.

The fixed-point operations that we defined so far iterate the inductive definitions of the predicates mentioned in the formula indefinitely, until a fixed point is reached. In implementations, it may be necessary to bound the number of iterations to limit the computation time. The resulting operators are also of interest from a theoretical point of view since they can also be used to characterise complexity classes.

We will define first-order with iteration, $\backslash mathsf\{FO\}[t(n)]$; here $t(n)$ is a (class of) functions from integers to integers, and for different classes of functions $t(n)$ we will obtain different complexity classes $\backslash mathsf\{FO\}[t(n)]$.

In this section we will write $(\backslash forall\; x\; P)\; Q$ to mean $(\backslash forall\; x\; (P\backslash Rightarrow\; Q))$ and $(\backslash exists\; x\; P)\; Q$ to mean $(\backslash exists\; x\; (P\; \backslash wedge\; Q))$. We first need to define quantifier blocks (QB), a quantifier block is a list $(Q\_1\; x\_1,\; \backslash phi\_1)...(Q\_k\; x\_k,\; \backslash phi\_k)$ where the $\backslash phi\_i$s are quantifier-free FO-formulae and $Q\_i$s are either $\backslash forall$ or $\backslash exists$. If {{mvar|Q}} is a quantifiers block then we will call $[Q]^\{t(n)\}$ the iteration operator, which is defined as {{mvar|Q}} written $t(n)$ time. One should pay attention that here there are $k*t(n)$ quantifiers in the list, but only {{mvar|k}} variables and each of those variable are used $t(n)$ times.Immerman 1999, p. 63

We can now define $\backslash mathsf\{FO\}[t(n)]$ to be the FO-formulae with an iteration operator whose exponent is in the class $t(n)$, and we obtain the following equalities:

• $\backslash mathsf\{FO\}[(\backslash log\; n)^i]$ is equal to FO-uniform ACⁱ, and in fact $\backslash mathsf\{FO\}[t(n)]$ is FO-uniform AC of depth $t(n)$.Immerman 1999, p. 82
• $\backslash mathsf\{FO\}[(\backslash log\; n)^\{O(1)\}]$ is equal to NC.Immerman 1999, p. 84
• $\backslash mathsf\{FO\}[n^\{O(1)\}]$ is equal to PTIME. It is also another way to write FO(IFP).Immerman 1999, p. 58
• $\backslash mathsf\{FO\}[2^\{n^\{O(1)\}\}]$ is equal to PSPACE. It is also another way to write FO(PFP). Immerman 1999, p. 161

{{reflist}}

• {{Cite book|last1=Ebbinghaus|first1=Heinz-Dieter|last2=Flum|first2=Jörg|date=1999|title=Finite Model Theory|edition=2|series=Perspectives in Mathematical Logic|publisher=Springer|doi=10.1007/978-3-662-03182-7|isbn=978-3-662-03184-1}}
• {{Cite book|last=Neil|first=Immerman|url=http://worldcat.org/oclc/901297152|title=Descriptive complexity|date=1999|publisher=Springer|isbn=0-387-98600-6|oclc=901297152}}

{{Mathematical logic}}

Category:Descriptive complexity

Category:Database theory

Category:Predicate logic