<p>I would recommend looking at higher-order logics (HOL), for instance Lambek and Scott's <a href="https://books.google.si/books/about/Introduction_to_Higher_Order_Categorical.html?id=6PY_emBeGjUC&amp;redir_esc=y" rel="nofollow noreferrer">Introduction to Higher-Order Categorical Logic</a>. 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).</p>

<p>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.</p>

<p>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 <span class="math-container">$\Omega$</span>, which are closed under formation of function spaces, so that higher-order predicates are formed as <span class="math-container">$\Omega$</span>, <span class="math-container">$A \to \Omega$</span>, <span class="math-container">$(A \to \Omega) \to \Omega$</span>. To prevent these, we can stratify the types into several sorts:</p>

<ul>
<li>the sort of <em>primitive types</em> <span class="math-container">$A$</span>, <span class="math-container">$B$</span>, <span class="math-container">$C$</span>, ... (in first-order logic you often have just a single one, which is not mentioned at all) </li>
<li>the sort of <em>propositions</em> <span class="math-container">$\Omega$</span></li>
<li>the sort of <em>first-order functions</em> <span class="math-container">$(A_1, \ldots, A_n) \to B$</span>, where <span class="math-container">$A_i$</span> and <span class="math-container">$B$</span> are primitive types</li>
<li>the sort of <em>(first-order) propositional functions</em> <span class="math-container">$(A_1, \ldots, A_n) \to \Omega$</span>, where <span class="math-container">$A_i$</span> are primitive types.</li>
</ul>

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

<p>If <span class="math-container">$S$</span> is a sort, we write <span class="math-container">$\Gamma \vdash e : S$</span> when <span class="math-container">$e$</span> is an expression of sort <span class="math-container">$S$</span> in context <span class="math-container">$\Gamma$</span>. For example,
<span class="math-container">$$x : \mathbb{R}, y : \mathbb{R} \vdash (\exists z : \mathbb{R} . x + z = y) : \Omega$$</span>
is the assertion that <span class="math-container">$\exists z : \mathbb{R} . x + z = y$</span> is a proposition (in the given context). It is <em>not</em> the assertion that <span class="math-container">$\exists z : \mathbb{R} . x + z = y$</span> holds! For that we postulate a new judgement of the form
<span class="math-container">$$\Gamma \mid \theta_1, \ldots, \theta_n \vdash \psi \ \mathsf{true}
\tag{1}$$</span>
which states, intuitively, that propositions <span class="math-container">$\theta_1, \ldots, \theta_n$</span> jointly entail the proposition <span class="math-container">$\psi$</span>. If we also have equations (at all types), (1) can be replaced with
<span class="math-container">$$\Gamma \mid (\theta_1 \land \cdots \land \theta_n) \land \psi =_\Omega \theta_1 \land \cdots \land \theta_n.$$</span>
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.</p>

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

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

<ol>
<li><p><span class="math-container">$\forall$</span> is an operation which takes a propositional function <span class="math-container">$(A) \to \Omega$</span> to a proposition. The formation rule would read as follows:
<span class="math-container">$$\frac{\Gamma \vdash p : (A) \to \Omega}{\Gamma \vdash \forall p : \Omega}$$</span>
En example of such an expression would be <span class="math-container">$\forall (\langle x : \mathbb{R} \rangle . x^4 - 5 x^2 + 7 &gt; 0)$</span>.</p></li>
<li><p>Assuming there is a primitive type <span class="math-container">$\mathsf{Set}$</span> of sets and a relation symbol <span class="math-container">$\in$</span> of sort <span class="math-container">$(\mathsf{Set}, \mathsf{Set}) \to \Omega$</span>, subset formation <span class="math-container">$\sigma$</span> is an operation which takes <span class="math-container">$s : \mathsf{Set}$</span> and <span class="math-container">$p : (\mathsf{Set}) \to \Omega$</span> and yields <span class="math-container">$\sigma(s, p) : \mathsf{Set}$</span>. We also need some rules regarding these, e.g.,
<span class="math-container">$$
\Gamma \mid \vec{\theta}, e \in s, p(s) \vdash e \in \sigma(s, p) \ \mathsf{true}.
$$</span></p></li>
<li><p>We can also do unrestricted comprehension <span class="math-container">$\sigma'$</span>, the kind that leads to Russell's paradox. It takes <span class="math-container">$p : (\mathsf{Set}) \to \Omega$</span> to <span class="math-container">$\sigma' p : \mathsf{Set}$</span>. Assuming there is also <span class="math-container">$\epsilon : (\mathsf{Set}, \mathsf{Set}) \to \Omega$</span> and negation, we can define Russell's paradoxical <span class="math-container">$R$</span> as <span class="math-container">$\sigma' (\langle x : \mathsf{Set} \rangle . \lnot (x \in x))$</span>.</p></li>
<li><p>For a "non-logical" example, let us introduce the <span class="math-container">$\lambda$</span>-notation from <span class="math-container">$\lambda$</span>-calculus. Suppose for every primitive types <span class="math-container">$A$</span> and <span class="math-container">$B$</span> there is a primitive type <span class="math-container">$A \Rightarrow B$</span> (normally written as <span class="math-container">$A \to B$</span> but I am using a different arrow to avoid confusion). For all primitive types <span class="math-container">$A$</span> and <span class="math-container">$B$</span>, we can introduce an operator <span class="math-container">$\lambda_{A, B}$</span> which takes <span class="math-container">$f : (A) \to B$</span> to an expression <span class="math-container">$\lambda_{A,B} f : A \Rightarrow B$</span>. The identity map on <span class="math-container">$A$</span> is thus written as <span class="math-container">$\lambda_{A,A} (\langle x : A \rangle . x)$</span>. 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 <span class="math-container">$\Omega$</span> is mixed with <span class="math-container">$\Rightarrow$</span> freely).</p></li>
</ol>

