Saturday, 18 August 2012

A Conservation Theorem for Mereology

Hartry Field, in his Science without Numbers (1980), introduced and developed a fictionalist programme for mathematical nominalism based on two major ideas:
1. An Elimination/Nominalization Result:
For certain kinds of mathematicized theories $T$ in science, the quantification over mathematical entities (numbers, real numbers, values of quantities, etc.) can be eliminated by "encoding" mixed relations (between concreta and mathematicalia, such as "$r$ is the mass-in-kg of $x$" or "$r$ is the value of scalar field $\phi$ at spacetime point $p$") and pure relations (amongst mathematicalia, such as "$r_1 = r_2 \times r_3$") into the purely concrete domain.

2. A Conservative Extension Result:
Given a theory $T$ entirely about concreta (a "nominalistic theory), the result of extending $T$ with axioms for sets yields a conservative extension when restricted to what one can prove about the concreta.
There is an important similarity between Field's programme and Hilbert's programme: for Hilbert, only finite mathematical entities (natural numbers, finite sets, finite graphs, etc.) are considered "real", while infinite sets are to be considered "useful fictions". Ideally, one would have shown that extending, say, $\mathsf{PA}$ with axioms for sets would give a conservative extension. However, of course, Gödel's results showed that this cannot hold in general. Gödel himself notes this in the famous foonote 48a of his 1931 paper. For example, extending $\mathsf{PA}$ with impredicative comprehension yields a theory that is arithmetically much stronger.

One might try and develop an analogous fictionalism for other kinds of entity that are sometimes considered metaphysically dubious (e.g., theoretical objects, possible worlds). One kind of fishy metaphysical entity is a mereological fusion. One might think that for any $a$ and $b$, there is always a fusion $a + b$. Or one might reject this in all cases. The analogous question then is: does extending a theory with axioms for mereological fusions make no difference? Does it yield a conservative extension? The answer to this is, "yes", under certain circumstances.

In a draft article, "What Difference Does it Make?", I sketch a conservation result for mereology. The basic idea is to begin with a theory $T$, which is then extended by a version of mereology I call Fusion theory, $\mathsf{F}$ (equivalent to Classical Mereology: the difference is that binary fusion, $x + y$, is treated as primitive). If the original entities are treated as atoms of the resulting combination (this is achieved by relativization of quantifiers to the predicate $At(x)$), $T^{At} \cup \mathsf{F}$, then anything provable in the extended theory about the original entities is provable in the original theory $T$.

The method is model-theoretic, and is analogous to Field's approach in his 1980. Take a structure $M$ for the original language $L$, with domain $X$, say. We try to construct a larger structure $M^{\ast}$ for the extended language, with the right properties. Let the larger domain be simply $X^{\ast} = \mathcal{P}(X) \setminus \{\varnothing\}$, so that we shall get a power set algebra (a complete lattice) with the least element removed. Then map the original elements $a \in X$ to their singletons $\{a\} \in X^{\ast}$. So, let $s(a) = \{a\}$. Finally, we define a structure $M^{\ast}$ for the full language by defining, each distinguished relation $(P_i)^M$ in $M$, a corresponding relation $s[(P_i)^M]$. In the larger structure we interpret $At$ as $s[X]$; we interpret the fusion symbol $+$ as $\cup$ and interpret the parthood symbol $\preceq$ as $\subseteq$ (we interpret the overlap predicate $xOy$ in the obvious way too).

The construction guarantees that
$M^{\ast} \models \mathsf{F}$.
Also, the singleton mapping $s$ embeds $M$ into $M^{\ast} | L$, with image $s[X]$, which is the denotation of $At$. So, for any $L$-sentence $\phi$,
$M \models \phi$ iff $M^{\ast} \models \phi^{At}$
(here $\phi^{At}$ is the relativization of $\phi$ to $At$).

It follows from this that
if $T^{At} \cup \mathsf{F}$ proves $\phi^{At}$, then $T$ proves $\phi$.
For if $T$ does not prove $\phi$, then there is a model $M \models T$ with $M \not \models \phi$. But then $M^{\ast} \models T^{At}$ and $M^{\ast} \not \models \phi^{At}$. And $M^{\ast} \models \mathsf{F}$. So, $M^{\ast} \models T^{At} \cup \mathsf{F}$. So, $T^{At} \cup \mathsf{F}$ does not prove $\phi^{At}$.

1. By a similar method one proves that arithmetical comprehension $ACA_0$ (with set parameters and the second-order induction axiom instead of the first-order schema) is conservative over PA, by showing that every model of PA can be extended to a model of $ACA_0$ by taking the collection of all first-order definable sets of naturals as the second-order domain. The result is well-known, I am not sure who proved it first, and it might in fact be a folk theorem. That could well be where Field got the idea of the conservativeness proof in the first place.

2. Aldo, thanks, yes - the result for $ACA_0$ over PA goes way back, but I don't know who originally proved it. In an earlier, longer draft I included a description of this and other similar results (e.g., the restricted T-scheme extension of PA is conservative).
What I do here is also bit similar to Field's model for $T + ZFU$ - i.e., given a model M for T, treat its elements as urelements (i.e., set atoms), and define the universe V(U), keeping the original relations amongst the urelements fixed. (This argument doesn't work if schemes in T are extended to formulas containing $x \in y$.)

I think there might be a close relationship between predicative comprehension and mereology with unrestricted fusion, but I haven't been able to get it clear yet. I'm also unsure what happens when one adds the fusion theory (mereology) to PA, with full induction. It looks like the fusions of atoms (i.e., numbers) will behave just like sets of numbers, so possibly it becomes non-conservative.
I've spent a while searching for literature discussing whether mereology is conservative but can't find anything.

Cheers, Jeff