title: Logica a due variabili
text: # Logica a due variabili
  
  Nella logica matematica e nell'informatica, la logica a due variabili è la parte della logica del primo ordine le cui formule possono essere scritte mediante due variabili e solitamente senza simboli di funzione.
  
  ## Soddisfacibilità e decidibilità
  
  La sodisfacibilità logica finita è un problema decidibile. Questo risultato generalizza ciò che era già noto per alcune logiche a due variabili come la logica descrittiva. I problemi di soddisfacibilità di alcune logiche a due variabili godono di una complessità computazionale molto inferiore rispetto alle altre.
  
  Al contrario, per quanto concerne la logica del primo ordine a tre variabili e senza simboli di funzione, la soddisfacibilità è indecidibile.
  
  ## Counting quantifiers
  
  La logica del primo ordine a due variabili e senza simboli di funzione è decidibile anche mediante l'impiego di counting quantifier che ne quantificano l'unicità. Per valori numerici elevati, i counting quantifier non sono esprimibili nella logica a due variabili.
  
  I counting quantifier migliorano effettivamente l'espressività delle logiche a variabili finite in quanto consentono di dire che esiste un nodo con $n$ altri nodi prossimali, vale a dire che $\Phi =\exists x\exists ^{\geq n}yE(x,y)$ (senza dover enunciare nella stessa formula i counting quantifier per le altre $n+1$ variabili).
  
  ## Connessione con l'algoritmo di Weisfeiler-Leman
  
  La logica a due variabili presenta una stretta connessione con l'algoritmo di Weisfeiler-Leman. Dati due grafi, due nodi qualsiasi presentano lo stesso colore stabile se e solo se hanno lo stesso tipo $C^{2}$, cioè se soddisfano le medesime formule in una logica a due variabili che fa uso di counting quantifier.
  
  