FPL may be equivalent to FO but not equivalent to PFP

2004/04/09 by Saharon Shelah, Shelah, Saharon
Computer Science · Mathematics · #FOS: Mathematics #Formal Methods in Verification #Logic (math.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #math.LO

paper · pdf · doi:10.48550/arxiv.math/0404205

arxiv created 2004/04/09 · openalex publication_date 2004/04/09 · arxiv updated 2009/12/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

Abstract

Given a class of finite models we would like to expand each model (allowing new elements but the old universe is a separate sort), making the expressive power of LFP (least fix point logic) and PFP (inductive logic) similar while not changing the expressive power of FO (first order logic). This continues in math.LO/9411235.

Related

• The theory of concatenation over finite models
• A logic with temporally accessible iteration
• FMP for QD logics. A wrong proof
• One Quantifier Alternation in First-Order Logic with Modular Predicates
• Undecidability of Finite Model Reasoning in DLFD