A Lindstr\"om theorem for intuitionistic first-order logic

TL;DR

This paper extends Lindström's theorem to first-order intuitionistic logic, characterizing it as the most expressive logic satisfying compactness, the Tarski union property, and preservation under asimulations.

Contribution

It generalizes previous results to first-order intuitionistic logic, including constant domains, establishing its maximality under specific model-theoretic properties.

Findings

First-order intuitionistic logic is maximal among logics with compactness and the Tarski union property.

The result applies to intuitionistic logic with and without equality.

A similar characterization is provided for the logic of constant domains.

Abstract

We extend the main result of (G. Badia and G. Olkhovikov. A Lindstr\"om theorem for intuitionistic propositional logic. Notre Dame Journal of Formal Logic, 61 (1): 11--30 (2020)) to the first-order intuitionistic logic (with and without equality), showing that it is the maximal (with respect to expressive power) abstract logic satisfying a certain form of compactness, the Tarski union property and preservation under asimulations. A similar result is also shown for the intuitionistic logic of constant domains.