Existential Fixed-point Logic

  • Andrea Blass ,
  • Yuri Gurevich

Springer Lecture Notes in Computer Science 270 |

Download BibTex

The purpose of this paper is to draw attention to existential fixed-point logic (EFPL). Among other things, we show the following.

  • If a structure A satisfies an EFPL formula φ then A has a finite subset F such that every structure that coincides with A on F satisfies φ.
  • Using EFPL instead of first-order logic removes the expressivity hypothesis in Cook’s completeness theorem for Hoare logic.

In the presence of a successor relation, EFPL captures polynomial time.