Descriptive complexity is the study of the relative difficulty of formal languages based on the

syntactic resources needed to create logical formulas defining them.

We've defined first-order logic, where variables represent positions in the input string, the

atomic formulas are "Ia(x)" (position x holds an a), x = y, and x ≤ y, we have boolean

connectives, and we have first order forall and exists quantifiers.

-- BarrinG - 2012-02-27

Theorem

A language is first-order definable iff it is star-free regular.

Proof

Star-free → first-order

We show that the following elements of a star-free expression can be expressed in first-order logic:

∅ (empty set): ∃x: x≠x

a (letter in Σ): ∃x:∀y: (y=x) ∧ Ia(x)

‾ (complement): If ΦX is the first-order formula for a star-free expression X, then ¬ΦX is the formula for expression X

∪ (union): If ΦX and ΦY are the first-order formulas for star-free expressions X and Y, then ΦX∨ΦY is the formula for expression X∪Y

• (concatenation): Let ΦX and ΦY be the first-order formulas for star-free expressions X and Y. Informally, the formula for XY would be the following:

∃z: (w1w2...wz satisfies ΦX) ∧ (wz+1...wn satisfies ΦY), where w1w2...wn is a string over Σ.

The first part (call it Φ≤z) can be constructed from ΦX in the following way: replace each "∃x" with "∃x: (x≤z) ∧" and each "∀x" with "∀x: (x≤z) →". Analogously we construct the second part.

-- SvorotnI - 2012-03-25

Buchi's Theorem says that a language is definable in second-order monadic logic iff it is regular. (See the page with the theorem for the proof.)

-- SvorotnI - 2012-03-12

Topic revision: r5 - 2012-04-22 - SvorotnI    Copyright © 2008-2019 by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding UMass CS EdLab? Send feedback