You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
CZF's characterization of the von Neumann "hierarchy"
In this video we analyze how much we get without LEM or the Powerset axiom.
(But with function spaces and the very set theoretical Replacement.)
That context has semnatics where all sets are in the surjective image of a subset of ${\mathbb N}$.
(Subcountability, see also subquotients.)
Powerset axiom:
$\forall B. \exists C. \forall S. \big(S\in C\leftrightarrow S\subset B\big)$
(Tead $C={\mathcal P}(B)$)
That axiom uses unbounded quantififcation.
Particularly iffy may be considered the one over $S$.
Pre-Warmup: Correspondence between predicates and subsets via Separation
Given some $B$, say $B={\mathbb N}$
Further given some $A\subset B$.
Then $A = B\cap A = {n \in B \mid n\in A}$
Write $P_A(n) := n\in A$, then
$A = {n \in B \mid P_A(n)}$
Now, given first some predicate $Q(n) = \dots$
e.g. some polynomial zero, or true on naturals $n$ that don't end up at $1$ in Collatz, etc.
$A_Q := {n \in B\mid Q(n)}$
Meditation: Ponder the powerset axiom in light of the breadth of all the predicates out there.
$\Omega_2 := 2 = {0,1}$ amounts to the $\mathrm{Bool}$ data type and functions as th set of classical truth values.
Exponentiation axiom: If $A$ and $Y$ are a set, then $Y^A$ is a set.
Here we need that $(\Omega_2)^A$ is a set, the function space of characteristic function
Set of detachable sets exist
Consider $U\subseteq A$ which is detachable, i.e.
$\forall (a\in A). \big(a\in U \lor a\notin U\big)$
Then there's a characteristic function $\chi_U\in (\Omega_2)^A$, and so $\chi_U\subset A\times \Omega_2$, with
$a\in U\iff \chi_U(a) = 1$.
Consider now $\rho \in (\Omega_2)^A$.
This characterizes a class $U_\rho$ via $a\in U_\rho\iff \rho(a) = 1$.
$U_\rho$ is a set by bounded the Separation axiom:
$U_\rho := {a \in A \mid \rho(a) = 1 }$
Consider the pairings $\langle \rho, U_\rho\rangle$, which has left entries that are members of $(\Omega_2)^A$.
Now
${\mathcal P}{\Omega_2}A := { u \mid \exists \big(\rho\in (\Omega_2)^A\big). U\rho = u }$
is a set, via the Replacement axiom.
It contains exactly the detachable subsets of $A$.
In other terms, for $\rho\in\Omega^A$ with $\Omega = \Omega_2 = {0,1}$,
${\mathcal P}_{\Omega}A = im(\wp)$, where $\wp(\rho) := {a \in A \mid \rho(a) = 1}$.
With LEM, all sets are detachable and so have a characteristic function,
and so since ${0, 1}\subseteq {\Omega_2}$ (indeed it's equal) we have that ${\mathcal P}_{\Omega_2}A$ is the powerset, generally just written ${\mathcal P}A$.
Somewhat informally written, ${\mathcal P}A = {S\subseteq A \mid \top}$. We'll generalize away from $\top$.
Class of truth values
Observe:
$t\in \Omega_2\leftrightarrow (t=0 \lor t=1)$
which implies
$t\in \Omega_2. \forall x\in t. x\in 1$
which is the definition of
$t\in \Omega_2\to t\subseteq 1$
A truth value is defined to be a subset of of $1$.
If $t$ is a truth value, then by Extensionality $(0 \in t) \leftrightarrow (t = 1)$.
(We'll use the (arguably more intricate looking) equality notation,
just because its more natural when talking of characteristic functions)
The ordinals are defined to be the transitive sets of transitive sets.
A truth value is an ordinal. And indeed, classically those are just the two ordinals $0$ and $1$.
Bummer: Constructively, in general, ordinals aren't linearly ordered.
More generic sets of truth values
$\forall t\in T. t\subseteq 1$
which is to say,
$\forall t\in T. \forall x\in t. x\in 1$
Give a set $Y$, we can isolate the truth value set it contains as $Y_{\subset 1}:={a\in Y\mid a\subset 1}$
The class of all truth values doesn't provably exists in $\mathsf{CZF}$.
We might write it as
${\mathcal P}1 = {t \mid t\subset 1}$,
or $V_{\subset 1}$.
The subset induces the partial order of a [[Heyting algebra]].
If $R$ is some bounded predicate (or even a collection thereof), say $R(x,y) := (x=y)$ with $x,y\in B$,
we get various derived sets of truth values such as, here, ${[![ x=y ]!] \mid x,y\in B}$
Truth value reification
$P$ ... an unary predicate
$Q$ ... a proposition, e.g. $Q = P(a)$ when $a$ is some fixed term.
Define
$[![ Q ]!] := {x\in 1\mid Q}$
This has
$[![ Q ]!]\subseteq 1$
$Q \leftrightarrow [![ Q ]!] = 1$
$\neg Q \leftrightarrow [![ Q ]!] = 0$
Interesting example:
If ${\mathsf T}$ denotes our theory, then
$[![ {\mathrm{Con}}({\mathsf T}) ]!] := {x\in 1\mid {\mathrm{Con}}({\mathsf T})}$
and if ${\mathsf T}$ is sound and consistent, it proves neither
$[![ {\mathrm{Con}}({\mathsf T}) ]!]=0$
nor
$[![ {\mathrm{Con}}({\mathsf T}) ]!]=1$.
Let, from now on, $\Omega = 2\cup T$.
Consider the statement
$\forall a\in A. [![ P(a) ]!]\in \Omega$
... read: On $A$, the predicate $P$ has classical-or-$T$-small truth values
Think of $T$ as a set of undecided truth values you still consider fair game.
Note that
$(Q\lor \neg Q) \to [![ Q ]!] \in \Omega$
So classically, the above $\forall a\in A$-statement always holds, no matter the $T$.
When $T=\emptyset$, we're back in the previous situation $\Omega=\Omega_2$. Here, this implication is an equivalence.
Generalizing ${\mathcal P}_2$
For a predicate, use now "$a\in X$".
Preamble:
${a \in A \mid [![ a\in X ]!] = 1} = A\cap X$
$(X\subseteq A) \leftrightarrow (A\cap X = X)$
So for our situation of interest $X\subseteq A$, this really a new way to write all of $X$ itself.
Assuming just
$\forall a\in A. [![ a\in X ]!]\in \Omega$,
we got that $a\mapsto [![ a\in X ]!]$ is a total map into $\Omega$,
which acts akin to a characteristic function for membership in $X$ on $A$,
but now generalized to live in $A\to \Omega$ with $T$ not necessarily empty.
Now step throught the Exponentiation-Separation-Replacement construction from the beginning again,
obtaining ${\mathcal P}_\Omega A$ as an image of $\wp(\rho) := {a \in A \mid \rho(a) = 1}$.
... read: The collection of those subsets $X$ of $A$ whos membership (w.r.t. $A$) is decidable-or-$T$-like.
Our power operation then also validates (class notation),
${\mathcal P}_\Omega A = {X\subseteq A\quad \mid \quad \forall a\in A. [![ a\in X ]!]\in \Omega}$
(This is arguably more neat, but note that ${X\subseteq A \mid Q(A, X, T)}$ is still syntactic sugar,
not amenable to plain subset separation.)
When $T=\emptyset$, then $\Omega = {0, 1} = \Omega_2$, which is the strictest we can sensibly be.
In that case we collect merely the subset with decidable membership, as in the previous section.
Again, classically $[![ Q ]!] \in \Omega$ always, and so there ${\mathcal P}_\Omega A = {\mathcal P} A$.
I don't know of a reason to consider $\Omega$ without $2\subseteq\Omega$
One is, in any case, only interested in $\Omega$ which holds only truth values. In that case,
For non-empty $A$, these are really equivalences.
The statement we're really interested here is that $A \in {\mathcal P}_\Omega A$,
as this means we can form sizable chains of sets with ever higher rank.
We might actually really wanna use $A \cup {\mathcal P}_\Omega A$.
(That's however not necessary in the definition below, where $\bigcup$ are used on top of it all.)
Intermezzo on limitations of the constructive theory
I'm not good with ordinal analysis - the following are some pointers to geta feel for how far CZF takes you - confirm in the literature for yourself!
There's models of $\mathsf{CZF}$ where the class $\omega_1$ (classically, all countable ordinals) is not a set.
$\mathsf{CZF}$ proves availablility of recursive ordinal notation system for some of its mid-sized countable ordinal sets.
At and beyond this, some well-foundedness provability by $\mathsf{CZF}$, and the corresponding induction, is lacking.
Namely one that's larger than $\varepsilon_0$ but smaller than some stronger subsystem of classical second-order arithmetic.
(That's the Bachmann–Howard ordinal. Surely at least below it, $\mathsf{CZF}$-provably all ordinals are also sets.)
In particular, that structure's existence of ordinals below, say, $(\omega^\omega)^\omega$ is fine.
In particular, $\omega\cdot n$ is defined as in the classical case.
$H_{\aleph_1}$ is not provably a set, albeit stating this needs some work...
Consider the functions the domain of which is $\omega$ or some $n\in\omega$.
These are sequences and their ranges are counted sets.
Denote by $C$ the class characterized as the smallest codomain
such that the ranges of the aforementioned functions into $C$ are also itself members of $C$.
${\mathsf {CZF}}$ does not prove that $C$ would constitutes a set, even when countable choice is assumed.
In ${\mathsf {ZF}}$, this is the set$H_{\aleph_1}$ but also various things about it are independent.
The set is uncountable, as it also contains all countable ordinals,
And it has ordinal rank at most $\omega_2$, but its cardinality is not necessarily that of ${\mathbb R}$.
The classical cummulative Neumann hierarchy uses expression like
$V_0=0,\quad V_{\beta+1}:={\mathcal P} V_{\beta}, \quad V_\lambda := \bigcup_{\beta \in \lambda} V_\beta$
Where $\beta \in \lambda$ gives a predecessor relation - and here is read $\beta < \lambda$.
Note that
$V_\lambda := \bigcup_{\beta \in \lambda} {\mathcal P} V_\beta$
For the powerset operation, use now the more constructive, more bottom alternative of mapping $A$ to
${\mathcal P}{\Omega{(2,\cup,A_{\subset 1})}}$
and use (eventually, see Ziegler links below) all ordinals (of ranks of all sets) as index sets.
But constructively the class of ordinals don't all form a linear chain along one does recursion.
So this setup thus involves "stray ordinals" (my term) and then the sets of the whole "hierarchy"
constructively doesn't form a monotone, ever more encompassing chain.
Still, we got Set induction (classically equivalent to Foundation/Regularity) and a bunch of nice theorems. E.g.,
Having obtained ${\hat V}_\beta$ by applying a power-operation to some set, the latter set is also a member of the former
$\beta \in \lambda\to \big({\hat V}\beta\in {\hat V}\lambda\land {\hat V}\beta\subset {\hat V}\lambda\big)$,
so locally it's like the hierarchy, still.
Each set $x$ has an ordinal $\alpha_x$ that functions as an index for a ${\hat V}_{\alpha_x}$ that contains $x$.
We can still recursively define a set which e.g. classically equals $V_{\omega^n}$. Although only $\Omega_2$ provably is a subset of this.
The theorems $V_0 = 0, V_1 = 1$, i.e. the fixed points results $\forall t\in \Omega_2. V_t = t$, generalizes
i.e. all (general) truth values are fixed points also of our constructive variant.
And for nice sets such as ${\hat V}\omega$, which is indexed by the set $\omega$,
these $V$'s are the same no matter the approach.
(In the case of $V\omega$, it's the herditarily finite sets.)
"Hierarchies of Sets in Classical and Constructive
Set Theories"
But $L$ isn't as pretty: There's an $L$ definition but it fails to have all
function spaces as members, and so doesn't validate the Exponentiation axiom.
Related, recent text: Equiconsistency of $\mathsf{CZF}$ with $\mathsf{CZF}+V=L$
