Frege’s Concept Horse Paradox in the Simply-Typed λ-calculus

In “On Function and Concept,” Gottlob Frege makes a distinction between concepts and objects. Specifically, he claims that objects are saturated object-expressions while concepts are unsaturated function-expressions. My goal is to illuminate what the object-concept distinction entails in the context of simply-typed lambda calculus $(\lambda^{\rightarrow})$ and whether or not this entailment is susceptible to problems like the $\mathtt{\text{concept horse paradox}}$.


Frege’s “On Function and Concept” (1892) claims that there is a substantive difference between concepts and objects. This distinction is described on pg. 147:

Statements in general, just like equations or inequalities or expressions in Analysis, can be imagined to be split up into two parts; one complete in itself, and the other in need of supplementation, or ‘unsaturated’. Thus, e.g., we split up the sentence ‘Caesar conquered Gaul’ into ‘Caesar’ and ‘conquered Gaul’.

Definition 1. Complete parts of statements are ‘saturated’ while incomplete ones are ‘unsaturated’.

Example 1. Consider the following statement:

$$\text{‘Fido jumped over the fence’}$$

By Definition 1, we can see that (1) is split up into the saturated ‘Fido’ object-expression and ‘jumped over the fence’ unsaturated function-expression.

Remark 1. These two categories, as it turns out, have simple analogues in $\lambda^{\rightarrow}$. Unsaturated function-expressions are terms with functional types, e.g. $N^{\sigma\rightarrow\tau}$ or $N:\sigma\rightarrow\tau$, while saturated object-expressions are terms with non-functional types, e.g. $M^{\sigma}$ or $M:\sigma$.

Definition 2. We say that if $M$ gets type $\sigma$ and $N$ gets type $\sigma\rightarrow\tau$ then the application $NM$ is legal (as $N$ is considered a function from terms of type $\sigma$ to terms of type $\tau$) and gets type $\tau$.

Definition 3. The set of types of $\lambda^{\rightarrow}$, denoted by Type($\lambda^{\rightarrow}$) is inductively defined as follows. We write $\mathbb{T}=\text{Type}(\lambda^{\rightarrow})$ where

                $\begin{array}{ll}\alpha,\alpha^{\prime},\alpha^{\prime\prime},\ldots\in\mathbb{T} & \text{(type variables);}\\\sigma,\tau\in\mathbb{T}\Rightarrow(\sigma\rightarrow\tau)\in\mathbb{T} &\text{(function space variables).}\end{array}$

Definition 4. We will now define a new variant of $\mathbb{T}$ that more closely models Frege’s natural language notions of concept and object. This new variant, $\mathbb{T_{\mathcal{F}}}$, has the following restrictions:

  1. There are three and only three types: $\begin{cases}\alpha\in\mathbb{T_{\mathcal{F}}} & \text{(}objects\text{);}\\\mathbf{\text{H}}\in\mathbb{T_{\mathcal{F}}} & \text{(truth-values);}\\(\alpha\rightarrow\mathbf{\text{H}})\in\mathbb{T_{\mathcal{F}}} & \text{(}concepts\text{).}\end{cases}$
  2. Objects have an unrestricted domain.
  3. A truth-value is a boolean type where $\mathbf{\text{H}}=\{\text{‘true’},\text{‘false’}\}$.
  4. A concept is a functional type that takes an object as an input and returns a truth value. This mapping is done by some valuation function $v$ where $v$ maps to $\text{‘true’}$ if the function-expression applied to the argument(s) is true, e.g., in (1), if Fido did jump over a fence then $v(\text{‘Fido’})=\text{‘true’}$; otherwise, $v$ maps to $\text{‘false’}$.
  5. Note that $(\mathbf{\text{H}}\rightarrow\alpha)\notin\mathbb{T_{\mathcal{F}}}$.

Remark 2. Until otherwise noted, we will work only with types in $\mathbb{T_{\mathcal{F}}}$.

Definition 5. Let $M$ be an untyped $\lambda^{\rightarrow}$-term. Given the non-functional type $\alpha$, we say that $M:\alpha$ is a saturated object-expression, or simply an object.

Definition 6. Let $N$ be an untyped $\lambda^{\rightarrow}$-term. Given the functional type $\alpha\rightarrow\mathbf{\text{H}}$, we say that $N:\alpha\rightarrow\mathbf{\text{H}}$ is an unsaturated function-expression, or simply a concept.

