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 "I_{a}(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) ∧ I_{a}(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: (w_{1}w_{2}...w_{z} *satisfies* Φ_{X}) ∧ (w_{z+1}...w_{n} *satisfies* Φ_{Y}), where w_{1}w_{2}...w_{n} 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

Copyright © 2008-2017 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

Ideas, requests, problems regarding UMass CS EdLab? Send feedback