Revision as of 22:51, 27 May 2015 edit Fmarkqiao (talk \| contribs) 57 edits →Logic without arithmetical relations ← Previous edit		Revision as of 00:09, 13 January 2016 edit undo 24.212.193.99 (talk) →Iterating Next edit →
Line 74: We will define first-order with iteration, ''''FO[<math>t(n)</math>]''''; here <math>t(n)</math> is a (class of) functions from integers to integers, and for different classes of functions <math>t(n)</math> we will obtain different complexity classes FO[<math>t(n)</math>]. In this section we will write <math>(\forall x P) Q</math> to mean <math>(\forall x (P\Rightarrow Q))</math> and <math>(\exists x P) Q</math> to mean <math>(\exists x (P \~~vee~~wedge Q))</math>. We first need to define quantifier blocks (QB), a quantifier block is a list <math>(Q_1 x_1, \phi_1)...(Q_k x_k, \phi_k)</math> where the <math>\phi_i</math>s are quantifier-free [[#Complexity_Zoo:F#FO\|FO]]-formulae and <math>Q_i</math>s are either <math>\forall</math> or <math>\exists</math>. If <math>Q</math> is a quantifiers block then we will call <math>[Q]^{t(n)}</math> the iteration operator, which is defined as <math>Q</math> written <math>t(n)</math> time. One should pay attention that here there are <math>k*t(n)</math> quantifiers in the list, but only <math>k</math> variables and each of those variable are used <math>t(n)</math> times.

FO (complexity): Difference between revisions