# FO (complexidade)

FO é uma classe de complexidade de estruturas que podem ser reconhecidas por fórmulas da lógica de primeira ordem. É a base do campo da teoria da complexidade descritiva e é equivalente à classe de complexidade AC$^0$ FO-regulares. Várias extensões de FO, formadas pela adição de certos operadores, dão origem a outras classes de complexidade conhecidas, permitindo que a complexidade de certos problemas seja provada sem ter que recorrer ao nível algorítmico.

## Definição e exemplos
### A ideia

Quando usamos o formalismo lógico para descrever um problema computacional, a entrada é uma estrutura finita e os elementos dessa estrutura formam o domínio de discurso. Usualmente a entrada é ou uma string (de bits ou sobre um alfabeto) dos elementos que são posições da string, ou um grafo cujos elementos são vértices. O comprimento da entrada será dado pelo tamanho da respectiva estrutura. Qualquer que seja a estrutura, podemos assumir que há relações que podem ser testadas, por exemplo “$E(x,y)$ é verdadeiro se e somente se existe uma aresta de $x$ para $y$” ( no caso da estrutura estar em um grafo), ou “$P(n)$ é verdadeiro se e somente se o $n$-ésimo carácter da string é 1”. Essas relações são os predicados para a lógica de primeira ordem. Também há constantes, que são elementos especiais da respectiva estrutura. Um exemplo é verificar se um dado vértice é alcançável em um certo grafo. Para isso teremos que escolher duas constantes s(início) e t(fim).
Na teoria da complexidade descritiva temos quase sempre que supor que há uma ordem total sobre os elementos e que podemos checar a igualdade entre os elementos. Isso nos permite considerar elementos como números: o elemento $x$ representa o número $n$ se e somente se há $n-1$ elementos $y$ com $x<y$. Graças a isso podemos considerar a primitiva “bit”, onde $bit(x,k)$ é verdadeiro se e somente se o $k$-ésimo bit de $x$ é 1. Podemos substituir a adição e multiplicação por relações ternárias tal que adição$(x,y,z)$ é verdadeiro se e somente se $x+y=z$ e multiplicação$(x,y,z)$ se e somente se $x*y=z$).

### Definição formal

A semântica das fórmulas em FO é direta, $\neg A$ é verdadeira se e somente se $A$ é falso, $A$ é verdadeiro e $B$ é verdadeiro se e somente se $A$ é verdadeiro e $B$ é verdadeiro, e $\forall xP(x)$ é verdadeiro se e somente se $P(v)$ é verdadeiro para todos os valores $v$ que $x$ pode ter no universo fundamental.

## Propriedades
### Justificativa

Dado que elementos computacionais são apenas ponteiros, i.e strings de bits, na complexidade descritiva as premissas que temos tem uma ordem sobre o elemento de uma estrutura faz sentido. Pela mesma razão comumente supomos que ou bit é um predicado ou +, e X, visto que essas funções primitivas podem ser calculadas na maioria das classes de complexidade menores.
FO sem essas primitivas é estudada com mais ênfase na teoria de modelos finitos, e seu equivalente para classes de complexidade menores; essas classes são as decidiveis pela máquina relacional.

### Aviso

Um consulta FO irá então ser a avaliação de se uma formula na lógica de primeira ordem é verdadeira sobre uma estrutura representando a entrada para o problema. Não se deve confundir esse tipo de problema com o da checagem de se uma fórmula booleana é verdadeira, que é a definição de QBF, que é PSPACE-completo. A diferença entre esses dois problemas é que em QBF o tamanho do problema é o tamanho da fórmula e elementos são somente valores booleanos, enquanto no FO o tamanho do problema, isto é, o tamanho da estrutura e fórmula, são fixos.
Isso é similar a Complexidade parametrizada mas o tamanho da fórmula não é um parâmetro fixo.

### Forma normal

Toda fórmula tem uma equivalente na forma normal prenex (onde todos os quantificadores são escritos primeiramente, seguidos de uma fórmula livre de quantificadores).

## Operadores
### FO quaisquer operadores

