draft updates symmetry and NF consistency

Drafts/symmetricfoundations2.tex

@@ -47,11 +47,17 @@
 \begin{description}
 
 \item[Axiom of elementary sets (following Zermelo):]  The empty class $$\emptyset = \{x\in V:x \neq x\}$$ is a set.  For any sets $x,y$ the set $\{x,y\} = \{z\in V :z =x \vee z=y\}$ is a set.
-We define $\{x\}$ as $\{x,x\}$ and note that this axiom provides it for each set $x$.  We define $\iota(x)$ as $\{x\}$ and define $\iota^0(x)$ as $x$ and $\iota^{n+1}(x)$ as $\{\iota^n(x)\}$.
+We define $\{x\}$ as $\{x,x\}$ and note that this axiom provides it for each set $x$.  
 
-\item[Definition:]  We define the ordered pair $(x,y)$ as $\{\{x\},\{x,y\}\}$.  Notice that we can define $\pi_1(z)$ as the unique object which belongs to all elements of $z$, and otherwise as $\emptyset$, and define $\pi_2(z)$ as the unique object which belongs to exactly one element of $z$, if there is one, and otherwise as $\emptyset$,
+\item[Definition (iteration of singleton operation):]
+
+We define $\iota(x)$ as $\{x\}$ and define $\iota^0(x)$ as $x$ and $\iota^{n+1}(x)$ as $\{\iota^n(x)\}$.
+
+\item[Ordered Pairs:]  We define the ordered pair $(x,y)$ as $\{\{x\},\{x,y\}\}$.  Notice that we can define $\pi_1(z)$ as the unique object which belongs to all elements of $z$, and otherwise as $\emptyset$, and define $\pi_2(z)$ as the unique object which belongs to exactly one element of $z$, if there is one, and otherwise as $\emptyset$,
 and see that $\pi_i((x_1,x_2)) = x_i$ for $i=1,2$, so we get the basic property of ordered pairs:  if $(x_1,x_2) = (y_1,y_2)$ then $x_1=y_1$ (apply $\pi_1$ to both sides) and $x_2=y_2$ (apply $\pi_2$ to both sides).
 
+
+
 \item[Relations:]  We define ${\tt pair}(x)$ as $x=(\pi_1(x),\pi_2(x))$.  We define ${\tt relation}(R)$ as $(\forall x\in R:{\tt pair}(x))$.  A relation is a class of ordered pairs.  We define $x \, R\, y$ as ${\tt relation}(R) \wedge (x,y)\in R$.  We define $R^{-1}$ as $\{(y,x):y \, R\, x\}$.  We define
 ${\tt dom}(R)$ as $\{x\in V:(\exists y\in V:x \,R\,y)\}$.  We define ${\tt rng}(R)$ as ${\tt dom}(R^{-1})$.
 
@@ -62,7 +68,7 @@
 
 \item[Lifted permutations:]  If $\pi$ is a permutation, we define $j[\pi]$ as $$\{(A,f``A):A=A\}$$ if $(\forall A\in V:{\tt set}(f``A))$ and otherwise as $\emptyset$.
 Note that this will be a permutation iff it is not $\emptyset$.
-We define $j^0[\pi]$ as $\pi$ and $j^{n+1}[\pi]$ as $j[j^n[\pi])$ if it exists.
+We define $j^0[\pi]$ as $\pi$ and $j^{n+1}[\pi]$ as $j[j^n[\pi])$ if it exists.  Note that $j$ is not a function:  it is being ``applied" to permutations which are not in general assumed to be sets.
 
 \item[Setlike permutations:]  We say that a permutation $\pi$ is $n$-setlike iff $j^n[\pi] \neq \emptyset$.  We refer to 2-setlike permutations as simply setlike.  What this means, speaking informally, is that applying $\pi$ to iterated elements $n$ levels down sends sets to sets.
 
@@ -125,27 +131,27 @@
 
 \item[Lemma 3:]  If a class $A$ is 4-symmetric, it is 3-symmetric and so a set.  More generally, if a class $A$ is $n$-symmetric with $n>3$, it is 3-symmetric and so a set.
 
-\item[Proof of Lemma 2:]  Suppose that for all $\pi$ such that $j^3[\rho](s)=s$, $j^3[\rho]``A =A$
+\item[Proof of Lemma 3:]  Suppose that for all $\pi$ such that $j^3[\rho](s)=s$, $j^3[\rho]``A =A$
 
 Let $E = \{\{\{x\},y\}:x \in y\}$.  We claim that any permutation $\rho$ such that $j^2[\rho](E)=E$ is actually of the form $j[\rho']$.
 Such a permutation $\rho$ must have $j^2[\rho]``\{\{\{x\}\}:x \in V\}= \{\{\{x\}\}:x \in V\}$, since these are the 1-element elements of $E$.
 Define $\rho'$ by $j^2[\rho](\{\{x\}\}) = \{\{\rho'(x)\}\}$.  Observe further that because $j^2[\rho]$ fixes $E$, we have, for any $x \in y$, since this is equivalent to $\{\{x\},y\} \in E$,
