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
Copy file name to clipboardExpand all lines: doc/epsilon0-chapter.tex
+35-26Lines changed: 35 additions & 26 deletions
Original file line number
Diff line number
Diff line change
@@ -353,9 +353,7 @@ \subsubsection{A Predicate for Characterizing Normal Forms}
353
353
\input{movies/snippets/T1/badTerm}
354
354
355
355
356
-
This term would have been written \(\omega^1\times 2 + \omega^\omega\times 3\) in the usual mathematical notation. We note that the exponents of $\omega$ are not in the right (strictly decreasing) order.
357
-
Nevertheless, with the help of the order \texttt{lt} on \texttt{T1}, we are now able to characterize
358
-
the set of all well-formed ordinal terms:
356
+
This term would have been written \(\omega^1\times 2 + \omega^\omega\times 3\) in the usual mathematical notation. We note that the exponents of $\omega$ are not in the right (strictly decreasing) order. The following boolean function determines whether a given ordinal term is well formed.
359
357
360
358
361
359
\vspace{4pt}
@@ -472,7 +470,7 @@ \subsubsection{\texttt{E0}: a sigma-type for \texorpdfstring{$\epsilon_0$}{epsil
472
470
473
471
\paragraph*{\gaiasign}
474
472
\index{gaiabridge}{Type of well formed ordinal terms below $\epsilon_0$}
475
-
The library~\href{../theories/html/gaia_hydras.T1Bridge.html}{gaia\_hydras.T1Bridge} defines a \gaia-compatible type \texttt{E0}.
473
+
Our library~\href{../theories/html/gaia_hydras.T1Bridge.html}{gaia\_hydras.T1Bridge} also defines a type \texttt{E0} (which doesn't exist in \gaia-\texttt{ssete9}).
476
474
477
475
478
476
@@ -483,7 +481,7 @@ \subsection{Syntactic definition of limit and successor ordinals}
In~\cite{Manolios2005}, Manolios and Vroom prove the well-foundedness of ordinal terms below $\epsilon_0$ by reduction to the natural order on the set of natural numbers.
746
747
\end{remark}
747
748
748
749
749
750
750
751
\subsection{An ordinal notation for \texorpdfstring{$\epsilon_0$}{epsilon0}}
751
752
752
-
We build an instance of \texttt{ON}, and prove its correctness w.r.t. Schutte's model (see Chapter~\ref{chap:schutte}).
753
753
754
+
We are now able to build an instance of \texttt{ON}.
Let us recall three results we have proved so far.
1136
-
\begin{itemize}
1137
-
\item There exists a strictly decreasing variant which maps \texttt{Hydra} into
1138
-
the segment $[0,\epsilon_0)$ for proving the termination of any hydra battle
1139
-
\item There exists \emph{no} such variant from \texttt{Hydra} into
1140
-
$[0,\omega^2)$, \emph{a fortiori} into $[0,\omega)$.
1141
-
\end{itemize}
1144
+
%Let us recall three results we have proved so far.
1145
+
%\begin{itemize}
1146
+
%\item There exists a strictly decreasing variant which maps \texttt{Hydra} into
1147
+
%the segment $[0,\epsilon_0)$ for proving the termination of any hydra battle
1148
+
%\item There exists \emph{no} such variant from \texttt{Hydra} into
1149
+
%$[0,\omega^2)$, \emph{a fortiori} into $[0,\omega)$.
1150
+
%\end{itemize}
1142
1151
1143
-
So, a natural question is `` Does there exist any strictly decreasing variant mapping
1144
-
type \texttt{Hydra} into some interval $[0,\alpha)$ (where $\alpha <\epsilon_0$) for proving the termination of all hydra battles''. The next chapter is dedicated to a formal proof that there exists no such $\alpha$, even if we consider a restriction to the set of ``standard'' battles.
1152
+
%So, a natural question is `` Does there exist any strictly decreasing variant mapping
1153
+
%type \texttt{Hydra} into some interval $[0,\mu)$ (where $\mu <\epsilon_0$) for proving the termination of all hydra battles''. The next chapter is dedicated to a formal proof that there exists no such $\mu$, even if we consider a restriction to the set of ``standard'' battles.
Copy file name to clipboardExpand all lines: doc/ks-chapter.tex
+31-26Lines changed: 31 additions & 26 deletions
Original file line number
Diff line number
Diff line change
@@ -31,7 +31,7 @@ \section{Introduction}
31
31
\end{quote}
32
32
33
33
Our proofs are constructive and require no axioms: they are closed terms of the CIC, and are mainly composed on function definitions and proofs of properties of these functions.
34
-
They share much theoretical material with Kirby and Paris', although they do not use any knowledge about Peano arithmetic nor model theory. The combinatorial arguments we use and implement
34
+
They borrow much theoretical material from Kirby and Paris, although they do not use any knowledge about Peano arithmetic nor about model theory. The combinatorial arguments we use and implement
35
35
come from
36
36
an article by J.~Ketonen and R.~Solovay~\cite{KS81}, already cited in the work
37
37
by L.~Kirby and J.~Paris. % on the termination of Goodstein sequences and hydra battles~\cite{KP82}.
@@ -49,31 +49,33 @@ \section{Canonical Sequences}
49
49
50
50
\index{maths}{Transfinite induction}
51
51
\begin{itemize}
52
-
\item If $\alpha\not=0$, then $\canonseq{\alpha}{i}<\alpha$. Thus canonical sequences can be used for proofs by transfinite induction or function definition by transfinite recursion
52
+
\item If $\alpha\not=0$, then $\canonseq{\alpha}{i}<\alpha$. Thus canonical sequences can be used in proofs by transfinite induction or function definition by transfinite recursion
53
53
\item If $\lambda$ is a limit ordinal, then $\lambda$ is the least upper bound of the set
54
54
$\{\canonseq{\lambda}{i}\;|\,i\in\mathbb{N}_1\}$
55
55
56
56
57
57
\item If $\beta<\alpha<\epsilon_0$, then there is a ``path'' from $\alpha$ to $\beta$, \emph{i.e.} a
58
58
sequence $\alpha_0=\alpha, \alpha_1, \dots, \alpha_n=\beta$, where for every $k<n$, there exists some $i_k$ such that $\alpha_{k+1}=\canonseq{\alpha_k}{i_k}$
59
-
\item Canonical sequences correspond tightly to rounds of hydra battles: if $\alpha\not=0$,
60
-
then $\iota(\alpha)$ is transformed into $\iota(\canonseq{\alpha}{i+1})$ in one round with
61
-
the replication factor $i$ (Lemma \href{../theories/html/hydras.Hydra.O2H.html\#canonS_iota_i}{Hydra.O2H.canonS\_iota\_i}).
62
-
\item From the two previous properties, we infer that whenever $\beta<\alpha<\epsilon_0$, there exists a (free) battle from $\iota(\alpha)$ to $\iota(\beta)$.
63
59
\end{itemize}
64
60
65
61
\begin{remark}
66
-
In~\cite{KS81}, canonical sequences are defined for any ordinal $\alpha <\epsilon_0$,
62
+
Canonical sequences are defined for any ordinal $\alpha <\epsilon_0$,
67
63
by stating that if $\alpha$ is a successor ordinal $\beta+1$, the sequence associated with
68
64
$\alpha$ is simply the constant sequence whose terms are equal to $\beta$.
69
65
Likewise, the canonical sequence of $0$ maps any natural number to $0$.
70
66
71
-
This convention allows us to make total the function that maps any ordinal $\alpha$ and natural number $i$ to the ordinal $\canonseq{\alpha}{i}$.
72
-
67
+
Thus, the function that maps any ordinal $\alpha$ and natural number $i$ to the ordinal $\canonseq{\alpha}{i}$ is total.
73
68
\end{remark}
74
69
70
+
\subsection{Canonical sequences and hydra battles}
75
71
76
-
First, let us recall how canonical sequences are defined in~\cite{KS81}. For efficiency's sake, we decided not to implement directly K.\&S's definitions, but to define in \gallina{} simply typed structurally recursive functions which share the abstract properties which are used in the mathematical proofs\footnote{With a small difference: the $0$-th term of the canonical sequence is not the same in our development as in~\cite{KS81}.}.
72
+
Canonical sequences correspond tightly to rounds of hydra battles: if $\alpha\not=0$,
73
+
then $\iota(\alpha)$ is transformed into $\iota(\canonseq{\alpha}{i+1})$ in one round with
74
+
the replication factor $i$ (Lemma \href{../theories/html/hydras.Hydra.O2H.html\#canonS_iota_i}{Hydra.O2H.canonS\_iota\_i}).
75
+
Thus, whenever $\beta<\alpha<\epsilon_0$, there exists a (free) battle from $\iota(\alpha)$ to $\iota(\beta)$.
76
+
77
+
\subsection{Definitions}
78
+
First, let us recall how canonical sequences are defined in~\cite{KS81}. For efficiency's sake, we decided not to implement directly K.\&S's definitions, but to define in \gallina{} simply typed structurally recursive functions which share the abstract properties which are used in the mathematical proofs.
77
79
78
80
79
81
@@ -125,8 +127,10 @@ \subsubsection{Canonical sequences in \coq}
125
127
126
128
\input{movies/snippets/Canon/canonDef}
127
129
128
-
\paragraph*{\gaiasign} Our library~\href{../theories/html/gaia_hydras.GCanon.html}{gaia\_hydras.GCanon} transposes the function \texttt{canon} into \gaia's type \texttt{T1}
129
-
(please see Sect.\~ref{sect:gcanon}).
130
+
\paragraph*{\gaiasign}
131
+
The translation of \texttt{canon} compatible with \gaia's data-types is
132
+
defined in ~\href{../theories/html/gaia_hydras.GCanon.html\#canon}{gaia\_hydras.GCanon} (please see Sect.~\ref{sect:gcanon}).
133
+
130
134
\index{gaiabridge}{Canonical sequences}
131
135
\paragraph*{Remark}
132
136
In the present state of this library, the following specializations of \texttt{canon} are still used in some proofs or lemma statements. They are planned to be deprecated.
@@ -195,8 +199,7 @@ \subsubsection{Limit ordinals are truly limits}
195
199
\label{lemma:canonS-limit}
196
200
197
201
198
-
Note the use of \coq's \texttt{sig} type in the theorem's statement, which
199
-
relates the boolean function \texttt{limitb} defined on the \texttt{T1} data-type with a constructive view of the limit of a sequence: for any $\beta<\lambda$, we can compute an item of the canonical sequence of $\lambda$ which is greater than $\beta$.
202
+
Note the use of \coq's \texttt{sig} type in the theorem's statement, which expresses a constructive view of the limit of a sequence: for any $\beta<\lambda$, we can compute an item of the canonical sequence of $\lambda$ which is greater than $\beta$.
200
203
We can also state directly that $\lambda$ is a (strict) least upper bound of the elements of its canonical sequence.
Let us consider a kind of accessibility problem inside $\epsilon_0$: given two ordinals $\alpha$ and $\beta$, where $\beta<\alpha<\epsilon_0$, find a \emph{path} consisting of a finite sequence $\gamma_0=\alpha,\dots,\gamma_l=\beta$,
235
-
where, for every $i<l$, $\gamma_i \not= 0$\footnote{This condition allows us to ignore paths which end by a lot of useless $0$s.} and there exists some strictly positive integer $s_i$
238
+
where, for every $i<l$, $\gamma_i \not= 0$
239
+
and there exists some strictly positive integer $s_i$
236
240
such that $\gamma_{i+1}=\canonseq{\gamma}{s_i}$.
237
241
238
242
Let $s$ be the sequence $\langle s_0,s_1,\dots, s_{l-1} \rangle$. We describe the
Note that, given $\alpha$ and $\beta$, where $\beta < \alpha$, the sequence $s$ which leads from $\alpha$ to $\beta$ is not unique.
250
-
Indeed, if $\alpha$ is a limit ordinal, the first element of $s$ can be any integer $i$ such that $\beta<\canonseq{\alpha}{i}$, and if $\alpha$ is a successor ordinal,
251
-
then the sequence $s$ can start with any positive integer.
The library~\href{../theories/html/gaia_hydras.GPaths.html}{gaia\_hydras.GPaths} transposes the notion of path into \gaia's type \texttt{T1}
288
-
(please see Sect.\~ref{sect:gpath}).
292
+
(please see Sect.~\ref{sect:gpath}).
289
293
290
294
291
295
\index{hydras}{Exercises}
@@ -312,7 +316,7 @@ \subsection{Existence of a path}
312
316
313
317
314
318
\noindent
315
-
From the lemma \texttt{canon\_LT}~\vref{lemma:canon_LT}, we can convert any path into an inequality on ordinals (by induction on paths).
319
+
By the lemma \texttt{canon\_LT}~(Sct.\vref{lemma:canon_LT}), we can convert any path into an inequality on ordinals (by induction on paths).
316
320
317
321
\input{movies/snippets/Paths/pathToLT}
318
322
@@ -532,12 +536,13 @@ \section{The case of standard battles}
532
536
533
537
534
538
535
-
Our goal is now to transform any inequality $\beta<\alpha<\epsilon_0$ into a standard path $\alpha\xrightarrow[i,j]{} \beta$ for some $i$ and $j$, then into a standard battle
536
-
from $\iota(\alpha+i)$ to $\iota(\beta)$.
539
+
Our goal is now to transform any inequality $\beta<\alpha<\epsilon_0$ into a standard path $\alpha\xrightarrow[i,j]{} \beta$ for some $i$ and $j$, which corresponds to a standard battle
540
+
from $\iota(\alpha)$ (at time $i$) to $\iota(\beta)$
541
+
(at time $j$) .
537
542
Following~\cite{KS81}, we proceed in two stages:
538
543
\begin{enumerate}
539
544
\item we simulate plain (free) paths from $\alpha$ to $\beta$ with
540
-
paths made of steps $(\gamma,\canonseq{\gamma}{n})$, \emph{with the same $n$ all along the path}
545
+
paths made of steps $(\gamma,\canonseq{\gamma}{n})$, \emph{with the same $n$ all along the path}.
541
546
\item we simulate any such path by a standard path.
Copy file name to clipboardExpand all lines: doc/large-sets-chapter.tex
+3-3Lines changed: 3 additions & 3 deletions
Original file line number
Diff line number
Diff line change
@@ -1,7 +1,7 @@
1
1
\chapter{Large sets and rapidly growing functions}\label{chap:alpha-large}
2
2
3
3
\begin{remark}
4
-
Some notations (mainly names of fast-growing functions) of our development may differ slightly from the literature. Although this fact does not affect our proofs, we are preparing a future version where the names $F\_alpha$, $f\_alpha$, $H\_alpha$, etc., are fully consistent with the cited articles.
4
+
Some notations (mainly names of fast-growing functions) of our development may differ slightly from the literature. Although this fact does not affect our proofs, we are preparing a future version where the names $F_\alpha$, $f_\alpha$, $H_\alpha$, etc., are fully consistent with the cited articles.
5
5
6
6
\end{remark}
7
7
%\section{Introduction}
@@ -109,7 +109,7 @@ \subsection{Examples}
109
109
\section{Length of minimal large sequences}
110
110
\label{sect:lalpha-section}
111
111
112
-
Now, consider any natural number $k>0$any ordinal $0<\alpha<\epsilon_0$. We would like to compute
112
+
Now, let us consider some natural number $k>0$and an ordinal $0<\alpha<\epsilon_0$. We would like to compute
113
113
a number $l$ such that the interval $[k,l]$ is $\alpha$-mlarge. So,
114
114
the standard battle starting with $\iota(\alpha)$ and the replication factor $k$ will end after $(l-k+1)$ steps.
115
115
@@ -136,7 +136,7 @@ \section{Length of minimal large sequences}
136
136
use \coq{} to reason about the \emph{specification} of \texttt{L},
137
137
prove properties of any function which satisfies this specification.
138
138
In Sect.~\ref{sect:L-equations}, we use the \texttt{coq-equations} plug-in
139
-
to define a function \texttt{L\_}, and prove its correctness w.r.t. its specification.
139
+
to define \texttt{L\_}, then prove its correctness w.r.t. its specification.
Copy file name to clipboardExpand all lines: doc/ordinal-chapter.tex
+2-5Lines changed: 2 additions & 5 deletions
Original file line number
Diff line number
Diff line change
@@ -952,14 +952,11 @@ \section{Comparing two ordinal notations}
952
952
\label{fig:subsegment}
953
953
\end{figure}
954
954
955
-
If \texttt{OB} is presumed to be correct, then we may consider that \texttt{OA} ``inherits'' its correctness from the bigger notation system \texttt{OB}.
0 commit comments