Definition 7. We will now make a semantic distinction between two kinds of uses of the token ‘is’ in natural language. To illustrate the distinction, consider:

  1. ‘Mark Twain is Samuel Clemens’: here, we have the ‘is’ of identity, or $x=x$. The equality operator $=$ is used as a mathematical formalism and may not necessarily be computable in $\lambda^{\rightarrow}$. So, $v(\text{‘Mark Twain’})=\text{‘true’}$ iff $\text{‘Mark Twain’}=\text{‘Samuel Clemens’}$.
  2. ‘Mark Twain is dead’: here, we have the ‘is’ of predication which, if combined with some property $P$ will yield a functional type of form $\alpha\rightarrow\mathbf{\text{H}}$ for some object $\alpha$. As in Definition 4, if $\alpha$ has property $P$, $v(\alpha)=\text{‘true’}$; otherwise, $v$ maps to $\text{‘false’}$.

Simple Natural Language Sentences in $\lambda^{\rightarrow}$

Lemma 1. Consider the same sentence from Example 1:

$$\text{‘Fido jumped over the fence’}$$

This sentence can be formulated in $\lambda^{\rightarrow}$ like so:

$$\Gamma\vdash J:\alpha\rightarrow\mathbf{\text{H}},\,\Gamma\vdash F:\alpha\Rightarrow\Gamma\vdash(JF):\mathbf{\text{H}}$$

Proof. We will set the object-expression ‘Fido’ $=F$ and the (one-place) function-expression ‘$\left(x\right)$ jumped over the fence’ $=J\left(x\right)$. Note that we will drop the $\left(x\right)$ in practice for $\lambda$-calculus wff satisfiability. By Definition 5, $F$ must be of type $\alpha$. And to make $(JF)$ legal, by Definition 2, $J$ must be of type $\alpha\rightarrow\mathbf{\text{H}}$. Therefore, a correctly typed $(JF)$ from $J:\alpha\rightarrow\mathbf{\text{H}}$ and $F:\alpha$ looks like
which is precisely what we wanted to show in (3). $\square$

Proof. We can also derive a more formally-rigorous proof. Consider:
$$\dfrac{\Gamma\vdash J:\alpha\rightarrow\mathbf{\text{H}}\,\,\,\,\,\,\,\Gamma\vdash F:\alpha}{\Gamma\vdash JF:\mathbf{\text{H}}}{\scriptscriptstyle (\rightarrow e)}$$

where we get the same result: $JF$ is of type $\mathbf{\text{H}}$. $\square$

Remark 3. Natural language predicates (e.g. ‘is blue’, ‘jumped over the fence’, ‘is a concept’, ‘conquered Gaul’, ‘may have stolen my wallet’, etc.) are concepts in $\mathbb{T_{\mathcal{F}}}$ while subjects, be they proper nouns, improper nouns, pronouns, etc. (e.g. ‘the car’, ‘Fido’, ‘he’, ‘the tall man’, ‘the Brooklyn Bridge’, etc.) are objects. We will now look at more nontrivial examples of natural language propositions and attempt to model them in $\lambda^{\rightarrow}$ under $\mathbb{T_{\mathcal{F}}}$.

Example 2. Consider the statement

$$\text{‘The concept horse is a concept.’}$$

Claim 1. We will set the object-expression ‘The concept horse’ $=T_{ch}$ and the (one-place) function-expression ‘$\left(x\right)$ is a concept’ $=C$. Example 2 is witness to a semantic ambiguity between natural language and our type system ($\mathbb{T_{\mathcal{F}}}$). More specifically, (6) evaluates to ‘true’ in natural language, but ‘false’ under $\mathbb{T_{\mathcal{F}}}$, i.e. $CT_{ch}:\mathbf{\text{H}}$ has an ambiguous truth-value. So, if $T_{ch}:\alpha$ is the saturated object-expression ‘the concept horse’ and $C:\alpha\rightarrow\mathbf{\text{H}}$ is the unsaturated function-expression ‘is a concept’, then the mapping $v:\alpha\rightarrow\mathbf{\text{H}}$ is ambiguous.

Proof. Consider the following natural language statement

$$\text{‘The house is a house.’}$$

