Tuesday, 12 April 2011

"There is a set of Fs" implies only logical truths

Nominalists and anti-nominalists disagree about whether there are, for example, sets of things, where the things in question may be "concrete". The sentence "there is a set of chairs" is an example of a mixed mathematical claim. It uses the (presumably) non-mathematical predicate "x is a chair" as the defining formula $\varphi(x)$ in an instance of the Comprehension Scheme:
  • $\exists y \forall x(x\in y \leftrightarrow \varphi(x))$
The sentence "there is a set of chairs" cannot be true if there are no sets. So, a nominalist will conclude that instances of comprehension are not true. Even so, the nominalist, like everyone else, will want to employ such sentences in their reasoning. How is this justified? Hartry Field (1980: Science Without Numbers) argued that the justification of the use of such (believed-to-be-untrue) sentences in reasoning involves their conservativeness. Unrestricted comprehension is, of course, inconsistent. For replacing $\varphi(x)$ with $x \notin x$ yields:
  • $\exists y \forall x(x\in y \leftrightarrow x \notin x)$
which is inconsistent. (Russell's Paradox.) However, there are restricted classes of instances of comprehension which are consistent. In particular, the class of instances of comprehension where $\varphi(x)$ contains non-mathematical vocabulary. Suppose that we call sentences containing only "concrete" predicates nom-sentences; call instances of the Comprehension Scheme using only nom-formulas comp-axioms. The simplest relevant conservativeness result says:
  • If there is a derivation of a nom-sentence $B$ from a comp-axiom, there is also a derivation of $B$ from logic.
Unfortunately, the literature on this topic is quite difficult, and there are a number of different results and a number of different kinds of proofs.

Here is the simplest proof of the simplest kind of conservativeness result which will give a flavour of why comprehension axioms are conservative. We consider the simplest scenario: the nom-language $\mathcal{L}$ is a first-order language (with identity) and has only a single unary concrete predicate $Fx$ and we consider the simplest comp-axiom, $\exists y \forall x(Rxy \leftrightarrow Fx)$, where we write $Rxy$ to mean "x is an element of y". The conservativeness result now is: for any $\mathcal{L}$-sentence $B$,
  • $ \text{If } \exists y \forall x(Rxy \leftrightarrow Fx) \vdash B \text{ then } \vdash B$.
Here is a proof which shows how to convert a derivation of $B$ from $\exists y \forall x(Rxy \leftrightarrow Fx)$ to a derivation of $B$ entirely in logic. I will assume a Hilbert-style deductive system with linear derivations, some bunch of axiom schemes and the single rule Modus Ponens.

First, note that, in general, if $\exists y \varphi(y) \vdash B$, then $\varphi(y/c) \vdash B$ (where $c$ is a new constant: it is skolem constant). So, it will be sufficient to show that we can do this given a derivation $(P_0, P_1, ..., P_n)$ of $B$ from $\forall x(Rxc \leftrightarrow Fx)$. Let $\mathcal{L}(c)$ be the result of extending $\mathcal{L}$ with the new constant $c$. The main idea of the proof is that the assumption $\forall x(Rxc \leftrightarrow Fx)$ looks just like a "definition" of $Rxc$. So, the plan is to consider each formula $P_i$ in the derivation, and replace any occurrence of $Rt_1t_2$ in $P_i$ by $Ft_1 \wedge t_2 = c$ (where $t_1, t_2$ are terms). This replacement therefore eliminates the symbol $R$ (i.e., the membership predicate). Let $(P_i)^{\circ}$ be the result of making this replacement.

From the definition of "derivation", each $P_i$ is either an axiom of logic, or is the assumption formula $\forall x(Rxc \leftrightarrow Fx)$, or is obtained by Modus Ponens on previous formulas. The hope is that, after the replacements, the new sequence of formulas $((P_0)^{\circ}, ..., (P_n)^{\circ})$ is, "more or less", a derivation of B in logic.

Since $B$ does not contain the symbol $R$, the replacement makes no difference to $B$. (I.e., $B^{\circ}$ is just $B$.) Next, if $P_i$ is a logical axiom containing $R$, then replacing $Rt_1t_2$ by $Ft_1 \wedge t_2 = c$ will give a logical axiom in $\mathcal{L}(c)$. Next, if $P_i$ is the assumption formula $\forall x(Rxc \leftrightarrow Fx)$, then replacing $Rxc$ by $Fx \wedge c = c$ yields $\forall x((Fx \wedge c = c) \leftrightarrow Fx)$. But this is itself a logically derivable $\mathcal{L}(c)$-sentence. Finally, if $P_i$ is obtained by Modus Ponens from $P_j$ and $P_k$ (with $j, k < i$), we need to check that after we've made the replacements, then result is still an instance of Modus Ponens. The only thing to check is that applying the replacement to a conditional $P_j \rightarrow P_i$ yields the conditional of applying the replacements; and this is so. (I.e., that $(P_j \rightarrow P_i)^{\circ}$ is $(P_j)^{\circ} \rightarrow (P_i)^{\circ}$.) It follows then that, assuming we "paste in" the missing derivation of $\forall x((Fx \wedge c = c) \leftrightarrow Fx)$, the replacement yields a derivation of $B$ in logic alone, in the language $\mathcal{L}(c)$. However, since $B$ does not contain $c$, if there is a logical derivation of $B$ in $\mathcal{L}(c)$, then there is a logical derivation of $B$ in $\mathcal{L}$ itself. So, $\vdash B$, as required.

This is probably the simplest case of a Field-style conservativeness result for mathematical axioms over "nominalistic" sentences. One can then build-up to more complicated cases by modifying this kind of proof. E.g., to consider comp-axioms where the defining formula is $\varphi(x)$, where $\varphi(x)$ is any $\mathcal{L}$-formula (rather just the atomic formula $Fx$). Also, to consider a nom-language $\mathcal{L}$ with various primitive predicates for concreta. In these latter cases, the comp-axioms have the form $\forall x(Rxc \leftrightarrow \varphi(x))$, where $\varphi(x)$ is an $\mathcal{L}$-formula and $c$ is a constant (a new constant is needed for each formula $\varphi(x)$). The method is, again, to replace occurrences of the atomic formula $Rt_1t_2$ as they appear in a derivation by certain $\mathcal{L}(c_1, ..., c_n)$-formulas. This will transform a given derivation using comp-axioms into a derivation in logic alone (in the language $\mathcal{L}(c_1, ..., c_n)$).

No comments:

Post a comment