🚀 go-pugleaf

In article <Bx81Ho.9HL@cantua.canterbury.ac.nz> wft@math.canterbury.ac.nz (Bill Taylor) writes:

BT:
>>>A = { 1 , { 2 , { 3 , { 4 , {.....}}}}} . Such a set seems very well defined

VP:
>>If you are comfortable with A, you should not mind
>>B = { 1 , { 1 , { 1 , { 1 , {.....}}}}} .

BT:
>Yes, I *do* mind B, for the very reason you suggest; that it is a member of
>itself. There is, I agree, not a lot of difference, on the face of it, between
>B and A.  I'm not *devoted* to A. It *does* have a slightly fishy look. 
>Even a hereditarily fishy look.  :)    That's why I put out my request.
>Let me repeat it...
>
>REQUEST: Can B above, be obtained from A above, by ZF methods.
>~~~~~~~  I don't think Replacement can achieve it, but I'm open to correction.
>Any ideas, anyone ?

Bill, Vaughan, -- look at the proof I sent you.  Better yet, here it
is.  This is some material from my set theory notes, which should work
as is in amslatex:

\begin{document}

\theoremstyle{plain}

%{\theorembodyfont{\normalshape} \newtheorem{problem}{Problem}[section]}
{\theorembodyfont{\normalshape} \newtheorem{problem}{Problem}}
%{\theorembodyfont{\normalshape} \newtheorem{theorem}{Theorem}[section]}
{\theorembodyfont{\normalshape} \newtheorem{theorem}{Theorem}}
{\theorembodyfont{\normalshape} \newtheor% sqdots.sty
% Author: R. A. Riemenschneider (rar@ads.com)

\newdimen\sqdotdim
\sqdotdim=.35ex         % Adjust this number to change the size of the dots
% Adjust this number to change the size of the dots

\def\sqdot{{}\mathop{
   \vrule width\sqdotdim height\sqdotdim depth0ex}{}}

\def\sqdots{\sqdot\llap{\raise3\sqdotdim\hbox{$\sqdot$}}}

em{lemma}[theorem]{Lemma}}
{\newtheorem{axiom}{Axiom}}
{\theorembodyfont{\normalshape} \newtheorem{remark}{Remark}}
%{\theorembodyfont{\normalshape} \newtheorem{defn}{Definition}[section]}
{\theorembodyfont{\normalshape} \newtheorem{defn}{Definition}}
%{\theorembodyfont{\normalshape} \newtheorem{prop}{Proposition}[section]}
{\theorembodyfont{\normalshape} \newtheorem{prop}{Proposition}}
{\theorembodyfont{\normalshape} \newtheorem{cor}[theorem]{Corollary}}
\newenvironment{proof}{\noindent \rm {\sc Proof:\\}}{\quad $\blacksquare$}
%\newenvironment{proof}{\noindent \rm {\sc Proof:\\}}{$\Box$ \vspace{2 ex}}
%\newenvironment{defn}{\noindent \rm {\sc Definition:\\}}{$\Box$ \vspace{2 ex}}



\def\bexists{\boldsymbol{\exists}}
\def\boldexists{\boldsymbol{\exists}}
\def\varexists#1#2{\operatornamewithlimits{(\boldsymbol\exists \hbox{$#1$})}_{#\
2}}

\def\bsupset{\boldsymbol{\supset}}
\def\boldsupset{\boldsymbol{\supset}}
\def\varsupset#1{\operatornamewithlimits{\boldsymbol\supset}_{#1}}

\def\bequiv{\boldsymbol{\equiv}}
\def\boldequiv{\boldsymbol{\equiv}}
\def\varequiv#1{\operatornamewithlimits{\boldsymbol\equiv}_{#1}}


\begin{axiom}
\label{foundation}
% Fraenkel \& Bar-Hillel, p.88
Foundation.
If $x$ is non-empty, then it contains a member which is disjoint from $x$,
i.e.~a member $y$ with no members common to $x$ and $y$:
$$\varexists{u}{}(u \in x) \varsupset{x} \varexists{y}{y \in x}
\varforall{z}{z \in x} \sqdot z \not\in y.$$
\end{axiom}

