NF revision

Nfproof/maybedetangled2-for-arxiv.tex

@@ -93,6 +93,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 in our view (at least in the view of the first author) avoid metamathematics as far as possible, 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[1/8/2025:]  reviewed and slightly revised the proof of the existence of position functions.
+
 \item[1/1/2025:]  Sky proposed changes to the beginning of section 3, which are incorporated.
 
 \item[12/31/2024:]  Pulled out the section natural models and theories TST$_n$, because no use seems to be made of those concepts in the paper as it stands.
@@ -162,7 +164,7 @@ \subsection{The simple theory of types TST and TSTU}
 
 The witness to $(\exists A:(\forall x:x \in A \leftrightarrow \phi))$ is unique by extensionality, and we introduce the notation $\{x:\phi\}$ for this object.  Of course, $\{x:\phi\}$  is to be assigned type one higher than that of $x$;  in general, complex terms will have types as variables do.
 
-The modification which gives TSTU (the simple type theory of sets with urelements) replaces the extensionality axioms with the formulas of the shape $$(\forall xyw:w \in x \rightarrow (x=y \leftrightarrow (\forall z:z \in x \leftrightarrow z\in y))),$$  allowing many objects with no elements (called atoms or urelements)  in each positive type.  A technically useful refinement adds a constant $\emptyset^i$ of each positive type $i$ with no elements:  we can then address the problem that $\{x^i:\phi\}$ is not necessarily  uniquely defined when $\phi$ is uniformly false by defining $\{x^i:\phi\}$ as $\emptyset^{i+1}$ in this case.
+The modification which gives TSTU (the simple type theory of sets with urelements) replaces the extensionality axioms with the formulas of the shape $$(\forall xyw:w \in x \rightarrow (x=y \leftrightarrow (\forall z:z \in x \leftrightarrow z\in y))),$$  allowing many objects with no elements (called atoms or urelements)  in each positive type.  A technically useful refinement adds a constant $\emptyset^i$ of each positive type $i$ with no elements:  we can then address the problem that $\{x^i:\phi\}$ is not necessarily  uniquely defined when $\phi$ is uniformly false by defining $\{x^i:\phi\}$ as $\emptyset^{i+1}$ in this case.  The superscript is sometimes omitted from $\emptyset^i$ (and other constants parametrized by types) when the type can be deduced from context.
 
 \subsubsection{Typical ambiguity}
 
@@ -187,7 +189,7 @@ \subsubsection{Historical remarks}
 
 Russell noticed a phenomenon like the typical ambiguity of TST in the more complex system of {\em Principia Mathematica\/}, which he refers to as ``systematic ambiguity".
 
-In 1914 (\cite{wiener}), Norbert Wiener gave a definition of the ordered pair as a set (not the one now in use) and seems to have recognized that the type theory of {\em Principia Mathematica\/} could be simplified to something like TST, but he did not give a formal description.  The theory we call TST was apparently first described by Tarski in the 1930s.
+In 1914 (\cite{wiener}), Norbert Wiener gave a definition of the ordered pair as a set (not the one now in use) and seems to have recognized that the type theory of {\em Principia Mathematica\/} could be simplified to something like TST, but he did not give a formal description.  The theory we call TST was apparently first described by Tarski in the 1930s\footnote{We regard it as an important feature of TST that the nature of type 0 is left completely undetermined, so we do not regard descriptions of arithmetic of order $\omega$ appearing about the same time as part of this history.     Arithmetic of order $\omega$ is a similar typed theory but lacks the ambiguity of interest here.}.
 
 It is worth observing that the axioms of TST look exactly like those of ``naive set theory", the restriction preventing paradox being embodied in the restriction of the language by the type system.
 For example, the Russell paradox is averted because one cannot have $\{x:x \not\in x\}$ because $x \in x$ (and so its negation $\neg x \in x$) cannot be a well-formed formula.
@@ -252,8 +254,8 @@ \subsection{New Foundations and NFU}
 The concrete implementation follows.  NF is the first order unsorted theory with equality and membership as primitive with an axiom of extensionality $(\forall xy:x=y \leftrightarrow (\forall z:z \in x \leftrightarrow z\in y))$ and an axiom of comprehension $(\exists A:(\forall x:x \in A \leftrightarrow \phi))$ for each formula $\phi$ in which $A$ is not free which can be obtained from a formula of TST by dropping all distinctions of type.  We give a precise formalization of this idea:  provide a bijective map $(x \mapsto x^*)$ from the countable supply of variables (of all types) of TST onto the countable supply of variables of the language of NF.  Where $\phi$ is a formula of the language of TST, let $\phi^*$ be the formula obtained by replacing every variable $x$, free and bound,
 in $\phi$ with $x^*$. For each formula $\phi$ of the language of TST in which $A$ is not free in $\phi^*$ and each variable $x^*$, an axiom of comprehension of NF asserts $(\exists A:(\forall x^*:x^* \in A \leftrightarrow \phi^*))$.
 