Trivially, (7) is true. Per Definition 7, the ‘is’ here seems to be an ‘is’ of identity, so $v(\text{‘house’})=\text{‘true’}$ since $\text{‘house’}=\text{‘house’}$.

Now, let’s define a new set of types $\mathbb{T_{\mathcal{F}}^{\mathrm{*}}}$ where $\mathbb{T_{\mathcal{F}}^{\mathrm{*}}}$ is just like $\mathbb{T_{\mathcal{F}}}$ except that $\mathbb{T_{\mathcal{F}}^{\mathrm{*}}}$ has one and only one additional type: $\beta\in\mathbb{T_{\mathcal{F}}^{\mathrm{*}}}$. We will call all terms of type $\beta$ houses. Now, we have an ambiguity in (7); it is unclear whether we’re asking if the identity $\text{‘house’}=\text{‘house’}$ holds or whether we’re asking if the saturated object-expression ‘the house’ is of type $\beta$. The former is true per the first half of this proof. The latter is false, as any object-expression is of type $\alpha$ in $\mathbb{T_{\mathcal{F}}}$ and, by extension, also in $\mathbb{T_{\mathcal{F}}^{\mathrm{*}}}$ and $\alpha\neq\beta$. This same kind of ambiguity happens in (7). $\square$

Definition 8. Given the proof of Claim 1, we will now denote two variations of $v$, essentially defining two valuations for $\alpha\rightarrow\mathbf{\text{H}}$:

  1. $v_{0}$ for meta-language predicates;
  2. $v_{\mathfrak{L}}$ for natural language predicates.

In light of this, we now have two interpretations for statements that involve objects, concepts, and truth-values. So, in some cases, $v_{0}(CT_{ch}:\mathbf{\text{H}})$ will evaluate to ‘false’, but $v_{\mathfrak{L}}(CT_{ch}:\mathbf{\text{H}})$ evaluates to ‘true’ or vice-versa. This is known as the $\mathtt{\text{concept horse paradox}}$.

Theorem 1. Given any object-expression, $\mathbb{O}:\alpha$, and if we let the function-expression ‘$\left(x\right)$ is a concept‘ $=C$, $v_{0}(C\mathbb{O}:\mathbf{\text{H}})$ will always evaluate to ‘false’.

Proof. From the proof of Claim 1 and Definition 8. $\square$

Example 3. Now consider the statement:

$$\text{‘Seabiscuit is the concept horse.’}$$

Claim 2. We will set the object-expression ‘Seabiscuit’ $=S$ and the (one-place) function-expression ‘$\left(x\right)$ is the concept horse’ $=C_{h}$. Example 3 avoids the ambiguity in (6) because its truth value happens to be false under both valuations, so $v_{0}(C_{h}S:\mathbf{\text{H}})=v_{\mathfrak{L}}(C_{h}S:\mathbf{\text{H}})$.

Proof. By Theorem 1, $v_{0}(C_{h}S:\mathbf{\text{H}})$, will always evaluate to ‘false’. In natural language, ‘Seabiscuit’ is not ‘the concept horse’ (at best, it is an instance of ‘the concept horse’), so $v_{\mathfrak{L}}(C_{h}S:\mathbf{\text{H}})$ will evaluate to ‘false’ here as well. Since both valuations return ‘false’, we avoid the paradox. $\square$

Example 4. Consider the statement:

$$\text{‘Anna is something Bill is not — namely, a student.’}$$

Remark 4. Example 4 is not ambiguous as it only uses terms found in natural language. This is trivial to prove (since the only valid valuation is $v_{\mathfrak{L}}$) However, (9) introduces another problem with $\mathbb{T_{\mathcal{F}}}$ (more specifically, with $\lambda^{\rightarrow}$): subtyping. It seems intuitive that ‘being a student’ should be a member of ‘things Bill is not’. As it turns out, $\lambda^{\rightarrow}$ has no way of representing this.

Proposed Solution: Semantic Culling

The most straightforward solution to the semantic problem of the $\mathtt{\text{concept horse paradox}}$ is a simple one. Instead of using terms like concept and object, that not only have a meaning in the meta-language, but also in natural languages, we will use terms that have no meaning in natural language. Consider a new type system, $T_{\mathcal{F}}^{\mathrm{**}}$.