\begin{remark}
\label{inmin}
As a consequence of the Axiom~\ref{foundation}, we will obtain that if
there is some element $x$ which fulfils $\cal{P}(x)$ then there is an
$\in$-minimal element $u$ which fulfils $\cal{P}(x)$, i.e., $u$ fulfils
$\cal{P}(x)$ but none of its members fulfils $\cal{P}(x)$.  In symbols,
$$\varforall{z_1}{} \ldots \varforall{z_n}{} \sqdot \varexists{x}{} \phi(x)
\boldsupset \varexists{x}{} \sqdot \phi(x) \sqdot (y \in x \boldequiv_y \neg
\phi(y)).$$
This axiom is our second example (after the Axiom~\ref{comprehension}
(Comprehension)) of a principle that stipulates that all sets have certain
properties; all the other axioms can be interpreted as weakened instances
of the comprehension scheme embodied in Proposition~\ref{comprehension}.
\end{remark}

\begin{problem}
\label{hw1}
% homework #1
Show that there are no finite $\in$-cycles.

\begin{proof}
Assume there exists a cycle of length $n$, that is, $x_1 \in x_2 \in
\ldots \in x_n \in x_1$.  Let $y = \{ x_1, x_2, \ldots, x_n \}$, which
exists by iterated application of the Pairing and Union Axioms.  Consider
an arbitrary $x_i\in y$, $1\leq i\leq n$; then, if $i > 1$, we have that
$x_{i-1} \in x_i \cap y$; otherwise, if $i=1$, we have that $x_n\in x_i
\cap y$.  Hence the condition of Axiom~\ref{foundation} (Foundation) is
violated.

Alternatively, $y$ fails to satisfy the condition of Remark~\ref{inmin},
since there is no $\in$-minimal set which satisfies the property $(\lambda
x)\sqdot x \in y$.
\end{proof}
\end{problem}

\end{document}

Now, showing that 

A = { 1 , { 2 , { 3 , { 4 , {.....}}}}}

is *not* a set in a well-founded theory is left as an exercise for the
reader.  However, if your theory has no equivalent of the axiom of
foundation (a.k.a. regularity), then, given a suitable comprehension
schema guaranteeing the existence of A, you can obtain

B = { 1 , { 1 , { 1 , { 1 , {.....}}}}}

by Replacement with transfinite recursion.  I think.  Look at Aczel to
make sure.

BT:
>Randall Holmes - a question.  You say that it is a *theorem* of ZF that
>
>   "for any set x, for some ordinal a, x E V(a)" .
>
>[where V(a) is defined by  V(0) = {}
>                           V(a+1) = P{V{a}}
>                           V(L) = U{a < L}[V(a)] (L a limit ordinal). ]
>
>Is this really true ? Surely not. The collection of V's is a model for ZF, yes.
>But the above isn't a theorem, is it? 
>I expect it *is* a theorem of ZF+AxFndtn.
>
>Can you confirm this point please; and give a reference, if you still say
>it's a theorem of ZF only?

"ZF only" is conventionally taken to include Foundation.

Here is some more stuff:

\begin{defn}
\label{R}
\label{wellfounded}
% F&B, p.93-4, Jech, p.21, Levy, p.68
We define the function $R$ on all ordinals by transfinite recursion as
follows:
\begin{itemize}
\item[\I] $R(0) = \emptyset$,
\item[\II] $\varforall{\alpha}{}\sqdot R(S(\alpha)) = \f{P}(R(\alpha))$,
\item[\III] $\varforall{\lambda}{\Lim{\lambda}}\sqdot R(\lambda) =
\bigcup_{\beta < \alpha} R(\beta)$.
\end{itemize}
A set $x$ is said to be {\it well-founded} if it is a member (or a subset)
of $R(\alpha)$ for some ordinal $\alpha$.  The rank $\rho(x)$, or $\rank
(x)$, of a well-founded set $x$ is the least ordinal $\beta$ such that $x
\subseteq R(\beta)$: $$\rho (x) \Df (\mu \beta) \sqdot \Ord (\beta) \sqdot x
\subseteq R(\beta).$$
\end{defn}

(You may have to make some obvious adjustments to compile this.)

Being that an equivalent form of the Axiom of Foundation is that all
sets are well-founded, under these definitions each set has a rank.

>------------------------------------------------------------------------------
>            Bill Taylor              wft@math.canterbury.ac.nz
>------------------------------------------------------------------------------
>                   I think, therefore I am; (I think).
>------------------------------------------------------------------------------

cordially,
mikhail zeleny@husc.harvard.edu
" -- I shall speak bluntly, because life is short."