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