Q

Overview

$\mathtt{Q}$ is the basic logic of domain specifiers and the ”at some domain” operator. It is a (modestly) infinitary free logic formulated in a language with genuinely syncategorematic expressions makes Quantificationalism consistent, and a theorem once minimal existence assumptions are added.

There are lots of interesting metaphysical questions that $\mathtt{Q}$ leaves open. Various extensions of $\mathtt{Q}$ exist that settle these questions one way or another.

Syntax

The language ${\mathcal{L}}_{†}$ is defined in two steps. First, we define a higher-order language ${\mathcal{L}}_{+}$ with syncategorematic operations $\mathsf{At},■$ (and quantifiers) and unrestricted $\lambda$-abstraction. Then, we define ${\mathcal{L}}_{†}$ as a sublanguage of ${\mathcal{L}}_{+}$ where $\lambda$-abstraction is suitably restricted so to ensure that expressions like

$$\lambda p.\mathsf{At}(F)(p)\lambda x.■Fx$$

are ill formed. These restrictions guarantee that domain specifiers and $■$ are genuinely syncategorematic.

More precisely, given a signature $\Sigma$, let ${\mathcal{L}}_{+}(\Sigma )$ be defined recursively as follows, where $M\cdot \sigma$ means that $M$ is a ${\mathcal{L}}_{+}(\Sigma )$ term of type $\sigma$:

Definition (Recursive definition of ${\mathcal{L}}_{+}(\Sigma )$)

1. $x\cdot \sigma$ whenever $x\in {Var}^{\sigma }$;
2. $C\cdot \sigma$ whenever $C\in {\Sigma }^{\sigma }$;
3. $MN\cdot \tau$ whenever $M\cdot \sigma \to \tau$ and $N\cdot \tau$
4. $\lambda x.M\cdot \sigma \to \tau$ whenever $M\cdot \tau$ and $x\in {Var}^{\sigma }$;
5. $QxP\cdot t$ whenever $x\in {Var}^t$, and $P\cdot t$, for $Q\in \{\forall ,\exists \}$,
6. $\mathsf{At}(\bar{F})(M)\cdot \tau$ whenever $\bar{F}:=(F_{\sigma }{)}_{\sigma \in \bar{\sigma }}$ such that $\bar{\sigma }$ is a finite, non-repeating sequence of types (a nice type sequence) and $F_{\sigma }\cdot \sigma \to t$ for each $\sigma \in \bar{\sigma }$^[: I abuse notation slightly and write $\sigma \in \bar{\sigma }$ to mean that $\sigma$ occurs in a sequence of types $\bar{\sigma }$] and $M\cdot \tau$.
7. $■P\cdot t$ whenever $P\cdot t$

I will call $\bar{F}$ as above nice term sequences. Notice that quantifiers are also treated as syncategorematic expressions. This for expressive power concerns: categorematic quantifiers are less expressive than syncategorematic ones in languages with restricted abstraction.

The abstractable variables of a term $M$ of type $\sigma$, ${\mathsf{AV}}_{\sigma }(M)$, are defined as those variables of type $\sigma$ that do not occur free, in $M$, within the scope of the second argument place of $\mathsf{At}$ or within the scope of $■$. More precisely,

Definition (Abstractable Variable)

1. ${\mathsf{AV}}_{\sigma }(x)={Var}^{\sigma }$ for $x\in {Var}^{\sigma }$;
2. ${\mathsf{AV}}_{\sigma }(C)={Var}^{\sigma }$ for $C\in {\Sigma }^{\sigma }$;
3. ${\mathsf{AV}}_{\sigma }(MN)={\mathsf{AV}}_{\sigma }(M)\cap {\mathsf{AV}}_{\sigma }(N)$;
4. ${\mathsf{AV}}_{\sigma }(\lambda x.M)={\mathsf{AV}}_{\sigma }(M)$;
5. ${\mathsf{AV}}_{\sigma }(QxP)={\mathsf{AV}}_{\sigma }(P)$ for $Q\in \{\forall ,\exists \}$;
6. ${\mathsf{AV}}_{\sigma }(\mathsf{At}(\bar{F})(M))={\mathsf{AV}}_{\sigma }(\bar{F})\setminus {\mathsf{FV}}_{\sigma }(M)$;
7. ${\mathsf{AV}}_{\sigma }(■P)={Var}^{\sigma }\setminus {\mathsf{AV}}_{\sigma }(P)$

The language ${\mathcal{L}}_{†}(\Sigma )$ is then defined the same way as ${\mathcal{L}}_{+}(\Sigma )$, except that the clause for $\lambda$-abstraction is replaced with

