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?

  • 2
    $\begingroup$ Well, type theory certainly comes to mind, as it is a formal system which does not stratify everything into terms and formulas, and it takes proper account of binding. You could also use higher-order logic, i.e., $\lambda$-calculus with a type of truth values $\Omega$, and a suitable comprehension rule. $\endgroup$ Jul 22 '19 at 23:26
  • $\begingroup$ @AndrejBauer: Thanks. But this is not what I'm looking for. I'm looking for a first order predicate logic extended with a way of creating terms from formulas that introduces a binding scope restricted to the terms. $\endgroup$
    – Evan Aad
    Jul 23 '19 at 3:27
  • 2
    $\begingroup$ My point is twofold. First, if you're going to labor to define binding scopes, it'll be as easy doing first-order on steroids as something higher-order. Second, higher-order logics already have dealt with binding scopes and such, so that's where you can look and then just cut down on the order. $\endgroup$ Jul 23 '19 at 7:23
  • 1
    $\begingroup$ Here's the MathSciNet information for a paper that looks like what you requested: MR0305970 Corcoran, John; Hatcher, William; Herring, John Variable binding term operators. Z. Math. Logik Grundlagen Math. 18 (1972), 177–182. $\endgroup$ Jul 23 '19 at 21:57

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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.