The types of $\mathbb{T_{\mathcal{F}}^{\mathrm{*}}}$: $\begin{cases}\alpha\in\mathbb{T_{\mathcal{F}}} & \text{(}foo\text{);}\\\mathbf{\text{H}}\in\mathbb{T_{\mathcal{F}}} & \text{(baz);}\\(\alpha\rightarrow\mathbf{\text{H}})\in\mathbb{T_{\mathcal{F}}} & \text{(}foobaz\text{).}\end{cases}$

Under such a schema, statements like ‘The concept horse is [a] foobaz’ are meaningless in natural language, but are semantically well-formed in the meta-language. Thus, we can infer that we need to valuate the statement with $v_{0}$ as opposed to $v_{\mathfrak{L}}$ and avoid any ambiguity.

Remark 5. The caveat here is that we lose some expressiveness in natural languages. In Example 3, we were able to refer both to the semantics of natural language and the meta-language without ambiguity. This would no longer be possible.

Proposed Solution: Syntactic Sugar

Another proposed solution is syntactic in nature. We previously showed that ‘Fido jumped over the fence’ (Example 1) can be formulated as follows:

$$\dfrac{\Gamma\vdash J:\alpha\rightarrow\mathbf{\text{H}}\,\,\,\,\,\,\,\Gamma\vdash F:\alpha}{\Gamma\vdash JF:\mathbf{\text{H}}}{\scriptscriptstyle (\rightarrow e)}$$

We will now introduce a new type of $\lambda^{\rightarrow}$-term that will differentiate between what valuation $v$ one should use to determine the truth-value of some $M:\mathbf{\text{H}}$. To do this, consider a new type system $\mathbb{T_{\mathcal{F}}^{\mathrm{\omega}}}$.

The types of $\mathbb{T_{\mathcal{F}}^{\mathrm{\omega}}}$: $\begin{cases} \alpha\in\mathbb{\mathbb{T_{\mathcal{F}}^{\mathrm{\omega}}}} & \text{(}objects\text{);}\\\mathbf{\text{H}}\in\mathbb{T_{\mathcal{F}}^{\mathrm{\omega}}} & \text{(truth-values);}\\(\alpha\rightarrow\omega\rightarrow\mathbf{\text{H}})\in\mathbb{T_{\mathcal{F}}^{\mathrm{\omega}}} & \text{(unrestricted }concepts\text{);}\\(\omega\rightarrow\mathbf{\text{H}})\in\mathbb{T_{\mathcal{F}}^{\mathrm{\omega}}} & \text{(restricted }concepts\text{);} \\\omega\in\mathbb{T_{\mathcal{F}}^{\mathrm{\omega}}} & \text{(}\textbf{worlds}\text{).} \end{cases}$

A derivation of (10) would now look like the following:

$$\dfrac{\dfrac{\Gamma\vdash J:\alpha\rightarrow\omega\rightarrow\mathbf{\text{H}}\,\,\,\,\,\,\,\Gamma\vdash F:\alpha\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,}{\Gamma\vdash JF:\omega\rightarrow\mathbf{\text{H}}\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\Gamma\vdash W:\omega}{\scriptscriptstyle (\rightarrow e)}}{\Gamma\vdash JFW:\mathbf{\text{H}}}{\scriptscriptstyle (\rightarrow e)}$$

The purpose of $W$ is to pick out one (or several, if there are no ambiguities) valuating function(s). So, in Example 1, $W$ picks out $v_{\mathfrak{L}}$, in Example 3, $W$ picks out $\{v_{\mathfrak{L}},v_{0}\}$, and in Example 2, $W$ either picks out $v_{\mathfrak{L}}$ or $v_{0}$ but not both. A benefit of $W:\omega$ is that it can pick out the meta-language ($v_{0}$), meta-meta-language ($v_{1}$), meta-meta-meta-langauge ($v_{2}$), etc. ($v_{n}$). Furthermore, $W$ can also pick out combinations of languages ($\{v_{\mathfrak{L}},v_{0},v_{2},v_{n}\}$), provided the truth value stays consistent.

Remark 6. A caveat of this syntactic addition is that $W$ tends to be implicit and thus, the $\mathtt{\text{concept horse paradox}}$ merely shifts (now we have an ambiguity of $W$) and does not completely disappear. A rather elegant fix is letting $W$ pick out $v_{\mathfrak{L}}$ by default. In such a case, the paradox would dissolve and we would still preserve the truth-value in sentences like Example 3.