• $\lambda x.M\cdot \sigma \to \tau$ whenever $M\cdot \tau$ and $x\in \mathsf{AV}^\sigma(M)$;

Note ${\mathcal{L}}_{†}(\sigma )\subseteq {\mathcal{L}}_{+}(\Sigma )$. When discussing ${\mathtt{Q}}_{†}$ I reserve the notation $M:\sigma$ to mean that $M$ is a ${\mathcal{L}}_{†}$-term of type $\sigma$.

We assume we are always working in a signature containing:

• Existence predicates ${\mathsf{E}!}_{\sigma }:\sigma \to t$;
• Applicative indiscernibility predicates ${\equiv }_{\sigma }:\sigma \to \sigma \to t$

We let $\Lambda$ be the signature containing the usual Boolean operators and the above, and omit reference to signatures when $\Lambda$ is intended.

Background Higher-Order Logic

The background higher-order logic is ${\mathtt{FH}}_{†}$, a higher-order free logic formulated in ${\mathcal{L}}_{†}$. It uses primitive existence predicates ${\mathsf{E}!}_{\sigma }$, though these are definable up to provable equivalence as $\lambda x^{\sigma }.\exists y(x\equiv y)$. I use primitive existence predicates because existence has a central theoretical role in quantificationalism.

Axioms of ${\mathtt{FH}}_{†}$

$$\begin{array}{rlr}& ⊢P& \text{P a classical tautology}\\ & ⊢\forall x\mathsf{E}!x& \\ & ⊢\mathsf{E}!a\to (\forall yP\to P[y/a])& \\ & \forall x(P\to Q)\to (\forall xP\to \forall xQ)& \\ & ⊢M\equiv M& \\ & ⊢(M\equiv N)\to FM\to FN& \\ & ⊢M\equiv N& M,N\text{βη-equivalent}\\ P,P\to Q& ⊢Q& \\ \text{If }\Gamma & ⊢P\text{, then }\Gamma ⊢\forall xP& \end{array}\text{\hspace{1em}(Taut)(∀E!)(FrUI)(Norm)(Refl)(LL)(βη)(MP)(UG)}$$

Notice that $M\equiv N$ does not guarantee intersubstitutivity in all contexts: it’s applicative indiscernibility, not identity.

Axioms of ${\mathtt{Q}}_{†}$

${\mathtt{Q}}_{†}$ is an extension of ${\mathtt{FH}}_{†}$ with axioms for domain specifiers and $■$. Here they are, in turn.

Axioms for Domain Specifiers

Here are the axioms of ${\mathtt{Q}}_{†}$ concerning domain specifiers but not $■$

Axioms for domain specifiers

$$\begin{array}{rlr}& ⊢\mathsf{At}(\overline{\mathsf{E}!})(M)\equiv M& \\ & ⊢\mathsf{At}(\bar{F})(MN)\equiv (\mathsf{At}(\bar{F})(M))(\mathsf{At}(\bar{F})(N))& \\ & ⊢\mathsf{At}(\bar{F})(\mathsf{At}(\bar{G})(M))\equiv \mathsf{At}(\bar{F}\bullet \bar{G})(M)& \\ & ⊢\mathsf{At}(\bar{F})(M)\equiv \mathsf{At}(\bar{G})(M)& \text{Fˉ,Gˉ permutations}\\ & ⊢\mathsf{At}(\bar{F})(♡)\equiv ♡& ♡\in \{\wedge ,\neg ,\equiv \}\\ & ⊢\mathsf{At}(\bar{F})(M)\equiv M& \text{M a combinator}\\ & ⊢\mathsf{At}(\bar{F})({\mathsf{E}!}_{\sigma })\equiv F_{\sigma }& \text{when Fσ defined}\\ & ⊢\mathsf{At}(\bar{F})({\mathsf{E}!}_{\sigma })\equiv {\mathsf{E}!}_{\sigma }& \text{otherwise}\\ \text{If }& ⊢P,\text{ then }⊢\mathsf{At}(\bar{F})(P)& \\ \text{If }\Gamma & ⊢\mathsf{At}(\bar{F})(P),\text{ then }\Gamma ⊢\mathsf{At}(\bar{F})(\forall xP)& \end{array}\text{\hspace{1em}(Id)(App)(CompG)(Perm)(Stab♡)(Stabλ)(Gen)(Mod)(At Nec)(AtUG)}$$

Notice that adding these axioms and rules to $\mathtt{FH}$ yields a finitary logic. Infinitarity is only introduced by $■$.

