Tvåvariabel logik

Inom matematisk logik och datavetenskap är tvåvariabellogik fragmentet av första ordningens logik där formler kan skrivas med endast två olika variabler . Detta fragment studeras vanligtvis utan funktionssymboler .

Beslutbarhet

Några viktiga problem om tvåvariabel logik, såsom tillfredsställelse och ändlig tillfredsställelse , är avgörbara . Detta resultat generaliserar resultat om avgörbarheten av fragment av tvåvariabellogik, såsom vissa beskrivningslogiker ; vissa fragment av tvåvariabellogik åtnjuter emellertid en mycket lägre beräkningskomplexitet för sina tillfredsställbarhetsproblem.

Däremot, för trevariabelfragmentet av första ordningens logik utan funktionssymboler, är tillfredsställbarheten obestämbar.

Räkna kvantifierare

Tvåvariabelfragmentet av första ordningens logik utan funktionssymboler är känt för att kunna avgöras även med tillägg av räknekvantifierare , och därmed unikhetskvantifiering . Detta är ett mer kraftfullt resultat, eftersom räknekvantifierare för höga numeriska värden inte kan uttryckas i den logiken.

Räknekvantifierare förbättrar faktiskt uttrycksförmågan hos ändlig variabel logik eftersom de tillåter att säga att det finns en nod med $n$ grannar, nämligen $\Phi =\exists x\exists ^{\geq n}yE(x,y)$ . Utan att räkna kvantifierare behövs ${\displaystyle n+1} variabler för samma formel.$

Anslutning till Weisfeiler-Leman-algoritmen

Det finns ett starkt samband mellan tvåvariabellogik och Weisfeiler-Leman (eller färgförfining) algoritmen. Givet två grafer, så har två valfria noder samma stabila färg i färgförfining om och endast om de har samma $C^{2}$ -typ, det vill säga de uppfyller samma formler i tvåvariabellogik med att räkna.

^ L. Henkin. Logiska system som endast innehåller ett ändligt antal symboler , Rapport, Institutionen för matematik, University of Montreal, 1967
^ E. Grädel, PG Kolaitis och M. Vardi, på beslutsproblemet för två-variabel första ordningens logik, Bulletinen av symbolisk logik, vol. 3, nr 1 (mars, 1997), sid. 53-69.
^ AS Kahr, Edward F. Moore och Hao Wang. Entscheidungsproblem Reducerat till ∀ ∃ ∀ Case , 1962, och noterar att deras ∀ ∃ ∀-formler endast använder tre variabler.
^ E. Grädel, M. Otto och E. Rosen. Tvåvariabel logik med räkning kan avgöras. , Proceedings of Twelfth Annual IEEE Symposium on Logic in Computer Science, 1997.
^ Grohe, Martin. "Finita variabel logik i beskrivande komplexitetsteori." Bulletin of Symbolic Logic 4.4 (1998): 345-398.

[1] L. Henkin. Logiska system som endast innehåller ett ändligt antal symboler , Rapport, Institutionen för matematik, University of Montreal, 1967

[2] E. Grädel, PG Kolaitis och M. Vardi, på beslutsproblemet för två-variabel första ordningens logik, Bulletinen av symbolisk logik, vol. 3, nr 1 (mars, 1997), sid. 53-69.

[3] AS Kahr, Edward F. Moore och Hao Wang. Entscheidungsproblem Reducerat till ∀ ∃ ∀ Case , 1962, och noterar att deras ∀ ∃ ∀-formler endast använder tre variabler.

[4] E. Grädel, M. Otto och E. Rosen. Tvåvariabel logik med räkning kan avgöras. , Proceedings of Twelfth Annual IEEE Symposium on Logic in Computer Science, 1997.

[5] Grohe, Martin. "Finita variabel logik i beskrivande komplexitetsteori." Bulletin of Symbolic Logic 4.4 (1998): 345-398.