## AI generates interpretation videos

AI extracts and analyses the key points of the paper to generate videos automatically

Go Generating

## AI Traceability

AI parses the academic lineage of this thesis

Generate MRT

## AI Insight

AI extracts a summary of this paper

Weibo:
QUESTION Can a first-order query language exploit an auxiliary linear order/successor relation on data in a manner that does not depend on the particular linear order/successor relation?

# Successor-Invariance in the Finite

LICS, pp.148-148, (2003)

Cited by: 16|Views114
EI
Full Text
Bibtex
Weibo

Abstract

A first-order sentence \theta of vocabulary \sigma \cup {S} issuccessor-invariant in the finite if for every finite \sigma-structureM and successor relations S1 and S2 on M,(M,S1) \models \theta \iff (M, S2) \models \theta.In this paper I give an example of a non-first-order definableclass of finite structures which is, however, defined b...More

Code:

Data:

Introduction
• : <-invariance in the finite and ε-invariance in the finite. Interpolation theorem ⇒ If θ ∈ FO[S] is S-invariant for all structures θ ≡ θ for some θ ∈ FO.
• A first-order sentence θ of vocabulary σ ∪ {S} is successor-invariant in the finite if for every finite σ-structure M and successor relations S1, S2 on M, (M, S1) |= θ ⇐⇒ (M, S2) |= θ.
• FO[S] = first-order logic over finite structures with a successor relation
• FO[S]inv = successor-invariant sentences of FO[S]
Highlights
• : <-invariance in the finite and ε-invariance in the finite
• QUESTION Can a first-order query language exploit an auxiliary linear order/successor relation on data in a manner that does not depend on the particular linear order/successor relation?
Results
• The author will call FO[S]inv successor-invariant first-order logic.
• Is <-invariant over Q , where it defines PARITY(A).
• The authors can define PARITY(A) over Q without < if the authors have access to an arbitrary successor relation on A.
• The authors obtained a successor relation on A by restricting the linear order <.
• Q := class of all finite structures of the form
• The authors want to define a successor relation on A alone.
• CLAIM In the structure M, S, E0, 2E0, (2E0)(2E0) , every successor function : A −→ A is FO definable with a single parameter p ∈ (2E0)(2E0).
• This “definition” of (x, y ; p) modulo the helpmeets E0 ⊂ E, 2E0 and (2E0)(2E0) is adapted for the general case of an arbitrary successor relation S.
• M = A, Ac, E, #, X, EX, 2X, (2X)(2X) where (i) E, X, EX, 2X, (2X)(2X) ⊆ Ac (ii) # : Ac → 2E an injection (iii) X ≥ A
• CLAIM The desired formula (x, y ; p) is definable in the first-order language of Q plus S.
Conclusion
• It’s easy to see that PARITY(A) is not FO definable even if the authors allow quantification over 2A.
• The authors have come up with a class Q of finite structures of the form M = A ∪ Ac, .
• 2. there is a formula (x, y ; p) of FO[S] where, for every M ∈ Q and successor relation S on A ∪ Ac, there exist parameters pfrom M such that (x, y ; p) defines a successor relation on A.
• FO[A; dA]—first-order logic over structures with a distinguished subset A and a derangement dA of A.
Author