Here are some important groups of axioms.

---

Existence axioms of ${\mathtt{Q}}_{†}$

$$\begin{array}{rlr}& ⊢\mathsf{At}(\overline{\mathsf{E}!})(M)\equiv M& \\ & ⊢\mathsf{At}(\bar{F})({\mathsf{E}!}_{\sigma })\equiv F_{\sigma }& \text{when Fσ defined}\\ & ⊢\mathsf{At}(\bar{F})({\mathsf{E}!}_{\sigma })\equiv {\mathsf{E}!}_{\sigma }& \text{otherwise}\end{array}\text{\hspace{1em}(Id)(Gen)(Mod)}$$

The existence axioms capture the core of the idea that a domain specifier $\mathsf{At}(F^{\sigma \to t})$ forces quantification over entities of type $\sigma$ to range over precisely the $F$s:

1. To specify the existing${}_{\sigma }$ things as the new domain of quantification is to change nothing at all (Id);
2. To exist among the $F_{\sigma }$ is to be an $F_{\sigma }$ (Gen);
3. To exist${}_{\tau }$ among the $F^{\sigma }\to t$ is to exist${}_{\tau }$: changing the domain of quantification over things of type $\tau$ does not alter the domains of quantification at other types (Mod).

---

Action axioms of ${\mathtt{Q}}_{†}$

$$\begin{array}{rl}& ⊢\mathsf{At}(\overline{\mathsf{E}!})(M)\equiv M\\ & ⊢\mathsf{At}(\bar{F})(MN)\equiv (\mathsf{At}(\bar{F})(M))(\mathsf{At}(\bar{F})(N))\\ & ⊢\mathsf{At}(\bar{F})(\mathsf{At}(\bar{G})(M))\equiv \mathsf{At}(\bar{F}\bullet \bar{G})(M)\end{array}\text{\hspace{1em}(Id)(App)(CompG)}$$

The action axioms are object language counterparts to the idea that domain specifiers express metaphysical substitutions acting on propositions, properties and relations.

1. There is an identity substitution, expressed by $\mathsf{At}(\mathsf{E}!)$ (Id);
2. Substitutions commute with application (App);
3. Substitutions compose (CompG): the definition of $\bar{F}\bullet \bar{G}$ is

$$(\bar{F}\bullet \bar{G}{)}_{\sigma }:=\{\begin{array}{ll}\mathsf{At}(\bar{F})(G_{\sigma })& \text{if Fσ is defined;}\\ F_{\sigma }& \text{if Gσ is defined but Fσ is not;}\\ \text{undefined}& \text{otherwise}\end{array}$$

matching the way substitutions compose in the QSSs.

---

Stability axioms of ${\mathtt{Q}}_{†}$

$$\begin{array}{rlr}& ⊢\mathsf{At}(\bar{F})(♡)\equiv ♡& ♡\in \{\wedge ,\neg ,\equiv \}\\ & ⊢\mathsf{At}(\bar{F})(M)\equiv M& \text{M a combinator}\end{array}\text{\hspace{1em}(Stab♡)(Stabλ)}$$

The stability axioms specify the minimal theoretical role of stability. At a minimum, Boolean operators, applicative indiscernibility, and combinators do not involve quantification.

Axioms for $■$

Here are the axioms and rules for $■$

Axioms for $■$

$$\begin{array}{rl}& ⊢■P\to \mathsf{At}(\bar{F})(P)\\ & ⊢■(M\equiv N)\to (P[M/x]\to P[N/x])\\ \text{If }\Gamma & ⊢\mathsf{At}(\bar{F})(\mathsf{At}(\bar{X})(P))\text{ for all neutral Xˉ, then }\Gamma ⊢\mathsf{At}(\bar{F})(■P)\end{array}\text{\hspace{1em}(Master)(SLL)(Surj)}$$

We call a nice term sequence $\bar{X}$ neutral when no variable in $\bar{X}$ occurs free in any of $\Gamma ,P,\bar{F}$.

The two axioms capture, respectively, the idea that $■$ is broader than every domain specifier, and the idea that identity is applicative indiscernibility at all domains: $■$-necessitated applicative equivalence suffices for intersubstitutivity in all contexts.

The inference rule is infinitary and used as an introduction rule for $■$. Using an infinitary rule provides a way of generalizing over domains that gets around the limitations of both free quantification and the inability to quantify over types in the object language. The infinitarity of (Surj) is fairly harmless: proofs in ${\mathtt{Q}}_{†}$ can be infinitely long, but not infinitely wide.