-In the original paper, this is expressed in a way which avoids explicit dependence on the language of another theory.  Let $\phi$ be a formula of the language of
-NF.  A function $\sigma$ is a stratification of $\phi$ if it is a (possibly partial) map from variables to non-negative integers such that for each atomic subformula
+In the original paper, this is expressed in a way which avoids explicit dependence on the language of another theory.  We do this in a way which is usual now but not necessarily identical to what is done in the original paper.  Let $\phi$ be a formula of the language of
+NF.    A function $\sigma$ is a stratification of $\phi$ if it is a (possibly partial) map from variables to non-negative integers such that for each atomic subformula
 `$x=y$'  of $\phi$ we have $\sigma($`$x$'$)=\sigma($`$y$'$)$ and for each atomic subformula `$x \in y$' of $\phi$ we have $\sigma($`$x$'$)+1 = \sigma($`$y$'$)$.
 A formula $\phi$ is said to be stratified iff there is a stratification of $\phi$.  Then for each stratified formula $\phi$ of the language of NF and variable $x$ we have an axiom $(\exists A:(\forall x:x \in A \leftrightarrow \phi))$.  The stratified formulas are exactly the formulas $\phi^*$ up to renaming of variables.
 
@@ -870,7 +872,7 @@ \subsection{Machinery for enforcing extensionality in the model}\label{ss:extens
 \end{definition}
 
 The function may be constructed directly: first choose an ordering of type $\mu$ on litters, then put {singletons of} atoms directly after the litter they are inside (and before all later litters), then put near-litters after the corresponding litter and all {singletons of} atoms in the symmetric difference, then map each near-litter or {singleton of an} atom to its position in the resulting order.
-We don't run out of room before finishing the construction because $\mu$ has cofinality at least $\kappa$.
+We don't run out of room before finishing the construction because $\mu$ has cofinality at least $\kappa$.  We prove more formally that there are such functions just below.
 
 \begin{lemma}[position function generator]\label{lem:position_generator}
 
@@ -880,7 +882,7 @@ \subsection{Machinery for enforcing extensionality in the model}\label{ss:extens
 $f(x)$ is bounded, then there is an injection
 $\iota : X \to
 \mu$ such that
-$\iota(x) \notin f(x)$.
+$\iota(x) \not\in f(x)$.
 
 \end{lemma}
 
@@ -911,8 +913,7 @@ \subsection{Machinery for enforcing extensionality in the model}\label{ss:extens
 
  Since $\{
 \iota(y) : y < x \}$ has cardinality less than
-$\mu$, the difference must be nonempty, so the definition given is always
- well-defined.
+$\mu$, the difference must be nonempty, so the definition given always succeeds.
 
 \end{proof}
 
@@ -938,13 +939,12 @@ \subsection{Machinery for enforcing extensionality in the model}\label{ss:extens
 \nu
 \leq
 \iota_0(N^\circ)
- \} \cup \{
+ \} \cup 
+\bigcup_{a \in N \Delta N^{\circ}}\{
 \nu :
 \nu
 \leq
-\iota_1(a), a
-\in N
-\Delta N^\circ \},$$
+\iota_1(a)\},$$
 
  to obtain $\iota_2$.
 
@@ -977,7 +977,7 @@ \subsection{Machinery for enforcing extensionality in the model}\label{ss:extens
 \times
 \mu$ with the lexicographic order, we can then define
 $\iota_*(x)$ to be the position of
-$g(x)$ in the natural order of the restriction of 
+$g(x)$ in the restriction of the natural order on
 $3
 \times
 \mu$ to the image of
@@ -988,12 +988,13 @@ \subsection{Machinery for enforcing extensionality in the model}\label{ss:extens
 
 \end{proof}
 
-
+\begin{comment}
 \hsuggest{[MARKED FOR DELETION after review] We give a detailed description of how to do this. Choose a well-ordering $\leq_0$ of order type $\mu$ on the set of all near-litters.  
 
 We refer to a near-litter which is not a litter as a proper near-litter.  With each litter, singleton of atom, or proper near-litter associate a triple of ordinals.  For a litter, the first ordinal will be its position in the order $\leq_0$, and the next two will be 0.  For a singleton of an atom, the first ordinal will be the position in $\leq_0$ of the  litter $L$ which includes it, the second will be the successor of the position of its element in $\leq_L$, and the third will be zero.   For a proper near-litter $N$, the first ordinal will be the supremum of the position in $\leq_0$ of $N^\circ$ and the positions in $\leq_0$ of the litters in containing each element of $N\Delta N^\circ$ ($<\mu$ by cofinality), the second ordinal will be the supremum of the positions of the elements $x$ of $N \Delta N^\circ$ in the respective orders $\leq_{x^\circ}$, where $x^\circ$ is the litter containing $x$ ($<\kappa$ by regularity), and the third will be the successor of the position of $N$ itself in $\leq_0$.
 
 The order on the litters, singletons of atoms, and proper near-litters will be determined by lexicographic order on the associated triples.  This is clearly a well-ordering designed explicitly to have the properties indicated above, and has order type $\mu$ because each item in this order can be seen to have $<\mu$ possible predecessors, on the basis of its first coordinate:  this is obvious for a triple representing a litter;  for a triple representing a singleton of an atom, there are $\kappa$ choices for the second coordinate and one for the third;  for a triple representing a near-litter, there are $\kappa$ choices for the second coordinate, and there are $<\mu$ near litters which are subsets of the union of the litters with position in $\leq_0$ at or before the first coordinate, simply because this union is a set of size $<\mu$ which has $<\mu$ subsets because $\mu$ is strong limit, so there are $<\mu$ possible values for the third coordinate.}
+\end{comment}
 
 
 An additional property involving $\iota_*$ which is enforced by inductive hypotheses explained later about the maps $\iota_\beta^+$ is that $\iota_*(N) \leq \iota_*^+(N_\delta,S)$ will hold for any near litter $N$ and support $S$ of $N_\delta$ \ihref{ih:pos_typed_near_litter}.  It must be noted here because it is shortly used.