Structure by proxy, with an application to grounding

Abstract

An argument going back to Russell shows that the view that propositions are structured is inconsistent in standard type theories. Here, it is shown that such type theories may nevertheless provide entities which can serve as proxies for structured propositions. As an illustration, such proxies are applied to the case of grounding, as standard views of grounding require a degree of propositional structure which suffices for a version of Russell’s argument. While this application solves some of the problems grounding faces, it introduces problematic limitations: it becomes impossible to quantify unrestrictedly over the relata of ground. The proposed proxies may thus not save grounding, but they shed light on what exactly Russell’s argument does and does not show.

Appendix

Let P be the set of instances of the following schema:

• $P_t\bar{\varepsilon }=\pi _\varepsilon$    (for $t=\tau _\varepsilon$)

We show that P is consistent with classical logic by a standard model construction.

Standard models for functional type theory associate each type with a domain, containing the denotations of expressions of the relevant type. In the simplest models, the domain of type s is $\{0,1\}$, with 0 representing falsity and 1 representing truth, and for any functional type $(t_1\rightarrow t_2)$, the domain of type $(t_1\rightarrow t_2)$ is the set of functions from the domain of type $t_1$ to the domain of type $t_2$. In this very simple setting, a model is given by a set D, serving as the domain of type i, and an interpretation function I, mapping each constant c of some type to an element I(c) of the domain of that type. Such an interpretation function I is extended to map each expression, simple or complex, to an element of the domain of its type: writing $[e]_M$ for the interpretation of an expression e in a model M consisting of an individual domain D and an interpretation function I, let, for any constant c and complex expression (fa):

• $[c]_M=I(c)$

• $[(fa)]_M=[f]_M([a]_M)$

Call $[e]_M$ the denotation of e (in M). Such a model validates the principles of classical logic if it interprets the logical constants in the expected way. E.g., in the case of $\lnot$, this means mapping 0 to 1 and vice versa. For the following, we assume furthermore that there is a term $\bar{\varepsilon }$ of type i for every term $\varepsilon$, and that I interprets it as intended, i.e., as the expression $\varepsilon$. This requires, of course, that D contains all expressions of the language. Call models satisfying these constraints standard.

We show that there are standard models in which every member of P is true (i.e., mapped to 1). In fact, we show something slightly stronger: Let L be a language based on a choice of constants including $P_t$, for all types t, and $L_0$ the sublanguage obtained by omitting the constants $P_t$. We show that any standard model for a language $L_0$ can be extended to a model of L which verifies the members of P.

So let $M_0$ be a standard model of $L_0$. We specify the interpretation of $P_t$ in a sequence of steps corresponding to the complexity of t. Inductively define the rank of a type t, written r(t), as follows:

• $r(i)=r(s)=0$

• $r(t_1\rightarrow t_2)=\mathrm {max}(r(t_1),r(t_2))+1$

Let $L_n$ be the extension of $L_0$ by the constants $P_t$ with $r(t)<n$; thus $L_{n+1}$ extends $L_n$ by the constants $P_t$ with $r(t)=n$. Based on $M_0$, we define a sequence of models $M_n$ of $L_n$ by induction on the natural numbers, writing $I_n$ for the interpretation function of $M_n$. Let $I_{n+1}$ agree with $I_n$ on all constants in $L_n$. For the remaining constants, i.e., for any $P_t$ with $r(t)=n$, let $I_{n+1}(P_t)$ be some function in the domain of $\langle i,t\rangle$ such that for all constants c of type t and complex expressions $\varepsilon \eta$ with $\tau _{\varepsilon \eta }=t$:

• $I_{n+1}(P_t)(c)=I_n(c)$

• $I_{n+1}(P_t)(\varepsilon \eta )(x)(y)={\left\{ \begin{array}{ll} 1 &{} \text {if } x=I_n(P_{\tau _\varepsilon })(\varepsilon ) \text { and } y=I_n(P_{\tau _\eta })(\eta ) \\ 0 &{} \text {otherwise} \end{array}\right. }$

  for all x in the domain of type $\tau _\varepsilon$ and y in the domain of type $\tau _\eta$

Note that $I_n$ is defined on the required constants in these definitions: For the first equation, consider $c=P_{t'}$. Then $t=i\rightarrow t'$, so $r(t')=r(t)-1$. Thus $I_n=I_{r(t')+1}$ is defined on $P_{t'}=c$. For the second equation, $r(\tau _\varepsilon ),r(\tau _\eta )<r(\tau _{\varepsilon \eta })=n$, so $I_n$ is defined on $P_{\tau _\varepsilon }$ and $P_{\tau _\eta }$.

Finally, let M be the model of L extending $M_0$ whose interpretation function I maps each constant $P_t$ to $I_{r(t)+1}(P_t)$. By construction, $I_n(P_t)$ is the same function for all $n>r(t)$. Thus the two equations just used to define $I_{n+1}$ hold when both $I_{n+1}$ and $I_n$ are replaced by I, from which it follows that M verifies P.