-that $j[\rho](\{\{x\},y\}) = \{\rho(\{x\}),\rho(y)\} = \{\{rho'(x)\},rho(y)\} \in E$, so $\rho'(x) \in \rho(y)$ iff $x \in y$, so $j[\rho']=\rho$.
+that $j[\rho](\{\{x\},y\}) = \{\rho(\{x\}),\rho(y)\} = \{\{\rho'(x)\},\rho(y)\} \in E$, so $\rho'(x) \in \rho(y)$ iff $x \in y$, so $j[\rho']=\rho$.
 
 Using Lemma 2, construct a $t$ so that $j^2[\pi](t)=t$ implies $j^2[\pi](s)=s$ and $j^2[\pi](E)=E$, so there is $\rho$ such
 that $j[\rho]=\pi$, so  $j^3[\rho](s)=s$, so $j^3[\rho]``A =A$, so $j^2[\pi]``A=A$, so $A$ is a set with support $t$.
 
 Suppose that we have shown that if for all $\pi$ such that $j^n[\rho](s)=s$, $j^n[\rho]``A =A$, then $A$ is a set, for a fixed $n \geq 3$.
 
-Suppose that for all $\pi$ such that $j^{n+1}[\pi](s)=s$, $j^{n+1}[\pi]``A =A$, then $A$ is a set.
+Suppose that for all $\pi$ such that $j^{n+1}[\pi](s)=s$, we have $j^{n+1}[\pi]``A =A$.
 
 Thus we have for all $j[\pi]$ such that $j^n[j[\pi]](s) = s$ that $j^n[j[\pi]]``A = A$.
 
 Thus we have for all $\pi$ such that $j^2[\pi](E) = E$ and $j^n[\pi](s)=s$ that $ j^n[\pi]``A = A$.
 
 Thus we have for all $\pi$ such that $j^n[\pi](\iota^{n-2}(E)) = \iota^{n-2}(E)$ and $j^n[\pi](s)=s$ that  $ j^n[\pi]``A = A$, so $A$ is a set by Lemma 2 and the inductive hypothesis.
 
-The result follow for all $n$ by induction in the metatheory.
+The result follows for all $n$ by induction in the metatheory.
 
 
 

Nfproof/maybedetangled2.tex

@@ -52,6 +52,8 @@ \subsection{Dated remarks on versions}
 {\bf initial note for the previous series:}  This document is probably my best overall version so far.  The immediate occasion for its preparation was to serve students attempting to verify the proof in Lean.  A formal verification should avoid metamathematics, so it is the fact that the structure defined in section 3 is a model of TTT which should be verified, and further, a finite axiomatization (mod type indexing) of TST and thus TTT should be verified in the model in lieu of the usual statement of the axiom of comprehension of TTT.  {\bf This program has been completed, on the Lean side.}
 \begin{description}
 
+\item[5/18/2024:]  very slight adjustment in response to a question from Sky about inductive hypotheses about allowable permutations.
+
 \item[5/14/2024:]  I have made an explicit list of the hypotheses of the recursive construction in section 3, noting where they are used and where they are verified for subsequent stages.
 
 11:20 am further minor edits.
@@ -952,7 +954,7 @@ \subsection{Allowable permutations and supports}
 An $\beta$-allowable permutation ($\beta \leq \alpha$) is an $\beta$-structural permutation, each of whose derivatives $\pi_\gamma$ is a $\gamma$-allowable permutation (and satisfies the condition that $\pi_\gamma``\tau_\gamma = \tau_\gamma$) and which satisfies a coherence condition relating the $f$ maps and derivatives of the permutation:  for suitable $\gamma,\delta<\beta$, $$f_{\gamma,\delta}(\pi_\gamma(x),\pi_{\gamma}[S]) \sim \pi_\delta^+``f_{\gamma,\delta}(x,S).$$  (where the action of allowable
  permutations on supports will be defined shortly).
 
-Note that an $\alpha$-allowable permutation is actually defined on the entire supertype structure, though what interests us about it is its actions on objects in our purported TTT model.
+Note that an $\beta$-allowable permutation is actually defined on the entire supertype structure, though what interests us about it is its actions on objects in our purported TTT model.
 
 
 
@@ -1024,7 +1026,7 @@ \subsection{Allowable permutations and supports}
 \item[the definition of $\tau_\alpha$:]  We stipulate that all elements of $\tau_\beta$ ($\beta\in \alpha$) have $\beta$-supports ({\bf I10)}), and define $\tau_\alpha$ as the set of elements $x$ of $\tau^*_\alpha$ such that
 $x \cap \tau^*_{\beta} \subseteq \tau_\beta$ for each $\beta<\alpha$, $x$ is extensional, and $x$ has an $\alpha$-support.
 
-Note that an image of an element of $\tau_\alpha$ under an $\alpha$-allowable permutation will belong to $\tau_\alpha$.
+Note that an image of an element of $\tau_\beta$ ($\beta\leq \alpha$)  under a $\beta$-allowable permutation will belong to $\tau_\beta$, because supportedness and extensionality are preserved by allowable permutations.
 
 The definition explicitly enforces {\bf I1, I3, I5 (a near-litter obviously has a support), I6, I8, I9, I10} for subsequent stages of the construction.