A first order logic extended with binding terms like the familiar set descriptors $\{x:\varphi\}$

Question

First order logic comes equipped with two kinds of terms:

1. Variable: those terms of the form $x$ for some variable $x$, of which there are infinite.
2. Function application: those terms of the form $f(t_1,\dots,t_n)$ for some $n$-place function symbol $f$, of which there are infinite, and some $n$ terms $t_1, \dots, t_n$.

In practice, one more kind of term is commonly used informally in the context of set theory: set descriptors of the form $\{x:\varphi\}$, where $x$ is a variable, and $\varphi$ is a first order well-formed formula. This term cannot be rewritten as a function application, since $\varphi$ is not a term. This term creates a scope in which the variable $x$ is bound, similar to the way the quantified formulas of the form $\forall x\varphi$ and $\exists x\varphi$ work.

One way to introduce set descriptor terms into the logic, which then will no longer be a first order logic, so lets call it extended first order logic, is by introducing an infinite set of binding term constructors that is disjoint from the the first order logic vocabulary (consisting of logical symbols, variables, function symbols, and relation symbols), and a new way of forming terms: $Cx\varphi$, for every binding term constructor $C$, every variable $x$, and every extended first order well-formed formula $\varphi$ (the definition of function application and of a well-formed formula should be modified to accomodate this new kind of term). Let's call such terms binding terms.

We can now set aside one of the new-fangled binding term constructors, say $\sigma$, and interpret every binding term of the form $\sigma x\varphi$ as $\{x:\varphi\}$.

Set descriptors are probably the most familiar example of binding terms, but two others that I know of have been proposed in the past by mainstream mathematicians, likewise in the context of set theory: Hilbert's epsilon operator and Bourbaki's $\tau$ operator, which, though similar, are not the same operator, as they satisfy slightly different axioms.

Note that extending first order logic with binding terms necessitates a corresponding extension of the inference system, say Gentzen's Natural Deduction.

Has the combination of extended first order logic with a corresponding inference system been studied? Where can I read more about it?

Answer 1

I would recommend looking at higher-order logics (HOL), for instance Lambek and Scott's Introduction to Higher-Order Categorical Logic. Such a logic will set up binding of bound variables and treat variable contexts properly (single-sorted first-order logic tends to have a somewhat simplistic view of those).

Note that your suggestion to always bind just a single variable does not cover operators that require simulatneous binding of several variables. They are uncommon, but do appear occasionally.

To get what you're asking for, we can cut down on the order. In HOL there is a single sort of types, including a type of propositions $\Omega$, which are closed under formation of function spaces, so that higher-order predicates are formed as $\Omega$, $A \to \Omega$, $(A \to \Omega) \to \Omega$. To prevent these, we can stratify the types into several sorts:

• the sort of primitive types $A$, $B$, $C$, ... (in first-order logic you often have just a single one, which is not mentioned at all)
• the sort of propositions $\Omega$
• the sort of first-order functions $(A_1, \ldots, A_n) \to B$, where $A_i$ and $B$ are primitive types
• the sort of (first-order) propositional functions $(A_1, \ldots, A_n) \to \Omega$, where $A_i$ are primitive types.

Variables always range over primitive types. A context $\Gamma$ is a list of variables with their (primitive) types, $\Gamma \equiv x_1 : A_1, \ldots, x_n : A_n$. We never speak of an expression without specifying its context, so that we can keep track of which variables are allowed to appear.

If $S$ is a sort, we write $\Gamma \vdash e : S$ when $e$ is an expression of sort $S$ in context $\Gamma$. For example, $$x : \mathbb{R}, y : \mathbb{R} \vdash (\exists z : \mathbb{R} . x + z = y) : \Omega$$ is the assertion that $\exists z : \mathbb{R} . x + z = y$ is a proposition (in the given context). It is not the assertion that $\exists z : \mathbb{R} . x + z = y$ holds! For that we postulate a new judgement of the form $$\Gamma \mid \theta_1, \ldots, \theta_n \vdash \psi \ \mathsf{true} \tag{1}$$ which states, intuitively, that propositions $\theta_1, \ldots, \theta_n$ jointly entail the proposition $\psi$. If we also have equations (at all types), (1) can be replaced with $$\Gamma \mid (\theta_1 \land \cdots \land \theta_n) \land \psi =_\Omega \theta_1 \land \cdots \land \theta_n.$$ This is the approach taken by Lambek and Scott. Its main advantage is that the formal system is more like algebra, since it is just a bunch of (fancy) operations and equations.

Another example (where I am using the notation $\langle x_1 : A_1, \ldots, x_n : A_n \rangle . e$ to express the fact that the variables $x_1, \ldots, x_n$ are bound in $e$): $$x : \mathbb{R} \vdash (\langle y : \mathbb{R}, z : \mathbb{R} \rangle . y^2 + x \cdot z) : (\mathbb{R}, \mathbb{R}) \to \mathbb{R}.$$ This says that there is a function taking $(y, z)$ to $y^2 + x \cdot z$.

We can now introduce first-order binders as operations that map first-order (propositional) functions to primitive sorts and propositions, for instance:

1. $\forall$ is an operation which takes a propositional function $(A) \to \Omega$ to a proposition. The formation rule would read as follows: $$\frac{\Gamma \vdash p : (A) \to \Omega}{\Gamma \vdash \forall p : \Omega}$$ En example of such an expression would be $\forall (\langle x : \mathbb{R} \rangle . x^4 - 5 x^2 + 7 > 0)$.

2. Assuming there is a primitive type $\mathsf{Set}$ of sets and a relation symbol $\in$ of sort $(\mathsf{Set}, \mathsf{Set}) \to \Omega$, subset formation $\sigma$ is an operation which takes $s : \mathsf{Set}$ and $p : (\mathsf{Set}) \to \Omega$ and yields $\sigma(s, p) : \mathsf{Set}$. We also need some rules regarding these, e.g., $$ \Gamma \mid \vec{\theta}, e \in s, p(s) \vdash e \in \sigma(s, p) \ \mathsf{true}. $$

3. We can also do unrestricted comprehension $\sigma'$, the kind that leads to Russell's paradox. It takes $p : (\mathsf{Set}) \to \Omega$ to $\sigma' p : \mathsf{Set}$. Assuming there is also $\epsilon : (\mathsf{Set}, \mathsf{Set}) \to \Omega$ and negation, we can define Russell's paradoxical $R$ as $\sigma' (\langle x : \mathsf{Set} \rangle . \lnot (x \in x))$.

4. For a "non-logical" example, let us introduce the $\lambda$-notation from $\lambda$-calculus. Suppose for every primitive types $A$ and $B$ there is a primitive type $A \Rightarrow B$ (normally written as $A \to B$ but I am using a different arrow to avoid confusion). For all primitive types $A$ and $B$, we can introduce an operator $\lambda_{A, B}$ which takes $f : (A) \to B$ to an expression $\lambda_{A,B} f : A \Rightarrow B$. The identity map on $A$ is thus written as $\lambda_{A,A} (\langle x : A \rangle . x)$. This is an example of a higher-order calculus of types with first-order logic layered on top of it (as opposed to HOL, where $\Omega$ is mixed with $\Rightarrow$ freely).

I do not know of any texts that would carefully developed this sort of calculus. I do not know why that is. Traditional logic textbooks usually simplify matters by considering a single-sorted first-order language, whereas the newer computer-sciency texts dive for fancier stuff with unrestricted order. You're asking for a bastard child of higher-order logic, I suppose.