A proof-theoretical approach to some extensions of first order quantification

TL;DR

The paper develops a proof-theoretic approach to non-standard quantifiers by recasting them as second-order constructions over 'individual concepts'. It surveys generalised quantifiers and shows an equivalence between the second-order view and standard first-order quantification when individual concepts are standard and nonempty, then translates the simplest branching quantifier into a second-order formulation and proposes dedicated natural deduction rules for it. This work bridges model-theoretic ideas in linguistics with formal proof theory, enabling deductive reasoning about quantification patterns such as 'A member of each team and a member of each board of directors know each other'.

Abstract

Generalised quantifiers, which include Henkin's branching quantifiers, have been introduced by Mostowski and Lindström and developed as a substantial topic application of logic, especially model theory, to linguistics with work by Barwise, Cooper, Keenan. In this paper, we mainly study the proof theory of some non-standard quantifiers as second order formulae . Our first example is the usual pair of first order quantifiers (for all / there exists) when individuals are viewed as individual concepts handled by second order deductive rules. Our second example is the study of a second order translation of the simplest branching quantifier: ``A member of each team and a member of each board of directors know each other", for which we propose a second order treatment.