Na complexidade de circuitos, pode-se mostrar a equivalência entre FO e AC$^0$, a primeira classe na hierarquia AC. De fato, há uma tradução natural de símbolos de FO a nós de um circuito, com $\forall ,\exists$ sendo $\land$ e $\lor$ de tamanho $n$.

### Ponto fixo parcial pertence a PSPACE

FO(PFP) é o conjunto de consultas booleanas definível em FO onde adicionamos um operador de ponto fixo parcial.
Seja um inteiro $k$, $x,y$ de $k$ variáveis, $P$ uma variável de segunda ordem com aridade k e $\phi$ uma função FO(PFP) que usa $k$ e $P$ como variáveis. Podemos iterativamente definir $(P_{i})_{i\in N}$ tal que $P_{0}(x)=falso$ e $P_{i}(x)=\phi (P_{i-1},x)$ (significando $\phi$ com $P_{i-1}$ substituído pela variável de sugunda ordem $P$). Assim, ou há um ponto fixo ou a lista de $(P_{i})$s é cíclica.
PFP($\phi _{P,x})(y)$ é definida como o valor de um ponto fixo de $(P_{i})$ em $y$ se há um ponto fixo, caso contrário falso. Desde que Since $P$s são propriedades de aridade k, há no máximo $2^{n^{k}}$ valores para $P_{i}$s, então com um countador de espaço polinomial podemos checar se há um loop ou não.
É provado que FO(PFP) pertence a PSPACE. Essa definição é equivalente a ($2^{n^{O(1)}}$).

### Menor ponto fixo é P

FO(LFP) é o conjunto de consultas booleanas definíveis in FO(PFP) onde o ponto fixo parcial é limitado para ser monótono. Isso é, se a variável de segunda ordem é $P$, então $P_{i}(x)$ sempre implica $P_{i+1}(x)$.
Podemos garantir a monoticidade restringindo a fórmula $\phi$ para as únicas ocorrências positivas de $P$ ( isso é, ocorrências precedidas por um número par de negações). Nós podemos alternativamente descrever LFP($\phi _{P,x}$) como PFP($\psi _{P,x}$) onde $\psi (P,x)=\phi (P,x)\vee P(x)$.
Devido à monoticidade, somente adicionamos vetores para a tabela verdade de $P$, e uma vez que há somente $n^{k}$ vetores possíveis sempre encontraremos um ponto fixo antes $n^{k}$ iterações. Assim sendo, pode ser visto que FO(LFP) = P. Essa definição é equivalente a FO($n^{O(1)}$).

### Fecho transitivo é NL

FO(TC) é o conjunto de consultas booleanas definíveis in FO com um operador de fecho transitivo (TC).
TC é definido da seguinte maneira: seja $k$ um inteiro positivo e $u,v,x,y$ um vetor de $k$ variáveis. Então TC($\phi _{u,v})(x,y)$ é verdadeiro se existe $n$ vetores de variáveis $(z_{i})$ tal que z$z_{1}=x,z_{n}=y$, e para todos $i<n$, $\phi (z_{i},z_{i+1})$ é verdadeiro. Aqui, $\phi$ é uma fórmula escrita no FO(TC) e $\phi (x,y)$ significa que as variáveis $u$ e $v$ são substituídas por $x$ e $y$.
Essa classe é equivalente a NL.

### Fecho transitivo determinístico é L

FO(DTC) é definido como FO(TC) onde o operador do fecho transitivo é determinístico. Isso significa que quando nós aplicamos DTC($\phi _{u,v}$), nós sabemos que para todo $u$, existe no máximo um $v$ tal que $\phi (u,v)$.
Podemos supor que DTC($\phi _{u,v}$) é açúcar sintático para TC($\psi _{u,v}$)) onde $\psi (u,v)=\phi (u,v)\wedge \forall x,(x=v\vee \neg \psi (u,x))$
Isso mostra que essa classe é equivalente a L.

### Forma normal

