Implicitly definable generalized quantifiers

TL;DR

This paper provides a new elementary proof showing that quantifiers implicitly definable in second-order logic with Henkin semantics are also explicitly definable in first-order logic, simplifying understanding of their definability.

Contribution

It introduces a novel elementary proof of a key theorem relating implicit and explicit definability of quantifiers under Henkin semantics.

Findings

Implicitly definable quantifiers in second-order logic are explicitly definable in first-order logic.

The proof simplifies previous complex arguments.

Clarifies the relationship between second-order and first-order definability.

Abstract

We give a new elementary proof of the main theorem of [Fef12]: Quantifiers implicitly definable in pure second-order logic equipped with Henkin semantics implies are (explicitly) definable in first-order logic.