<p>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.</p>

CC BY-SA 4.0
2019-07-23T07:56:53.693Z
2019-07-23T08:10:32.593Z
2019-07-23T08:10:32.593Z
Andrej Bauer
<p>First order logic comes equipped with two kinds of terms:</p>

<ol>
<li>Variable: those terms of the form <span class="math-container">$x$</span> for some variable <span class="math-container">$x$</span>, of which there are infinite.</li>
<li>Function application: those terms of the form <span class="math-container">$f(t_1,\dots,t_n)$</span> for some <span class="math-container">$n$</span>-place function symbol <span class="math-container">$f$</span>, of which there are infinite, and some <span class="math-container">$n$</span> terms <span class="math-container">$t_1, \dots, t_n$</span>.</li>
</ol>

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

<p>One way to introduce set descriptor terms into the logic, which then will no longer be a first order logic, so lets call it <em>extended first order logic</em>, is by introducing an infinite set of <em>binding term constructors</em> 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: <span class="math-container">$Cx\varphi$</span>, for every binding term constructor <span class="math-container">$C$</span>, every variable <span class="math-container">$x$</span>, and every extended first order well-formed formula <span class="math-container">$\varphi$</span> (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 <em>binding terms</em>.</p>

<p>We can now set aside one of the new-fangled binding term constructors, say <span class="math-container">$\sigma$</span>, and interpret every binding term of the form <span class="math-container">$\sigma x\varphi$</span> as <span class="math-container">$\{x:\varphi\}$</span>.</p>

<p>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: <a href="https://en.wikipedia.org/w/index.php?title=Epsilon_calculus&amp;oldid=879234427#Epsilon_operator" rel="nofollow noreferrer">Hilbert's epsilon operator and Bourbaki's <span class="math-container">$\tau$</span> operator</a>, which, though similar, are not the same operator, as they satisfy slightly different axioms.</p>

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

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

CC BY-SA 4.0
2019-07-22T23:26:37.370Z
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.
Andrej Bauer
CC BY-SA 4.0
2019-07-23T03:27:40.513Z
@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.
Evan Aad
CC BY-SA 4.0
2019-07-23T07:23:32.253Z
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.
Andrej Bauer
CC BY-SA 4.0
2019-07-23T21:57:08.910Z
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.
Andreas Blass
<reference-request><first-order-logic>
A first order logic extended with binding terms like the familiar set descriptors $\{x:\varphi\}$
Evan Aad
# A first order logic extended with binding terms like the familiar set descriptors $\{x:\varphi\}$

(Asked by: username_0 on 2019-07-20)

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](https://en.wikipedia.org/w/index.php?title=Epsilon_calculus&oldid=879234427#Epsilon_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?

**Tags:** reference-request, first-order-logic

> **Comments:**
> **username_1**: 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.  
> **username_0**: @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.  
> **username_1**: 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.  
> **username_2**: 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.  

---

## 1 answers

### Answer by username_1 on 2019-07-23. Score: 4

I would recommend looking at higher-order logics (HOL), for instance Lambek and Scott's [Introduction to Higher-Order Categorical Logic](https://books.google.si/books/about/Introduction_to_Higher_Order_Categorical.html?id=6PY_emBeGjUC&redir_esc=y). 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.


---

