Regularity versus Induction

regularity_vs_induction.md

Text used in this video:

https://youtu.be/7HKnOOvssvs

==== Recall the regularity statement ==== $\forall s.\Big(s\neq{},\to,\exists(x\in s). x\cap s={}\Big)$

==== Logical definitions and theorems ==== === Definitions ===

$A(a)$ ... $a\in A$

$\forall(x\in A). B(x)$ ... $\forall x. A(x) \to B(x)$

$\exists(x\in A). B(x)$ ... $\exists x. A(x) \land B(x)$

$\forall(z < y).P(z)$ ... $\forall z.\big((z < y)\to P(z)\big)$

(used above)

$x\in {\mathbb U}$ ... $x=x$

${\mathrm{refl}}(x)$ ... $x=x$

${\mathbb U}$ ... ${x\mid x=x}$

$\top$ ... $\forall x. x=x$

$x\in {}$ ... $x\neq x$

${}$ ... ${x\mid x\neq x}$

$y\in(x\cap\Sigma)$ ... $y\in x\land y\in\Sigma$

A minimal $x$ for a relation $R$ is one for which there does not exist another $y$ with $R(y, x)$.

As relation, the membership relation restricted to a class $\Sigma$ will be considered,

i.e. a minimal element with respect to $\Sigma$ is one without a $y\in(x\cap \Sigma)$.

$\big(P\to(D\land\neg D)\big)\to\neg P$

(Consider $D=\neg E$)

$\big(P\to(\neg E\land\neg\neg E)\big)\to\neg P$

=== Identities and theorem ===

Identities:

$\forall z. z\in {\mathbb U}$

$\neg \exists z. z\in {}$

$\forall z. \neg(z\in {})$

Big guy for you:

$\forall(x\in X).\Big(A(x)\to\big(B(x)\to C\big)\Big),\leftrightarrow,\Big(\Big(\exists(x\in X).\big(A(x)\land B(x)\big)\Big)\to C\Big)$

The case $C=\bot$ is without content, so consider the Separation statement equivalence:

$\forall x.\big(A(x)\to \neg B(x)\big),\leftrightarrow,\neg \exists x.\big(A(x)\land B(x)\big)$

$\forall x.\neg B(x)\leftrightarrow\neg\exists x.B(x)$

If-clauses:

$\big(A\to\big(B\to C)\big),\leftrightarrow,\big((A\lor B)\to C\big)$

Currying:

$((A\to C)\land (A\to C)),\leftrightarrow,\big((A\land B)\to C\big)$

Furthermore:

$(A\to\neg B)\leftrightarrow\neg(A\land B)$

$(A\to \neg B)\to(B\to\neg A)$

$(B\lor\neg A)\to(A\to B)$

Contrapositive:

$(A\to B)\to(\neg B\to\neg A)$

(When discussing classical statements we're gonna use $\leftrightarrow$ for all of those,

as well as freely swapping propositional variables $B$ and $\neg B$ in a formula)

For fixed $c$,

$\big(\forall x.(x=c\to P(x,c))\big)\to P(c,c)$

=== Von Neumann model defintiions ===

$0_\omega$ ... ${}$

$n_\omega:={k\mid k < n}$

$S_\omega x$ ... $x\cup {x}$

(we're going to also just write $0$ and $S$, but don't confuseit with the zero in ${\mathsf{PA}}$)

Relatedly:

Transitive set $x$ ... $(z\in x)\to(z\subseteq x)$

The relation $<$ is modeled by just $\in$.

Ordinal set ... transitive sets of transitive sets.

$y\in x$ models the order relation $y < x$ for ordinals in general.

Order is classically trichotomous and total. Nice induction step formulation via $S_\omega$.

==== HA Recap ====

Induction: $\forall n.\Big(Q(0)\land \forall n.\big(Q(n)\to Q(Sn)\big)\Big),\to,\forall m.Q(m)$

Complete Induction:

$\forall n. \Big(\big(\forall (k < n). Q(k))\big),\to,Q(n)\Big),\to,\forall m.Q(m)$

$R(k,n)$ ... $k < n$

$\forall n. \Big(\big(\forall k.(R(k,n)\to Q(k))\big),\to,Q(n)\Big),\to,\forall m.Q(m)$

Its contrapositive:

$\neg\forall m.Q(m),\to,\neg\forall n. \Big(\big(\forall k.(R(k,n)\to Q(k))\big),\to,Q(n)\Big)$

$Q$ ... $\neg T$

$\neg\forall m.\neg T(m),\to,\neg\forall n. \Big(\big(\forall k.R(k,n)\to\neg T(k)\big),\to,\neg T(n)\Big)$

