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^[1] e solitamente senza simboli di funzione.

Soddisfacibilità e decidibilità

La sodisfacibilità logica finita è un problema decidibile.^[2] 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.^[3]

Counting quantifiers

La logica del primo ordine a due variabili e senza simboli di funzione è decidibile anche mediante l'impiego di counting quantifier^[4] 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.^[5]

Note

^ L. Henkin. Logical systems containing only a finite number of symbols, Report, Dipartimento di MAtematica, Università di Montreal, 1967
^ E. Grädel, P.G. Kolaitis and M. Vardi, On the Decision Problem for Two-Variable First-Order Logic, The Bulletin of Symbolic Logic, Vol. 3, n. 1 (marzo 1997), pp. 53-69.
^ A. S. Kahr, Edward F. Moore and Hao Wang. Entscheidungsproblem Reduced to the ∀ ∃ ∀ Case, 1962, notando che le loro formule con i simboli ∀ ∃ ∀ usano solo tre variabili.
^ E. Grädel, M. Otto and E. Rosen. Two-Variable Logic with Counting is Decidable., Proceedings of Twelfth Annual IEEE Symposium on Logic in Computer Science, 1997.
^ Grohe, Martin. "Finite variable logics in descriptive complexity theory." Bulletin of Symbolic Logic 4.4 (1998): 345-398.