Some Turing-Complete Extensions of First-Order Logic

TL;DR

This paper introduces a Turing-complete extension of first-order logic with features for model expansion and recursive evaluation, linking logical expressiveness to Turing machine recognition capabilities.

Contribution

The paper presents a novel Turing-complete extension of FO, incorporating model expansion, recursive semantics, and generalized quantifiers, bridging logic and computation.

Findings

Logic is Turing-complete with new features

Semantic game characterizes expressive power

Connection between oracles and generalized quantifiers

Abstract

We introduce a natural Turing-complete extension of first-order logic FO. The extension adds two novel features to FO. The first one of these is the capacity to add new points to models and new tuples to relations. The second one is the possibility of recursive looping when a formula is evaluated using a semantic game. We first define a game-theoretic semantics for the logic and then prove that the expressive power of the logic corresponds in a canonical way to the recognition capacity of Turing machines. Finally, we show how to incorporate generalized quantifiers into the logic and argue for a highly natural connection between oracles and generalized quantifiers.