Equivalent:

$\big(\neg\neg\exists m.T(m)\big),\to,\neg\neg\exists n.\Big(\big(\forall k.R(k,n)\to\neg T(k)\big),\land T(n)\Big)$

Weaker form $M$:

$\big(\exists m.T(m)\big),\to,\neg\neg\exists n.\Big(\big(\forall k.R(k,n)\to\neg T(k)\big),\land T(n)\Big)$

=== c < c ===

Fix a $c$

$T_c(k)$ ... $k=c$

$T_c(c)$ holds

$\Big(R(c,c)\land\exists n.\Big(\big(\forall k.(R(k,n)\to\neg T_c(k))\big),\land T_c(n)\Big)\Big)\to\bot$

$M\to\neg\exists c.R(c,c)$

=== c < c, again===

Directly from complete induction

$\forall n. \Big(\big(\forall k.(R(k,n)\to k\neq c)\big),\to,n\neq c\Big),\to,\forall m. m\neq c$

$\neg\neg R(c,c),\to,\neg\exists m. m= c$

==== A theorem for latter comparison ====

${\mathsf{PA}}\vdash$ Every $n$ is either zero or has a computable unique predecessor $p$ with $n = Sp$.

$Q_\mathrm{-1}(n)$ ... $n = 0,\lor,\exists p.\big(Sp = n\land Q(p)\big)$.

$(Q_\mathrm{-1}(0),\to, Q(0)),\leftrightarrow,Q(0)$.

$Q_\mathrm{-1}(Sn),\leftrightarrow, Q(n)$

(i.e. $Q_\mathrm{-1}(n)$ expresses $Q(n-1)$)

So

$\forall n. \big(Q_\mathrm{-1}(n) ,\to, Q(n)\big),\to,\forall m. Q(m)$

==== Classical equivalents ====

$\exists n. \big(\big(\forall k.(R(k,n)\to Q(k))\big),\land,\neg Q(n)\big),\lor,\forall m. Q(m)$

For any predicate $Q$, either there is some natural number $n$ for which $Q$ does not hold,

despite $Q$ holding for all predecessors, or $Q$ hold for all numbers.

