Logica a due variabili
# 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.

