It seems to me that there is a difference in the treatment of "partial" elements in boolean-valued models in set theory vs topos theory: in set theory, one usually only considers "global" elements of boolean-valued models, but in topos theory one also considers "partial" elements. Peter Lumsdaine remarks here that the cumulative hierarchy constructed inside a topos is flabby, and apparently this is why there is no loss of generality in ignoring "partial" elements in boolean-valued models of set theory. This is very plausible to me, but I am not sure I really understand what is going on. I also would like to know if this is something special about boolean-valued models of set theory.
Let me define terms.
Fix a complete Heyting algebra $A$. An $A$-valued partial equivalence relation (PER) on a set $X$ is a map $e : X \times X \to A$ satisfying the following conditions:
- For all pairs $(x_0, x_1)$ of elements of $X$, $e (x_0, x_1) = e (x_1, x_0)$.
- For all triples $(x_0, x_1, x_2)$ of elements of $X$, $e (x_0, x_1) \land e (x_1, x_2) \le e (x_0, x_2)$.
Note that it follows that $e (x_0, x_1) \le e (x_0, x_0) \land e (x_1, x_1)$. We should think of $e (x, x)$ as being the "extent" to which $x$ is "defined"; a "global" element is $x$ such that $e (x, x) = \top$.
Given such $(X, e)$, say $X$ has restriction with respect to $e$ if the following condition is satisfied:
- For all $x \in X$ and $a \in A$, if $a \le e (x, x)$, then there is some $x' \in X$ such that $a = e (x', x')$ and $e (x', x') \le e (x', x)$.
Say $X$ has amalgamation with respect to $e$ if the following condition is satisfied:
- For all subsets $X' \subseteq X$, if for every pair $(x_0, x_1)$ of elements of $X'$ we have $e (x_0, x_0) \land e (x_1, x_1) \le e (x_0, x_1)$, then there is some $x \in X$ such that $\bigvee_{x' \in X'} e (x', x') \le e (x, x)$ and, for all $x' \in X'$, $e(x', x') \le e (x', x)$.
Say $X$ is flabby with respect to $e$ if the following condition is satisfied:
- For all $x \in X$ and $a \in A$, if $e (x, x) \le a$, then there is some $x' \in X$ such that $a = e (x', x')$ and $e (x, x) \le e (x, x')$.
Now fix a first-order signature $\Sigma$. I will assume that $\Sigma$ is one-sorted and has no function symbols, but I hope it is clear how everything can be done for general first-order signatures. An $A$-valued $\Sigma$-structure $M$ consists of the following data:
- A set $\left| M \right|$.
- An $A$-valued PER on $\left| M \right|$, which we will write infix as $=_M$.
- For each $n$-ary relation symbol $\phi$, a map $\phi_M : \left| M \right|^n \to A$ satisfying the following conditions:
- For all $n$-tuples $(x_0, \ldots, x_{n-1})$ of elements of $\left| M \right|$, $$\phi_M (x_0, \ldots, x_{n-1}) \le (x_0 =_M x_0) \land \cdots \land (x_{n-1} =_M x_{n-1})$$
- For all pairs of $n$-tuples $((x_{0, 0}, \ldots, x_{0, n-1}), (x_{1, 0}, \ldots, x_{1, n-1}))$ of elements of $\left| M \right|$, $$(x_{0, 0} =_M x_{1, 0}) \land \cdots \land (x_{0, n-1} =_M x_{1, n-1}) \land \phi_M (x_{0, 0}, \ldots, x_{0, n-1}) \le \phi_M (x_{1, 0}, \ldots, x_{1, n-1})$$
Given such an $M$, we can interpret any first-order logical formula in $A$. More precisely, a formula-in-context with $n$ free variables is interpreted as a map $\left| M \right|^n \to A$. The interpretation is defined inductively. I omit the details of how to interpret the basic relations and connectives, except to note that logical consistency dictates that $$\psi_M (x_0, \ldots, x_{n-1}) \le (x_0 =_M x_0) \land \cdots \land (x_{n-1} =_M x_{n-1})$$ for all formulae-in-context $\psi$ with $n$ free variables, so we do have to be a bit careful. (I think $\Rightarrow$ is the only connective where the "obvious definition" falls foul of this rule.) Quantifiers are handled as follows:
Given the interpretation $\psi_M : \left| M \right|^{n+1} \to A$ of a formula-in-context $\psi$ with $n + 1$ free variables, the interpretation of $\exists y . \psi$ is the map $(\exists y . \psi)_M : \left| M \right|^n \to A$ defined by $$(\exists y . \psi)_M (\vec{x}, \vec{z}) = \bigvee_{y \in \left| M \right|} \psi_M (\vec{x}, y, \vec{z})$$
Given the interpretation $\psi_M : \left| M \right|^{n+1} \to A$ of a formula-in-context $\psi$ with $n + 1$ free variables, the interpretation of $\forall y . \psi$ is the map $(\forall y . \psi)_M : \left| M \right|^n \to A$ defined by $$(\forall y . \psi)_M (\vec{x}, \vec{z}) = (\vec{x} =_M \vec{x}) \land (\vec{z} =_M \vec{z}) \land \bigwedge_{y \in \left| M \right|} ((y =_M y) \Rightarrow \psi_M (\vec{x}, y, \vec{z}))$$
(Incidentally, this is the only place where we use the hypothesis that $A$ is complete, and upon closer inspection we see that less will suffice.)
There is an obvious notion of substructure of $M$. Given a substructure $M'$, say $M'$ is an elementary substructure of $M$ if it has the following property:
- For every formula-in-context $\psi$ with $n$ free variables and every $n$-tuple $(x_0, \ldots, x_{n-1})$ of elements of $\left| M' \right|$, $$\psi_{M'} (x_0, \ldots, x_{n-1}) = \psi_M (x_0, \ldots, x_{n-1})$$
Question 1. Is every $A$-valued $\Sigma$-structure isomorphic to an elementary substructure $M'$ of some $M$ where $\left| M \right|$ has restriction and amalgamation with respect to $=_M$, and where every element of $\left| M \right|$ can be obtained by (iterated) restriction and amalgamation of elements of $\left| M' \right|$?
(In other words, given a structure that is missing some "partial" elements, is it logically harmless to add them in?)
Given $M$, let $M'$ be the substructure where $$\left| M' \right| = \left\{ x \in \left| M \right| : (x =_M x) = \top \right\}$$ It is straightforward to find an example where $M'$ is not an elementary substructure of $M$: just arrange for $\left| M' \right|$ to be empty while $\left| M \right|$ has an element $x$ such that $x =_M x$ is not $\bot$; then the interpretations of $\exists x . x = x$ will differ. This can happen even if $\left| M \right|$ has restriction and amalgamation with respect to $=_M$.
Now suppose $\Sigma$ is the signature of set theory and $M$ is a model of set theory (such as, but not limited to, ZF).
Question 2. Assuming $\left| M \right|$ has restriction and amalgamation with respect to $=_M$, is $\left| M \right|$ flabby with respect to $=_M$?
Question 3. Assuming $\left| M \right|$ is flabby with respect to $=_M$, is $M'$ an elementary substructure of $M$?
(In other words, is it logically harmless to ignore "partial" elements?)
