Algorithmic uses of the Feferman–Vaught Theorem

Annals of Pure and Applied Logic 126 (1-3):159-213 (2004)
  Copy   BIBTEX

Abstract

The classical Feferman–Vaught Theorem for First Order Logic explains how to compute the truth value of a first order sentence in a generalized product of first order structures by reducing this computation to the computation of truth values of other first order sentences in the factors and evaluation of a monadic second order sentence in the index structure. This technique was later extended by Läuchli, Shelah and Gurevich to monadic second order logic. The technique has wide applications in decidability and definability theory. Here we give a unified presentation, including some new results, of how to use the Feferman–Vaught Theorem, and some new variations thereof, algorithmically in the case of Monadic Second Order Logic MSOL . We then extend the technique to graph polynomials where the range of the summation of the monomials is definable in MSOL . Here the Feferman–Vaught Theorem for these polynomials generalizes well known splitting theorems for graph polynomials. Again, these can be used algorithmically. Finally, we discuss extensions of MSOL for which the Feferman–Vaught Theorem holds as well

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 90,616

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

A Non‐Boolean Version of Feferman‐Vaught's Theorem.R. Lavendhomme & Th Lucas - 1985 - Mathematical Logic Quarterly 31 (19‐20):299-308.
The Vaught Conjecture: Do Uncountable Models Count?John T. Baldwin - 2007 - Notre Dame Journal of Formal Logic 48 (1):79-92.
Vaught's theorem on axiomatizability by a scheme.Albert Visser - 2012 - Bulletin of Symbolic Logic 18 (3):382-402.
Algorithmic logic. Multiple-valued extensions.Helena Rasiowa - 1979 - Studia Logica 38 (4):317 - 335.
The classification of small weakly minimal sets. II.Steven Buechler - 1988 - Journal of Symbolic Logic 53 (2):625-635.

Analytics

Added to PP
2014-01-16

Downloads
24 (#563,255)

6 months
1 (#1,042,085)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Feferman–Vaught Decompositions for Prefix Classes of First Order Logic.Abhisekh Sankaran - 2023 - Journal of Logic, Language and Information 32 (1):147-174.
Tarski’s Influence on Computer Science.Solomon Feferman - 2018 - In Urszula Wybraniec-Skardowska & Ángel Garrido (eds.), The Lvov-Warsaw School. Past and Present. Cham, Switzerland: Springer- Birkhauser,. pp. 391-404.
A logician's view of graph polynomials.J. A. Makowsky, E. V. Ravve & T. Kotek - 2019 - Annals of Pure and Applied Logic 170 (9):1030-1069.

View all 7 citations / Add more citations

References found in this work

Model theory.Wilfrid Hodges - 2008 - Stanford Encyclopedia of Philosophy.
Weak Second‐Order Arithmetic and Finite Automata.J. Richard Büchi - 1960 - Mathematical Logic Quarterly 6 (1-6):66-92.
Reduced Direct Products.T. Frayne, A. C. Morel & D. S. Scott - 1966 - Journal of Symbolic Logic 31 (3):506-507.
Infinitary analogs of theorems from first order model theory.Jerome Malitz - 1971 - Journal of Symbolic Logic 36 (2):216-228.

View all 20 references / Add more references