Two-variable logic: Difference between revisions

Revision as of 13:50, 9 May 2022

Latest revision as of 13:07, 13 September 2022

(One intermediate revision by one other user not shown)

Line 1:

{{ref improve|date=August 2014}}

In [[mathematical logic]] and [[computer science]], '''two-variable logic''' is the [[fragment (logics)|fragment]] of [[first-order logic]] where [[formula (logics)|formulae]] can be written using only two different [[variable (logics)|variable]]s.<ref>L. Henkin. ''Logical systems containing only a finite number of symbols'', Report, Department of Mathematics, University of Montreal, 1967</ref> This fragment is usually studied without [[function symbol]]s.

Line 16 ⟶ 15:

== Connection to the Weisfeiler-Leman algorithm ==

There is a strong connection between two-variable logic and the Weisfeiler-Leman (or [[Colour refinement algorithm|color refinement]]) algorithm. Given two graphs, then any two nodes have the same stable color in color refinement if and only if they have the same <math>C^2</math> type, that is, they satisfy the same formulas in two-variable logic with counting.<ref>Grohe, Martin. "Finite variable logics in descriptive complexity theory." Bulletin of Symbolic Logic 4.4 (1998): 345-398.</ref>

== References ==