Qualquer forma normal com um operador de ponto fixo (correspondendo o fecho transitivo) pode, sem perda de generalidade, ser escrito com apenas um operador dos operadores aplicados a 0 (correspondendo $0,(n-1)$).

## Iteração

Definimos primeira ordem com iteração, 'FO[$t(n)$]'; onde $t(n)$ aqui é uma classe de funções que mapeiam inteiros em inteiros e, para classes diferentes de funções $t(n)$ obteremos diferentes classes de complexidade FO[$t(n)$].
Nessa seção escreveremos $(\forall xP)Q$ como equivalente de $(\forall x(P\Rightarrow Q))$ e $(\exists xP)Q$ como equivalente a $(\exists x(P\vee Q))$. Primeiramente precisamos definir blocos quantificadores(QB do inglês) como uma lista $(Q_{1}x_{1},phi_{1})...(Q_{k}x_{k},phi_{k})$ onde $phi$is são quantificadores livres de fórmulas FO e $Q$is são ou $\forall$ ou $\exists$. Se $Q$ é um bloco quantificador então chamaremos $[Q]^{t(n)}$ o operador iteração que é definido como $Q$ escrito $t(n)$ vezes. Deve-se observar que aqui há $k*t(n)$ quantificadores na lista mas somente $k$ variáveis sendo cada uma dessas variáveis usadas $t(n)$ vezes.
Definimos ainda FO[$t(n)$] como as FO-fórmulas com um operador iteração cujo expoente está na classe $t(n)$, assim obtendo as seguintes igualdades:
* FO[$(\log n)^{i}$] é equivalente ao FO-Uniforme AC$^i$ e de fato FO[t(n)] é FO-Uniforme AC em profundidade $t(n)$.
* FO[$(\log n)^{O(1)}$] é equivalente a NC.
* FO[$n^{O(1)}$] é equivalente a PTIME, o que também é uma moutra maneira de escrever |FO(LFP).
* FO[$2^{n^{O(1)}}$] é equivalente a PSPACE, uma outra forma de escrever FO(PFP).

## Lógica sem relações aritméticas

Seja a relação sucessor, succ, uma relação binária tal que ${\rm {{succ}(x,y)}}$ é verdadeira se e somente se $x+1=y$. Sobre a lógica de primeira ordem, succ é estritamente menos expressiva que < que é menos expressiva que + que é menos expressiva que bit. + e X são menos expressivas que bit.

### Usando sucessor para definir bit

É possível definir as relações adição e então bit com um fecho transitivo determinístico.
${\rm {{plus}(a,b,c)=({\rm {{DTC}_{v,x,y,z}{\rm {{succ}(v,y)\land {\rm {{succ}(z,x))(a,b,c,0)}}}}}}}}$ e
${\rm {{bit}(a,b)=({\rm {{DTC}_{a,b,a',b'}\psi )(a,b,1,0)}}}}$ com
$\psi ={\text{if }}b=0{\text{ então }}({\text{se }}\exists m(a=m+m+1){\text{ então }}(a'=1\land b'=0){\text{ se-não }}\bot ){\text{ se-não }}({\rm {{succ}(b',b)\land (a+a=a'\lor a+a+1=a')}}$
Isso significa que quando consultamos para o bit 0 checamos a paridade e vamos para (1,0) se $a$ é impar (que é um estado de aceitação), caso contrário rejeitamos. Se checarmos um bit $b>0$, dividimos a por 2 e checamos bit $b-1$.
Assim não faz sentido falar de apenas com sucessores, sem outros predicados.

### Lógicas sem sucessores

Ná lógica sem succ, +, x, < ou bit, é formada a igualdade de FO(LFP) para p-relacional e FO(PFP) para PSPACE-relacional, com as classes P e PSPACE sobre máquinas relacionais. O teorema de Abiteboul-Vianu afirma que FO(LFP) = FO(PFP) se e somente se FO(<, LFP) = FO(PFP) e se somente se P = PSPACE. Esse resultado tem sido estendido a outros pontos fixos. Isso nos mostra que o problema de ordem na lógica de primeira ordem é muito mais um problema técnico que um problema fundamental.