Instead of $\forall(R(k,n)\to Q(k)$, one may also use $Q_\mathrm{-1}(n)$ and obtain a related statement.

It constrains the task of ruling out counter-examples for a property of natural numbers:

If the bottom case $Q(0)$ is validated and one can prove, for any number $n$,

that the property $Q$ is always passed on to $Sn$, then this already rules out a failure case.

(And via the least number principle: If a failure case exists, there there is a ''minimal'' such failure case.)

Compare with:

$\exists n.\neg Q(n),\lor,\forall m. Q(m)$

==== Set-induction ====

$\forall x. \Big(\big(\forall (y \in x). \psi(y)\big),\to,\psi(x)\Big),\to,\forall z. \psi(z)$

Also here $\forall(y\in 0).\psi(y)$, in a proof using this, $\psi({})$ must be established.

=== Rewrites ===

$\Psi$ ... ${x\mid \psi(x)}$

$\forall (x\subseteq \Psi). x\in \Psi,\leftrightarrow,\Psi={\mathbb U}$

(Note: Sleight abuse of notation, given we mix formal "$=$" and class notation.)

Note: A set is also a subset of itself.

Compare: $\Sigma$ is $\in$-transitive means

$\forall (x\in \Sigma). x\subseteq\Sigma$

==== Transfinite induction ==== Let $\psi(x)$ be

$(x\in\Sigma)\to P(x)$

for some class (and so predicate, i.e. for two predicates)

$\forall (x\in\Sigma). \Big(\big(\forall (y \in (x\cap\Sigma)). P(y)\big),\to,P(x)\Big),\to,\forall (z\in\Sigma).P(z)$

Note: For transitive classes

$\forall(x\in\Sigma).\big((x\cap\Sigma)=x\big)$

so with set induction induction holds in side those.

$\implies$ transfinite induction for ordinals

(Sidenote: Also proves that all sets have ordinal rank and the rank of an ordinal is itself)

==== Induction for well-founded relations ====

Roughly, just generalize $y\in x$ to $R_D(y, x)$ for a relation on a domain $D$.

Induction condition expression then reads $R_D(y, x)\land y\in D$.

(Proves no infinite descending $R_D$-sequences, similar to below for sets. So there $\forall y.\neg R_D(y, y)$.)

Classically, well-foundedness can be characterize as

$\bullet$ minimal element existence for every subset (strong claim)

$\bullet$ (with dependent choice) non-existence of infinite descending chains (relatively weak)

==== Negated predicates ====

Let $\psi(x)$ ... $\neg S(x)$

Let $\Sigma$ .. ${x\mid S(x)}$ by $\Sigma$

($P(x)$ above as $x\neq x$.)

So

$\forall(x\in\Sigma).x\cap \Sigma\neq{},\to,\Sigma={}$

So

$\neg\exists(x\in\Sigma). x\cap \Sigma={},\to,\Sigma={}$

I.e. a property such that there is no $\in$-minimal set for it is simply false for all sets.

==== Self-membership? ====

Consider $s$ with $\forall x. (x\in s\leftrightarrow x=s)$

Consider $S(x)$ ... $x=s$

Then

$s\in s$

$\forall (x\in s). s\in x$.

So

$s\cap x={}$ simplifies to $s\notin x$

Then the above plus our regularity expression implies $s={}$, a contradiction.

So, when set induction holds, $\neg\exists s.s={s}$.

So $\forall z.z\neq s$, i.e. $\Psi={\mathbb U}$.

In a theory with set induction, a $s$ with the described recursive property is not actually a set in the first place.

==== Infinite descending chains ====

Stronger assumption for the principle:

$A:=\forall\exists$-statement $\forall(x\in\Sigma). \exists (y\in\Sigma). y\in x$.

https://en.wikipedia.org/wiki/Axiom_of_dependent_choice

Assuming $\Sigma$ is an inhabited set together with dependent choice implies the existence of an infinite descending membership chain.

Assume dependent Choice and $A$. Non-existence of a chain means $\Sigma$ couldn't have been inhabited, i.e. $\Sigma={}$.

==== Contrapositive ====

$\neg \forall z.P(z),\to,\neg\forall x.\Big(\big(\forall (y \in x). P(y)\big),\to, P(x)\Big)$

And

$\Sigma\neq {},\to,\neg\neg\exists(x\in\Sigma). x\cap \Sigma={}$ Of course, the principle still holds (weaker form) when assuming $\exists z.(z\in \Sigma)$ instead of $\Sigma\neq {}$.

And of course classically remove the "$\neg\neg$".

In terms of classes, this states that every non-empty class $\Sigma$ has a member $x$ that is disjoint from it.

If $\Sigma$ is a set, this is the instance of the axiom of regularity for $\Sigma$.

Previous video:

In a context with an axiom of separation, regularity also implies LEM.

Set induction schema does not. (And so e.g. part of CZF.)

CZF+Regularity+Full separation => ZF

==== Classical equivalents ====

$\exists x. \Big(\big(\forall(y\in x). P(y)\big),\land,\neg P(x)\Big),\lor,\forall z. P(z)$

Expresses that, for any predicate $P$, either there is some set $x$ for which $P$ does not hold while $P$ being true for all

elements of $x$,

or the predicate $P$ holds for all sets.

Relating it back to the original formulation:

If one can, for any set $x$, prove that $\forall(y\in x).P(y)$ implies $P(x)$,

which includes a proof of the bottom case $P({})$, then the failure case is ruled out and,

then, by the disjunctive syllogism the disjunct $\forall z. P(z)$ holds.

Compare with:

$\exists x.\neg P(x),\lor,\forall z. P(z)$

==== Set induction from regularity and transitive sets ====

Again, regularity

$\Sigma\neq {},\to,\exists(x\in\Sigma). x\cap \Sigma={}$

Given a class $\Sigma$ and any transitive set $t$, define $s=t\cap\Sigma$

Note:

$\bullet$ $x\in s\to (x\in\Sigma\land x\subseteq t)$

$\bullet$ $(x\subseteq t)\to (x\cap s = x\cap \Sigma)$

which we'll use to rewrite the regularity statement.

Proof regularity for classes (i.e. set induction) from regularity from sets:

Assume there exists $z\in\Sigma$ and $z$ is the subset of a transitive set.**

Construct $s_z$ as above. Note $(z\cap\Sigma)\subseteq s_z$. Consider LEM for $s_z={}$:

$\bullet$ $s_z={}$: Then $x=z$ (the set) fulfills regularity.

(Note: If the transitive set is the transitive closure, this case is redundant.)

$\bullet$ $s_z\neq{}$: Then regularity (for the set $s_z$ not $\Sigma$) implies $\exists(x\in s_z)$

and we can use the above manipulation (Here we in fact learn $x\in s_z$ and not just $x\in\Sigma$)

QED.

**Note: Transitive set existence actually requires a lot of axioms (except powerset). The unpacking works with replacement on $\omega$.