\documentclass[runningheads]{llncs} \usepackage{amssymb,url,alltt} \usepackage[all]{xy} \raggedbottom \def\mizerror#1{\strut\rlap{\hspace\hsize\ \texttt{*#1}}} \def\xverb#1{\underbar{\tt{#1}}} \def\xsemi{\xverb{;}} \begin{document} \title{Ten Formal Proof Sketches} \author{Freek Wiedijk} \institute{Radboud University Nijmegen} \maketitle \begin{abstract} This note collects the formal proof sketches that I have done. \end{abstract} \section{Algebra: Irrationality of $\sqrt{2}$} \subsection{Source} G.H.~Hardy and E.M.~Wright, {\em An Introduction to the Theory of Numbers.} 4th edition, Clarendon Press, Oxford, 1960. Pages 39--40. \subsection{Informal Proof} {\sc Theorem 43 (Pythagoras' theorem).} {\em $\sqrt{2}$ is irrational.} \medskip\noindent The traditional proof ascribed to Pythagoras runs as follows. If $\sqrt{2}$ is rational, then the equation $$a^2 = 2b^2 \eqno{(4.3.1)}$$ is soluble in integers $a$, $b$ with $(a,b) = 1$. Hence $a^2$ is even, and there%- fore $a$ is even. If $a = 2c$, then $4c^2 = 2b^2$, $2c^2 = b^2$, and $b$ is also even, contrary to the hypothesis that $(a,b) = 1$. \subsection{Formal Proof Sketch: Informal Layout} {\sc theorem} Th43:$\,$ {\it $\mathop{\mbox{\rm sqrt}} 2$ is irrational\/} $\,$:: {\sc Pythagoras' theorem} \medskip\noindent {\sc proof}$\,$ assume $\mathop{\mbox{\rm sqrt}} 2$ is rational; consider $a,b$ such that $$\mbox{$a\mathbin{\hat{}}2 = 2\mathbin{*}b\mathbin{\hat{}}2$}\leqno{\mbox{4\_3\_1:}}$$ and $a,b$ are\_relative\_prime; $a\mathbin{\hat{}}2$ is even; $a$ is even; consider $c$ such that $a = 2\mathbin{*}c$; $4\mathbin{*}c\mathbin{\hat{}}2 = 2\mathbin{*}b\mathbin{\hat{}}2$; $2\mathbin{*}c\mathbin{\hat{}}2 = b\mathbin{\hat{}}2$; $b$ is even; thus contradiction; $\,${\sc end}; \subsection{Formal Proof Sketch: Formal Layout} \begin{flushleft}\footnotesize \verb|theorem Th43: sqrt 2 is irrational|\\ \verb|proof|\\ \verb| assume sqrt 2 is rational;|\\ \verb| consider a,b such that|\\ \verb|4_3_1: a^2 = 2*b^2 and|\\ \mizerror{4}\verb| a,b are_relative_prime;|\\ \mizerror{4}\verb| a^2 is even;|\\ \mizerror{4}\verb| a is even;|\\ \mizerror{4}\verb| consider c such that a = 2*c;|\\ \mizerror{4}\verb| 4*c^2 = 2*b^2;|\\ \mizerror{4}\verb| 2*c^2 = b^2;|\\ \mizerror{4}\verb| b is even;|\\ \mizerror{1}\verb| thus contradiction;|\\ \verb|end;| \end{flushleft} \subsection{Formal Proof} \begin{flushleft}\footnotesize \xverb{theorem Th43: sqrt 2 is irrational}\\ \xverb{proof}\\ \verb| |\xverb{assume sqrt 2 is rational;}\\ \verb| then |\xverb{consider a,b such that}\\ \verb|A1: b <> 0 and|\\ \verb|A2: sqrt 2 = a/b and|\\ \verb|A3: |\xverb{a,b are\char`_relative\char`_prime}\verb| by Def1;|\\ \verb|A4: b^2 <> 0 by A1,SQUARE_1:73;|\\ \verb| 2 = (a/b)^2 by A2,SQUARE_1:def 4|\\ \verb| .= a^2/b^2 by SQUARE_1:69;|\\ \verb| then|\\ \xverb{4\char`_3\char`_1: a\^{}2 = 2*b\^{}2}\verb| by A4,REAL_1:43|\xsemi\\ \verb| |\xverb{a\^{}2 is even}\verb| by 4_3_1,ABIAN:def 1|\xsemi\\ \verb| then|\\ \verb|A5: |\xverb{a is even}\verb| by PYTHTRIP:2|\xsemi\\ \verb| then |\xverb{consider c such that}\\ \verb|A6: |\xverb{a = 2*c}\verb| by ABIAN:def 1|\xsemi\\ \verb|A7: |\xverb{4*c\^{}2 =}\verb| (2*2)*c^2|\\ \verb| .= 2^2*c^2 by SQUARE_1:def 3|\\ \verb| .= |\xverb{2*b\^{}2}\verb| by A6,4_3_1,SQUARE_1:68|\xsemi\\ \verb| 2*(2*c^2) = (2*2)*c^2 by AXIOMS:16|\\ \verb| .= 2*b^2 by A7;|\\ \verb| then |\xverb{2*c\^{}2 = b\^{}2}\verb| by REAL_1:9|\xsemi\\ \verb| then b^2 is even by ABIAN:def 1;|\\ \verb| then |\xverb{b is even}\verb| by PYTHTRIP:2|\xsemi\\ \verb| then 2 divides a & 2 divides b by A5,Def2;|\\ \verb| then|\\ \verb|A8: 2 divides a gcd b by INT_2:33;|\\ \verb| a gcd b = 1 by A3,INT_2:def 4;|\\ \verb| |\xverb{hence contradiction}\verb| by A8,INT_2:17|\xsemi\\ \xverb{end;} \end{flushleft} \subsection{Mizar Version} 6.1.11 -- 3.33.722 \section{Algebra: Infinity of Primes} \subsection{Source} The slides of a talk by Herman Geuvers, {\em Formalizing an intuitionistic proof of the Fundamental Theorem of Algebra.} \subsection{Informal Proof} {\sc Theorem}$\,$ There are infinitely many primes:\\ for every number $n$ there exists a prime $p> n$ \medskip \medskip\noindent \textsc{Proof} [after Euclid]\\ Given $n$. Consider $k=n!+1$, where $n!=1\cdot 2\cdot 3\cdot \ldots\cdot n$.\\ Let $p$ be a prime that divides $k$.\\ For this number $p$ we have $p> n$: otherwise $p\leq n$;\\ but then $p$ divides $n!$,\\ so $p$ cannot divide $k=n!+1$,\\ contradicting the choice of $p$. QED \subsection{Formal Proof Sketch: Informal Layout} {\sc theorem}$\,$ $\{n: n\mbox{\rm\ is prime}\}$ is infinite $\,${\sc proof}\\ for $n$ ex $p$ st $p$ is prime \& $p > n$ \medskip\noindent {\sc proof} :: [after Euclid]\\ let $n$; set $k = n! + 1$;\\ consider $p$ such that $p$ is prime \& $p$ divides $k$;\\ take $p$; thus $p$ is prime; thus $p > n$ $\,${\sc proof}$\,$ assume $p <= n$;\\ $p$ divides $n!$;\\ not $p$ divides $n! + 1$;\\ thus contradiction; $\,${\sc end; end;} thus thesis; {\sc end;} \subsection{Formal Proof Sketch: Formal Layout} \begin{flushleft}\footnotesize \verb|theorem {n: n is prime} is infinite|\\ \verb|proof|\\ \verb| for n ex p st p is prime & p > n|\\ \verb| proof|\\ \verb| let n;|\\ \verb| set k = n! + 1;|\\ \mizerror{4}\verb| consider p such that p is prime & p divides k;|\\ \verb| take p;|\\ \mizerror{4}\verb| thus p is prime;|\\ \verb| thus p > n|\\ \verb| proof|\\ \verb| assume p <= n;|\\ \mizerror{4}\verb| p divides n!;|\\ \mizerror{4}\verb| not p divides n! + 1;|\\ \mizerror{1}\verb| thus contradiction;|\\ \verb| end;|\\ \verb| end;|\\ \mizerror{4}\verb| thus thesis;|\\ \verb|end;| \end{flushleft} \subsection{Formal Proof} \begin{flushleft}\footnotesize \xverb{theorem {\char`\{}p: p is prime{\char`\}} is infinite}\\ \xverb{proof}\\ \verb|A1: |\xverb{for n ex p st p is prime \& p > n}\\ \verb| |\xverb{proof}\\ \verb| |\xverb{let n;}\\ \verb| |\xverb{set k = n! + 1;}\\ \verb| n! > 0 by NEWTON:23;|\\ \verb| then n! >= 0 + 1 by NAT_1:38;|\\ \verb| then k >= 1 + 1 by REAL_1:55;|\\ \verb| then |\xverb{consider p such that}\\ \verb|A2: |\xverb{p is prime \& p divides k}\verb| by INT_2:48|\xsemi\\ \verb| |\xverb{take p;}\\ \verb| |\xverb{thus p is prime}\verb| by A2|\xsemi\\ \verb| |\xverb{assume}\\ \verb|A3: |\xverb{p <= n;}\\ \verb| p <> 0 by A2,INT_2:def 5;|\\ \verb| then|\\ \verb|A4: |\xverb{p divides n!}\verb| by A3,NAT_LAT:16|\xsemi\\ \verb| p > 1 by A2,INT_2:def 5;|\\ \verb| then not p divides 1 by NAT_1:54;|\\ \verb| |\xverb{hence contradiction}\verb| by A2,A4,NAT_1:57|\xsemi\\ \verb| |\xverb{end;}\\ \verb| |\xverb{thus thesis}\verb| from Unbounded(A1)|\xsemi\\ \xverb{end;} \end{flushleft} \subsection{Mizar Version} 6.1.11 -- 3.33.722 \section{Algebra: Image of Left Unit Element} \subsection{Source} Rob Nederpelt, {\em Weak Type Theory: A formal language for mathematics.} Computer Science Report 02-05, Eindhoven University of Technology, Department of Math.~and Comp.~Sc., May 2002. Page 42. \subsection{Informal Proof} {\sc Theorem.} Let $G$ be a set with a binary operation $\cdot$ and left unit element $e$. Let $H$ be a set with binary operation $*$ and assume that $\phi$ is a homo%- morphism of $G$ onto $H$. Then $H$ has a left unit element as well. \medskip\noindent {\sc Proof.} Take $e' = \phi(e)$. Let $h\in H$. There is $g\in G$ such that $\phi(g) = h$. Then $$e' * h = \phi(e) * \phi(g) = \phi(e\cdot g) = \phi(g) = h,$$ hence $e'$ is left unit element of $H$.\hfill$\Box$ \subsection{Formal Proof Sketch: Informal Layout} \quad let $G,H$ be non empty HGrStr; let $e$ be Element of $G$ such that $e$ is\_left\_unit\_of $G$; let {\it phi\/} be map of $G,H$ such that {\it phi\/} is\_homomorphism $G,H$ and {\it phi\/} is onto; thus ex $e'$ being Element of $H$ st $e'$ is\_left\_unit\_of $H$\medskip\\ {\sc proof}$\,$ take $e' = \mbox{\it phi\/}.e$; now let $h$ be Element of $H$; consider $g$ being Element of $G$ such that $\mbox{\it phi\/}.g = h$; thus $$\mbox{$e' * h = \mbox{\it phi\/}.e * \mbox{\it phi\/}.g \mathrel{\mbox{.=}} \mbox{\it phi\/}.(e * g) \mathrel{\mbox{.=}} \mbox{\it phi\/}.g \mathrel{\mbox{.=}} h$;}$$ end; hence $e'$ is\_left\_unit\_of $H$; \hfill {\sc end;} \subsection{Formal Proof Sketch: Formal Layout} \begin{flushleft}\footnotesize \verb| let G,H be non empty HGrStr;|\\ \verb| let e be Element of G such that e is_left_unit_of G;|\\ \verb| let phi be map of G,H such that|\\ \verb| phi is_homomorphism G,H and phi is onto;|\\ \verb| thus ex e' being Element of H st e' is_left_unit_of H|\\ \verb|proof|\\ \verb| take e' = phi.e;|\\ \verb| now|\\ \verb| let h be Element of H;|\\ \mizerror{4}\verb| consider g being Element of G such that phi.g = h;|\\ \mizerror{4$\;$*4$\;$*4$\;$*4}\verb| thus e' * h = phi.e * phi.g .= phi.(e * g) .= phi.g .= h;|\\ \verb| end;|\\ \mizerror{4}\verb| hence e' is_left_unit_of H;|\\ \verb|end;| \end{flushleft} \subsection{Formal Proof} \begin{flushleft}\footnotesize \verb| |\xverb{let G,H be non empty HGrStr;}\\ \verb| |\xverb{let e be Element of G such that}\\ \verb|H1: |\xverb{e is\char`_left\char`_unit\char`_of G;}\\ \verb| |\xverb{let phi be map of G,H such that}\\ \verb|H2: |\xverb{phi is\char`_homomorphism G,H and}\\ \verb|H3: |\xverb{phi is onto;}\\ \verb| |\xverb{thus ex e' being Element of H st e' is\char`_left\char`_unit\char`_of H}\\ \xverb{proof}\\ \verb| |\xverb{take e' = phi.e;}\\ \verb| |\xverb{now}\\ \verb| |\xverb{let h be Element of H;}\\ \verb| |\xverb{consider g being Element of G such that}\\ \verb|A1: |\xverb{phi.g = h}\verb| by H3,Th1|\xverb{;}\\ \verb| |\xverb{thus e' * h = phi.(e * g)}\verb| by A1,H2,Def2|\\ \verb| |\xverb{.= h}\verb| by A1,H1,Def1|\xverb{;}\\ \verb| |\xverb{end;}\\ \verb| |\xverb{hence e' is\char`_left\char`_unit\char`_of H}\verb| by Def1|\xverb{;}\\ \xverb{end;} \end{flushleft} \subsection{Mizar Version} 6.1.11 -- 3.33.722 \section{Algebra: Lagrange's Theorem} \subsection{Source} B.L. van der Waerden, \emph{Algebra}. 5th edition, Springer-Verlag, Berlin, 1966. Page 26. \subsection{Informal Proof} \strut\hspace{\parindent}% Zwei Nebenklassen $a\mathfrak{g}$, $b\mathfrak{g}$ k\"onnen sehr wohl gleich sein, ohne da{\ss} $a = b$ ist. Immer dann n\"amlich, wenn $a^{-1}b$ in $\mathfrak{g}$ liegt, gilt $$b\mathfrak{g} = aa^{-1}b\mathfrak{g} = a(a^{-1}b\mathfrak{g}) = a\mathfrak{g}.$$ Zwei {\it verschiedene} Nebenklassen haben kein Element gemeinsam. Denn wenn die Nebenklassen $a\mathfrak{g}$ und $b\mathfrak{g}$ ein Element gemein haben, etwa $$ag_1 = bg_2,$$ so folgt $$g_1g_2^{-1} = a^{-1}b.$$ so da{\ss} $a^{-1}b$ in $\mathfrak{g}$ liegt; nach dem Vorigen sind also $a\mathfrak{g}$ und $b\mathfrak{g}$ identisch. Jedes Element $a$ geh\"ort einer Nebenklasse an, n\"amlich der Neben\-% klasse $a\mathfrak{g}$. Diese enth\"alt ja sicher das Element $ae = a$. Nach dem eben Bewiesenen geh\"ort das Element $a$ auch {\it nur} einer Nebenklasse an. Wir k\"onnen demnach jedes Element $a$ als {\it Repr\"asentanten} der $a$ enthaltenden Nebenklass $a\mathfrak{g}$ ansehen. Nach dem vorhergehenden bilden die Nebenklassen eine {\it Klassen\-% einteilung} der Gruppe $\mathfrak{G}$. Jedes Element geh\"ort einer und nur einer Klasse an. Je zwei Nebenklassen sind gleichm\"achtig. Denn durch $a\mathfrak{g} \to b\mathfrak{g}$ ist eine eineindeutige Abbildung von $a\mathfrak{g}$ auf $b\mathfrak{g}$ definiert. Die Nebenklassen sind, mit Ausnahme von $\mathfrak{g}$ selbst, {\it keine} Gruppen; denn eine Gruppe m\"u{\ss}te das Einselelement enthalten. Die Anzahl der verschiedenen Nebenklassen einer Untergruppe $\mathfrak{g}$ in $\mathfrak{G}$ hei{\ss}t der {\it Index} von $\mathfrak{g}$ in $\mathfrak{G}$. Der Index kann endlich oder un\-% endlich sein. Ist $N$ die als (endlich angenommene) Ordnung von $\mathfrak{G}$, $n$ die von $\mathfrak{g}$, $j$~der Index, so gilt die Relation $$N = jn;\leqno{(2)}$$ denn $\mathfrak{G}$ ist ja in $j$ Klassen eingeteilt, deren jede $n$ Elemente enth\"alt. Man kann f\"ur endliche Gruppen aus (2) den Index $j$ berechnen: $$j = {N\over n}$$ Folge. {\it Die Ordnung einer Untergruppe einer endlichen Gruppe ist ein Teiler der Ordnung der Gesamtgruppe.} \subsection{Formal Proof Sketch: Informal Layout} \strut\hspace{\parindent}% now let a,b; assume $a\mbox{\char`\^$^{-1}$}*b$ in $G$; thus $$b*G = a*a\mbox{\char`\^$^{-1}$}*b*G .= a*(a\mbox{\char`\^$^{-1}$}*b*G) .= a*G; \eqno{\mbox{\it end;}}$$ for $a,b$ st $a*G <> b*G$ holds $(a*G) \mathbin{/\backslash} (b*G) = \{\}$ \noindent proof let a,b; now assume $(a*G) \mathbin{/\backslash} (b*G) <> \{\}$; consider $g_1,g_2$ such that $$a*g_1 = b*g_2\mbox{;}$$ $$g_1*g_2\mbox{\char`\^$^{-1}$} = a\mbox{\char`\^$^{-1}$}*b;\smallskip$$ $a\mbox{\char`\^$^{-1}$}*b$ in $G$; thus $a*G = b*G$; end; thus thesis; end; for $a$ holds $a$ in $a*G$ proof let $a$; $a*e(G) = a$; thus thesis; end; $\{a*G : a\mbox{ in }H\}\mbox{ is a\char`\_partition of }H$; for $a,b$ holds $\mbox{card}(a*G) = \mbox{card}(b*G)$ proof let $a,b$; consider $f$ being Function of $a*G,b*G$ such that for $g$ holds $f.(a*g) = b*g$; $f$ is bijective; thus thesis; end; set $\mbox{'Index'} = \mbox{card} \{a*G : a\mbox{ in }H\}$; now let $N$ such that $N = \mbox{card }H$; let $n$ such that $n = \mbox{card }G$; let $j$ such that $j = \mbox{'Index'}$; thus \begin{center} '2':\hfill $N = j*n$;\hfill{\it end;} \end{center} thus {\it card $G$ divides card $H$}; \subsection{Formal Proof Sketch: Formal Layout} \begingroup \def\\{\char`\\} \def\{{\char`\{} \def\}{\char`\}} \let\semi=\; \def\;{$\semi$} \begin{alltt}\footnotesize now let a,b; assume a^-1*b in G; \mizerror{4\;*4\;*4} thus b*G = a*a^-1*b*G .= a*(a^-1*b*G) .= a*G; end; for a,b st a*G <> b*G holds (a*G) /\\ (b*G) = \{\} proof let a,b; now assume (a*G) /\\ (b*G) <> \{\}; \mizerror{4} consider g1,g2 such that a*g1 = b*g2; \mizerror{4} g1*g2^-1 = a^-1*b; \mizerror{4} a^-1*b in G; \mizerror{4} thus a*G = b*G; end; \mizerror{4} thus thesis; end; for a holds a in a*G proof let a; \mizerror{4} a*e(G) = a; \mizerror{4} thus thesis; end; \mizerror{4}\{a*G : a in H\} is a_partition of H; for a,b holds card(a*G) = card(b*G) proof let a,b; consider f being Function of a*G,b*G such that \mizerror{4} for g holds f.(a*g) = b*g; \mizerror{4} f is bijective; \mizerror{4} thus thesis; end; set 'Index' = card \{a*G : a in H\}; now let N such that N = card H; let n such that n = card G; let j such that j = 'Index'; thus \mizerror{4}'2': N = j*n; end; \mizerror{4}thus card G divides card H; \end{alltt} \endgroup \subsection{Formal Proof} \begingroup \def\\{\char`\\} \def\{{\char`\{} \def\}{\char`\}} \def\'{\char`\'} \def\x#1{\underbar{#1}} \begin{alltt}\footnotesize A1: \x{now} \x{let a,b;} \x{assume} A2: \x{a^-1*b in G;} \x{thus b*G =} e(H)*b*G by GROUP_1:def 5 .= \x{a*a^-1*b*G} by GROUP_1:def 6 .= a*(a^-1*b)*G by GROUP_1:def 4 \x{.= a*(a^-1*b*G)} by GROUP_2:127 .= a*(carr G) by A2,GROUP_2:136 \x{.= a*G} by GROUP_2:def 13\x{;} \x{end;} A3: \x{for a,b st a*G <> b*G holds (a*G) /\\ (b*G) = \{\}} \x{proof} \x{let a,b;} \x{now} \x{assume (a*G) /\\ (b*G) <> \{\};} then consider x such that A4: x in (a*G) /\\ (b*G) by XBOOLE_0:7; A5: x in a*G & x in b*G by A4,XBOOLE_0:def 4; \x{consider g1} such that A6: x = a*g1 by A5,Th5; consider \x{g2 such that} A7: x = b*g2 by A5,Th5; set g1G = g1; set g2G = g2; reconsider g1 as Element of H by GROUP_2:51; reconsider g2 as Element of H by GROUP_2:51; A8: \x{a*g1 =} a*g1G by Th2 .= \x{b*g2} by A6,A7,Th2\x{;} g1G*g2G^-1 = g1*g2G^-1 by Th3 .= \x{g1*g2^-1} by Th2,GROUP_2:57 .= e(H)*g1*g2^-1 by GROUP_1:def 5 .= a^-1*a*g1*g2^-1 by GROUP_1:def 6 .= a^-1*(a*g1)*g2^-1 by GROUP_1:def 4 .= a^-1*(b*g2*g2^-1) by A8,GROUP_1:def 4 .= a^-1*(b*(g2*g2^-1)) by GROUP_1:def 4 .= a^-1*(b*e(H)) by GROUP_1:def 6 .\x{= a^-1*b} by GROUP_1:def 5\x{;} then \x{a^-1*b in G} by STRUCT_0:def 5\x{;} \x{hence a*G = b*G} by A1\x{;} \x{end;} \x{hence thesis;} \x{end;} A9: \x{for a holds a in a*G} \x{proof} \x{let a;} \x{a*e(G) =} a*e(H) by Th2,GROUP_2:53 .= \x{a} by GROUP_1:def 5\x{;} \x{hence thesis;} \x{end;} set X = \{a*G : a in H\}; X c= bool the carrier of H proof let A; assume A in X; then consider a such that A10: A = a*G & a in H; thus A in bool the carrier of H by A10,ZFMISC_1:def 1; end; then reconsider X as Subset-Family of H; A11: X is a_partition of the carrier of H proof thus union X = the carrier of H proof thus union X c= the carrier of H; let x; assume A12: x in the carrier of H; then reconsider a = x as Element of H; x in H by A12,STRUCT_0:def 5; then a in a*G & a*G in X by A9; hence x in union X by TARSKI:def 4; end; let A be Subset of the carrier of H; assume A in X; then consider a such that A13: A = a*G & a in H; thus A <> \{\} by A13; let B be Subset of the carrier of H; assume B in X; then consider b such that A14: B = b*G & b in H; assume A <> B; then A /\\ B = \{\} by A3,A13,A14; hence A misses B by XBOOLE_0:def 7; end; then reconsider X as a_partition of H; \x{\{a*G : a in H\} is a_partition of H} by A11\x{;} A15: \x{for a,b holds card(a*G) = card(b*G)} \x{proof} \x{let a,b;} defpred P[Element of a*G,Element of b*G] means for g st $1 = a*g holds $2 = b*g; A16: now let x be Element of a*G; consider g such that A17: x = a*g by Th5; reconsider y = b*g as Element of b*G; take y; thus P[x,y] by A17,Th4; end; \x{consider f being Function of a*G,b*G such that} A18: for x being Element of a*G holds P[x,f.x qua Element of b*G] from FUNCT_2:sch 3(A16); \x{for g holds f.(a*g) = b*g} by A18\x{;} \x{f is bijective} proof hereby let x,x' be Element of a*G; consider g such that A19: x = a*g by Th5; consider g' such that A20: x' = a*g' by Th5; A21: f.x = b*g & f.x' = b*g' by A19,A20,A18; assume f.x = f.x'; hence x = x' by A19,A20,A21,Th4; end; let y be Element of b*G; consider g such that A22: y = b*g by Th5; take a*g; thus thesis by A18,A22; end\x{;} \x{hence thesis} by EUCLID_7:3\x{;} \x{end;} \x{set \'Index\' = card \{a*G : a in H\};} 'Index' = card X; then reconsider 'Index' as natural number; \x{now} \x{let N such that} A23: \x{N = card H;} \x{let n such that} A24: \x{n = card G;} \x{let j such that} A25: \x{j = \'Index\';} A26: card H = card the carrier of H by STRUCT_0:def 17; now let A; assume A in X; then consider a such that A27: A = a*G & a in H; e(H)*G = carr(G) by GROUP_2:132 .= the carrier of G by GROUP_2:def 9; then card(e(H)*G) = card G by STRUCT_0:def 17; hence card A = n by A15,A24,A27; end; \x{hence N = j*n} by A23,A25,A26,Th1\x{;} \x{end;} then card H = 'Index'*card G; \x{hence card G divides card H} by INT_1:def 9\x{;} \end{alltt} \endgroup \subsection{Mizar Version} 7.11.01 -- 4.117.1046 \section{Analysis: successor has no fixed point} \subsection{Source} Fairouz Kamareddine, Manuel Maarek and J.B.~Wells, {\em MathLang: experience-driven development of a new mathematical language,} draft. Page 11. Quoted from: Edmund Landau, {\em Foundations of Analysis.} Translated by F. Steinhardt, Chelsea, 1951. \subsection{Informal Proof} \textbf{Theorem 2} $$x' \ne x$$ \medskip\noindent \textbf{Proof} \ Let $\mathfrak{M}$ be the set of all $x$ for which this holds true. \begin{enumerate} \item[I)] By Axiom 1 and Axiom 3, $$1' \ne 1;$$ therefore 1 belongs to $\mathfrak{M}$. \medskip \item[II)] If $x$ belongs to $\mathfrak{M}$, then $$x' \ne x,$$ and hence by Theorem 1, $$(x')' \ne x',$$ so that $x'$ belongs to $\mathfrak{M}$. \end{enumerate} By Axiom 5, $\mathfrak{M}$ therefore contains all the natural numbers, i.e.~we have for each $x$ that $$x' \ne x.$$ \subsection{Formal Proof Sketch: Informal Layout} \textbf{Theorem}\_2: $$x\;' \mathrel{<>} x$$ \medskip\noindent \textbf{proof} \ set $\mathfrak{M} = \{y : y\;' \mathrel{<>} y\}$; \begin{enumerate} \item[I:] now $$1\;' \mathrel{<>} 1$$ by Axiom\_1, Axiom\_3; hence $1$ in $\mathfrak{M}$; \hfill\emph{end;} \medskip \item[II:] now let $x$; assume $x$ in $\mathfrak{M}$; then $$x\;' \mathrel{<>} x;$$ then $$(x\;')' \mathrel{<>} x\;'$$ by Theorem\_1; hence $x\;'$ in $\mathfrak{M}$; \hfill\emph{end;} \end{enumerate} for $x$ holds $x$ in $\mathfrak{M}$ by Axiom\_5; hence $$x\;' \mathrel{<>} x; \eqno{\mbox{\emph{end;}}}$$ \subsection{Formal Proof Sketch: Formal Layout} \begin{flushleft}\footnotesize \verb|Theorem_2: x ' <> x|\\ \verb|proof|\\ \verb| set M = {y : y ' <> y};|\\ \verb|I: now|\\ \verb| 1 ' <> 1 by Axiom_1, Axiom_3;|\\ \mizerror{4}\verb| hence 1 in M;|\\ \verb| end;|\\ \verb|II: now let x;|\\ \verb| assume x in M;|\\ \mizerror{4}\verb| then x ' <> x;|\\ \verb| then (x ')' <> x ' by Theorem_1;|\\ \verb| hence x ' in M;|\\ \verb| end;|\\ \mizerror{4}\verb| for x holds x in M by Axiom_5;|\\ \mizerror{4}\verb| hence x ' <> x;|\\ \verb|end;| \end{flushleft} \subsection{Formal Proof} \begin{flushleft}\footnotesize \xverb{Theorem\char`\_2: x ' <> x}\\ \xverb{proof}\\ \verb| |\xverb{set M = \char`\{y : y ' <> y\char`\};}\\ \xverb{I: now}\\ \verb| |\xverb{1 ' <> 1 by Axiom\char`\_3;}\\ \verb| |\xverb{hence 1 in M by Axiom\char`\_1;}\\ \verb| |\xverb{end;}\\ \verb| |\xverb{now let x;}\\ \verb| |\xverb{assume x in M;}\\ \verb| |\xverb{then}\verb| ex y st x = y & |\xverb{y ' <> y;}\\ \verb| |\xverb{then (x ')' <> x '}\verb| by Axiom_4|\xsemi\\ \verb| |\xverb{hence x ' in M;}\\ \verb| |\xverb{end;}\\ \verb| then |\xverb{x in M by }\verb|I,|\xverb{Axiom\char`\_5;}\\ \verb| then ex y st x = y & y ' <> y;|\\ \verb| |\xverb{hence x ' <> x;}\\ \xverb{end;} \end{flushleft} \subsection{Mizar Version} 6.4.01 -- 3.60.795 \section{Analysis: successor has no fixed point} \subsection{Source} A message \emph{Formal verification} on the FOM mailing list by Lasse Rempe-Gillen $\langle$\verb|L.Rempe@liverpool|\penalty100\verb|.ac.uk|$\rangle$, dated 21 October 2014 and with Message-ID\break $\langle${\verb|675123965B518F43B235C5FCB5D565DCBF14577E@CHEXMBX1.livad.liv.ac.uk|}$\rangle$.$\hspace{-1cm}$ \subsection{Informal Proof} \emph{Let $f$ be a real-valued function on the real line, such that $f(x)>x$ for all $x$. Let $x_0$ be a real number, and define the sequence $(x_n)$ recursively by $x_{n+1} := f(x_n)$. Then $x_n$ diverges to infinity.} \medskip\noindent A standard proof might go along the following steps: 1) By assumption, the sequence is strictly increasing; 2) hence the sequence either diverges to infinity or has a finite limit; 3) by continuity, any finite limit would have to be a fixed point of $f$, hence the latter cannot occur. \subsection{Formal Proof Sketch: Informal Layout} \emph{now let $f$ be continuous Function of {\small REAL},{\small REAL}; assume for $x$ holds $f.(x) > x$; let $x_0$ be Element of {\small REAL}; set $x$ = \emph{recursively\_iterate}($f$,$x_0$); $x_{.(n + 1)} = f.(x_{.n})$; thus $x$ is divergent\_to+infty} \medskip\noindent proof$\enskip$ $x$ is increasing; $x$ is divergent\_to+infty or $x$ is convergent; $x$ is convergent implies $f.(\lim x) = \lim x$; $x$ is not convergent; $\enskip$thus thesis; end; \emph{end;} \subsection{Formal Proof Sketch: Formal Layout} \begin{flushleft}\footnotesize \verb|now |\\ \verb| let f be continuous Function of REAL,REAL;|\\ \verb| assume for x holds f.(x) > x;|\\ \verb| let x0 be Element of REAL; |\\ \verb| set x = recursively_iterate(f,x0);|\\ \mizerror{4}\verb| x.(n + 1) = f.(x.n);|\\ \verb| thus x is divergent_to+infty|\\ \verb| proof|\\ \mizerror{4}\verb| x is increasing;|\\ \mizerror{4}\verb| x is divergent_to+infty or x is convergent;|\\ \mizerror{4}\verb| x is convergent implies f.(lim x) = lim x;|\\ \mizerror{4}\verb| x is not convergent;|\\ \mizerror{4}\verb| thus thesis;|\\ \verb| end;|\\ \verb|end;| \end{flushleft} \subsection{Formal Proof} \begin{flushleft}\footnotesize \xverb{now}\\ \verb| |\xverb{let f be continuous Function of REAL,REAL;}\\ \verb| |\xverb{assume}\\ \verb|A1: |\xverb{for x holds f.(x) > x;}\\ \verb| |\xverb{let x0 be Element of REAL;}\\ \verb| |\xverb{set x = recursively\char`\_iterate(f,x0);}\\ \verb|A2: |\xverb{x.(n + 1) = f.(x.n)}\verb| by Def1|\xverb{;}\\ \verb| |\xverb{thus x is divergent\char`\_to+infty}\\ \verb| |\xverb{proof}\\ \verb| now let n;|\\ \verb| x.(n + 1) = f.(x.n) by A2;|\\ \verb| hence x.(n + 1) > x.n by A1;|\\ \verb| end;|\\ \verb| then|\\ \verb|A3: |\xverb{x is increasing}\verb| by SEQM_3:def 6|\xverb{;}\\ \verb| then x is bounded_above implies x is convergent;|\\ \verb| then|\\ \verb|A4: |\xverb{x is divergent\char`\_to+infty or x is convergent}\verb| by A3,LIMFUNC1:31|\xverb{;}\\ \verb| |\xverb{x is convergent implies f.(lim x) = lim x}\\ \verb| proof|\\ \verb| assume|\\ \verb|A5: x is convergent;|\\ \verb|A6: dom f = REAL by PARTFUN1:def 2;|\\ \verb|A7: rng x c= dom f by A6,RELAT_1:def 19;|\\ \verb|A8: now let n;|\\ \verb| reconsider m = n as Element of NAT by ORDINAL1:def 12;|\\ \verb| x.(m + 1) = f.(x.m) by A2|\\ \verb| .= (f /* x).m by A7,FUNCT_2:108;|\\ \verb| hence x.(n + 1) = (f /* x).n;|\\ \verb| end;|\\ \verb| f is_continuous_in lim x by A6,XREAL_0:def 1,FCONT_1:def 2;|\\ \verb| hence f.(lim x) = lim (f /* x) by A5,A7,FCONT_1:def 1|\\ \verb| .= lim (x ^\ 1) by A8,NAT_1:def 3|\\ \verb| .= lim x by A5,SEQ_4:22;|\\ \verb| end|\xverb{;}\\ \verb| then |\xverb{x is not convergent}\verb| by A1|\xverb{;}\\ \verb| |\xverb{hence thesis}\verb| by A4|\xverb{;}\\ \verb| |\xverb{end;}\\ \xverb{end;} \end{flushleft} \subsection{Mizar Version} 8.1.02 -- 5.22.1191 \section{Linear Algebra: Linear Independence} \subsection{Source} Jean Gallier, {\em Basics of Algebra and Analysis For Computer Science.} Published at \url{}, University of Pennsylvania, 2001. Page 16. \subsection{Informal Proof} {\bf Lemma 2.1.} {\em Given a linearly independent family $(u_i)_{i\in I}$ of elements of a vector space $E$, if $v\in E$ is not a linear combination of $(u_i)_{i\in I}$, then the family $(u_i)_{i\in I}\cup_k (v)$ obtained by adding $v$ to the family $(u_i)_{i\in I}$ is linearly independent (where $k\not\in I$).} \medskip\noindent {\em Proof.} Assume that $\mu v + \sum_{i\in I} \lambda_i u_i = 0$, for any family $(\lambda_i)_{i\in I}$ of scalars in $K$. If $\mu\ne 0$, then $\mu$ has an inverse (because $K$ is a field), and thus we have $v = -\sum_{i\in I} (\mu^{-1}\lambda_i) u_i$, showing that $v$ is a linear combination of $(u_i)_{i\in I}$ and contradicting the hypothesis. Thus, $\mu = 0$. But then, we have $\sum_{i\in I} \lambda_i u_i = 0$, and since the family $(u_i)_{i\in I}$ is linearly independent, we have $\lambda_i = 0$ for all $i\in I$. $\hfill\Box$ \subsection{Formal Proof Sketch: Informal Layout} {\bf theorem Lem21:} {\em $u$ is linearly-independent\/} \& {\em not $v$ in $\mbox{\rm Lin}(u)$ implies $u \mathbin{\backslash/} \{v\}$ is linearly-independent} \medskip\noindent {\em proof\/} assume $u$ is linearly-independent \& not $v$ in $\mbox{\rm Lin}(u)$; assume $u \mathbin{\backslash/} \{v\}$ is linearly-dependent; consider $m$ being Element of $K$, $l$ being Linear\_Combination of $u$ such that $m*v + \mbox{\rm Sum}(l) = 0.E$; now assume $m \mathrel{<>} 0.K$; $v = -m"*\mbox{\rm Sum}(l)$; $v$ in $\mbox{\rm Lin}(u)$; thus contradiction; end; $m = 0.K$; $\mbox{\rm Sum}(l) = 0.E$; $\mbox{\rm Carrier}(l) = \{\}$; thus contradiction; {\em end;} \subsection{Formal Proof Sketch: Formal Layout} \begin{flushleft}\footnotesize \verb|theorem Lem21:|\\ \verb| u is linearly-independent & not v in Lin(u) implies|\\ \verb| u \/ {v} is linearly-independent|\\ \verb|proof|\\ \verb| assume u is linearly-independent & not v in Lin(u);|\\ \verb| assume u \/ {v} is linearly-dependent;|\\ \verb| consider m being Element of K,|\\ \verb| l being Linear_Combination of u such that|\\ \mizerror{4}\verb| m*v + Sum(l) = 0.E;|\\ \verb| now|\\ \verb| assume m <> 0.K;|\\ \mizerror{4}\verb| v = -m"*Sum(l);|\\ \mizerror{4}\verb| v in Lin(u);|\\ \mizerror{1}\verb| thus contradiction;|\\ \verb| end;|\\ \mizerror{4}\verb| m = 0.K;|\\ \mizerror{4}\verb| Sum(l) = 0.E;|\\ \mizerror{4}\verb| Carrier(l) = {};|\\ \mizerror{1}\verb| thus contradiction;|\\ \verb|end;| \end{flushleft} \subsection{Formal Proof} \begin{flushleft}\footnotesize \xverb{theorem Lem21:}\\ \verb| |\xverb{u is linearly-independent \& not v in Lin(u) implies}\\ \verb| |\xverb{u \char`\\/ {\char`\{}v{\char`\}} is linearly-independent}\\ \xverb{proof}\\ \verb| |\xverb{assume}\\ \verb|A1: |\xverb{u is linearly-independent \& not v in Lin(u);}\\ \verb| given l' being Linear_Combination of u \/ {v} such that|\\ \verb|A2: Sum(l') = 0.E & Carrier(l') <> {};|\\ \verb| |\xverb{consider}\verb| m' being Linear_Combination of {v},|\\ \verb| |\xverb{l being Linear\char`_Combination of u such that}\\ \verb|A3: l' = m' + l by Th2;|\\ \verb| set m = m'.v;|\\ \verb|A4: |\xverb{m*v + Sum(l) =}\verb| Sum(m') + Sum(l) by VECTSP_6:43|\\ \verb| .= |\xverb{0.E}\verb| by A2,A3,VECTSP_6:77|\xsemi\\ \verb|A5: |\xverb{now}\\ \verb| |\xverb{assume}\\ \verb|A6: |\xverb{m <> 0.K;}\\ \verb| m*v = -Sum(l) by A4,RLVECT_1:def 10;|\\ \verb| then |\xverb{v =}\verb| m"*(-Sum(l)) by A6,VECTSP_1:67|\\ \verb| .= |\xverb{-m"*Sum(l)}\verb| by VECTSP_1:69|\xsemi\\ \verb| then|\\ \verb|A7: v = (-m")*Sum(l) by VECTSP_1:68;|\\ \verb| Sum(l) in Lin(u) by VECTSP_7:12;|\\ \verb| |\xverb{hence contradiction}\verb| by A1,A7,VECTSP_4:29|\xsemi\\ \verb| |\xverb{end;}\\ \verb| |\xverb{Sum(l) =}\verb| 0.E + Sum(l) by VECTSP_1:7|\\ \verb| .= |\xverb{0.E}\verb| by A4,A5,VECTSP_1:59|\xsemi\\ \verb| then|\\ \verb|A8: |\xverb{Carrier(l) = {\char`\{}{\char`\}}}\verb| by A1,VECTSP_7:def 1|\xsemi\\ \verb| now|\\ \verb| let x be set;|\\ \verb|A9: Carrier(m') c= {v} by VECTSP_6:def 7;|\\ \verb| not v in Carrier(m') by A5,VECTSP_6:20;|\\ \verb| hence not x in Carrier(m') by A9,TARSKI:def 1;|\\ \verb| end;|\\ \verb| then Carrier(m') = {} by BOOLE:def 1;|\\ \verb| then Carrier(l) \/ Carrier(m') = {} by A8;|\\ \verb| then Carrier(l') c= {} by A3,VECTSP_6:51;|\\ \verb| |\xverb{hence contradiction}\verb| by A2,BOOLE:30|\xsemi\\ \xverb{end;} \end{flushleft} \subsection{Mizar Version} 6.1.11 -- 3.33.722 \section{Mathematical Logic: Newman's Lemma} \subsection{Source} Henk Barendregt, {\em The Lambda Calculus: Its Syntax and Semantics.} North Holland, 1984. Page 58. \subsection{Informal Proof} 3.1.25. {\sc Proposition.} {\em For notions of reduction one has $$\mbox{\rm SN}\land\mbox{\rm WCR}\Rightarrow\mbox{\rm CR}$$}% {\sc Proof.} By SN each term $R$-reduces to an $R$-nf. It suffices to show that this $R$-nf is unique. Call $M$ {\em ambiguous\/} if $M$ $R$-reduces to two distinct $R$-nf's. For such $M$ one has $M\to_R M'$ with $M'$ ambiguous (use WCR, see figure 3.3). Hence by SN ambiguous terms do not exist. \medskip $$\xymatrix@=1.6em{&& M\ar[dl]\ar[dr] &&&& & M\ar[d] &\\ & M'\ar@{->>}[ddl]\ar@{->>}[dr] && \ar@{->>}[dl]\ar@{->>}[ddr] &&\mbox{ or }& & M'\ar@{->>}[d] &\\ && \ar@{->>}[d] &&&& & \ar@{->>}[dl]\ar@{->>}[dr] &\\ M_1 && M_3 && M_2 && M_1 && M_2} $$ \begin{center} {\sc fig.}~3.3. \end{center} \subsection{Formal Proof Sketch: Informal Layout} \begingroup \def\rewritearrow{\mathrel{\mbox{\rm {-}{-}{-}$>$}}} \def\doublerewritearrow{\mathrel{\mbox{\rm {-}{-}$>\!>$}}} {\sc theorem 3\_1\_25:} $$\mbox{$R$ is SN \& $R$ is WCR implies $R$ is CR}$$ {\sc proof}$\,$ assume that $R$ is SN and $R$ is WCR; for $M$ ex $M_1$ st $M$ reduces\_to $M_1$; (for $M,M_1,M_2$ st $M$ reduces\_to $M_1$ \& $M$ reduces\_to $M_2$ holds $M_1 = M_2$) implies $R$ is CR; defpred ambiguous[Term of $R$] means ex $M_1,M_2$ st $\$1$ reduces\_to $M_1$ \& $\$1$ reduces\_to $M_2$ \& $M_1 \mathrel{<>} M_2$; now now let $M$ such that ambiguous[$M$]; thus ex $M'$ st $M \rewritearrow M'$ \& ambiguous[$M'$] \begin{quote} {\sc proof} consider $M_1,M_2$ such that $M \doublerewritearrow M_1$ \& $M \doublerewritearrow M_2$ \& $M_1 <> M_2$; per cases; suppose not ex $M'$ st $M \rewritearrow M'$ \& $M' \doublerewritearrow M_1$ \& $M' \doublerewritearrow M_2$; consider $M'$ such that $M \rewritearrow M'$ \& $M' \doublerewritearrow M_1$; consider $M''$ such that $M \rewritearrow M''$ \& $M'' \doublerewritearrow M_2$; consider $M'''$ such that $M' \doublerewritearrow M'''$ \& $M'' \doublerewritearrow M'''$; consider $M_3$ such that $M''' \doublerewritearrow M_3$; take $M'$; thus thesis; suppose ex $M'$ st $M \rewritearrow M'$ \& $M' \doublerewritearrow M_1$ \& $M' \doublerewritearrow M_2$; consider $M'$ such that $M \rewritearrow M'$ \& $M' \doublerewritearrow M_1$ \& $M' \doublerewritearrow M_2$; take $M'$; thus thesis; {\sc end;} \end{quote} {\sc end;} thus not ex $M$ st ambiguous[$M$]; {\sc end;} thus thesis; {\sc end;} \endgroup \subsection{Formal Proof Sketch: Formal Layout} \begin{flushleft}\footnotesize \verb|theorem 3_1_25:|\\ \verb| R is SN & R is WCR implies R is CR|\\ \verb|proof|\\ \verb| assume that R is SN and R is WCR;|\\ \mizerror{4}\verb| for M ex M1 st M reduces_to M1;|\\ \verb| (for M,M1,M2 st M reduces_to M1 & M reduces_to M2 holds M1 = M2)|\\ \mizerror{4}\verb| implies R is CR;|\\ \verb| defpred ambiguous[Term of R] means|\\ \verb| ex M1,M2 st $1 reduces_to M1 & $1 reduces_to M2 & M1 <> M2;|\\ \verb| now|\\ \verb| now|\\ \verb| let M such that ambiguous[M];|\\ \verb| thus ex M' st M ---> M' & ambiguous[M']|\\ \verb| proof :: begin fig 3.3|\\ \mizerror{4}\verb| consider M1,M2 such that M -->> M1 & M -->> M2 & M1 <> M2;|\\ \verb| per cases;|\\ \verb| suppose not ex M' st M ---> M' & M' -->> M1 & M' -->> M2;|\\ \mizerror{4}\verb| consider M' such that M ---> M' & M' -->> M1;|\\ \mizerror{4}\verb| consider M'' such that M ---> M'' & M'' -->> M2;|\\ \mizerror{4}\verb| consider M''' such that M' -->> M''' & M'' -->> M''';|\\ \mizerror{4}\verb| consider M3 such that M''' -->> M3;|\\ \verb| take M';|\\ \mizerror{4,4}\verb| thus thesis;|\\ \verb| suppose ex M' st M ---> M' & M' -->> M1 & M' -->> M2;|\\ \mizerror{4}\verb| consider M' such that M ---> M' & M' -->> M1 & M' -->> M2;|\\ \verb| take M';|\\ \mizerror{4,4}\verb| thus thesis;|\\ \verb| end; :: end fig 3.3|\\ \verb| end;|\\ \mizerror{4}\verb| thus not ex M st ambiguous[M];|\\ \verb| end;|\\ \mizerror{4}\verb| thus thesis;|\\ \verb|end;| \end{flushleft} \subsection{Formal Proof} \begin{flushleft}\footnotesize \xverb{theorem 3\char`_1\char`_25:}\\ \verb| |\xverb{R is SN \& R is WCR implies R is CR}\\ \xverb{proof}\\ \verb| |\xverb{assume that}\\ \verb|A1: |\xverb{R is SN and}\\ \verb|A2: |\xverb{R is WCR;}\\ \verb|A3: R is WN by A1,Th9;|\\ \verb| then |\xverb{for M ex M1 st M reduces\char`_to M1}\verb| by Def10;|\\ \verb|A4: |\xverb{(for M,M1,M2 st M reduces\char`_to M1 \& M reduces\char`_to M2 holds M1 = M2)}\\ \verb| |\xverb{implies R is CR}\\ \verb| proof|\\ \verb| assume|\\ \verb|A5: for M,M1,M2 st M reduces_to M1 & M reduces_to M2 holds M1 = M2;|\\ \verb| let M,M',M'';|\\ \verb| assume|\\ \verb|A6: M -->> M' & M -->> M'';|\\ \verb| consider M1 such that|\\ \verb|A7: M' -->> M1 by A3,Def10;|\\ \verb| consider M2 such that|\\ \verb|A8: M'' -->> M2 by A3,Def10;|\\ \verb| M -->> M1 & M -->> M2 by A6,A7,A8,Th6;|\\ \verb| then M' -->> M1 & M'' -->> M1 by A5,A7,A8;|\\ \verb| hence thesis;|\\ \verb| end|\xsemi\\ \verb| |\xverb{defpred ambiguous[Term of R] means}\\ \verb| |\xverb{ex M1,M2 st \$1 reduces\char`_to M1 \& \$1 reduces\char`_to M2 \& M1 <> M2;}\\ \verb|A9: |\xverb{now}\\ \verb|A10: |\xverb{now}\\ \verb| |\xverb{let M such that}\\ \verb|A11: |\xverb{ambiguous[M];}\\ \verb| |\xverb{thus ex M' st M ---> M' \& ambiguous[M']}\\ \verb| |\xverb{proof :: begin fig 3.3}\\ \verb| |\xverb{consider M1,M2 such that}\\ \verb|A12: |\xverb{M -->> M1 \& M -->> M2 \& M1 <> M2}\verb| by A11|\xsemi\\ \verb| |\xverb{per cases;}\\ \verb| |\xverb{suppose}\\ \verb|A13: |\xverb{not ex M' st M ---> M' \& M' -->> M1 \& M' -->> M2;}\\ \verb| M1 is_nf & M2 is_nf by Def9;|\\ \verb| then|\\ \verb|A14: M <> M1 & M <> M2 by A12,Th8;|\\ \verb| then |\xverb{consider M' such that}\\ \verb|A15: |\xverb{M ---> M' \& M' -->> M1}\verb| by A12,Th7|\xsemi\\ \verb| |\xverb{consider M'' such that}\\ \verb|A16: |\xverb{M ---> M'' \& M'' -->> M2}\verb| by A12,A14,Th7|\xsemi\\ \verb| |\xverb{consider M''' such that}\\ \verb|A17: |\xverb{M' -->> M''' \& M'' -->> M'''}\verb| by A2,A15,A16,Def11|\xsemi\\ \verb| |\xverb{consider M3 such that}\\ \verb|A18: |\xverb{M''' -->> M3}\verb| by A3,Def10|\xsemi\\ \verb| |\xverb{take M';}\\ \verb| M' -->> M3 & M'' -->> M3 by A17,A18,Th6;|\\ \verb| then M' -->> M1 & M' -->> M3 & M1 <> M3 by A13,A15,A16;|\\ \verb| |\xverb{hence thesis}\verb| by A15|\xsemi\\ \verb| |\xverb{suppose ex M' st M ---> M' \& M' -->> M1 \& M' -->> M2;}\\ \verb| then |\xverb{consider M' such that}\\ \verb|A19: |\xverb{M ---> M' \& M' -->> M1 \& M' -->> M2;}\\ \verb| |\xverb{take M';}\\ \verb| |\xverb{thus thesis}\verb| by A12,A19|\xsemi\\ \verb| |\xverb{end; :: end fig 3.3}\\ \verb| |\xverb{end;}\\ \verb| |\xverb{thus not ex M st ambiguous[M]}\verb| from SN_induction1(A1,A10)|\xsemi\\ \verb| |\xverb{end;}\\ \verb| |\xverb{thus thesis}\verb| by A4,A9|\xsemi\\ \xverb{end;} \end{flushleft} \subsection{Mizar Version} 6.1.11 -- 3.33.722 \section{Mathematical Logic: Diaconescu's Theorem} \subsection{Source} Michael Beeson, \emph{Foundations of Constructive Mathematics}. Springer-Verlag,\penalty-10000 1985. %Page ?. \subsection{Informal Proof} \begingroup \def\N{\textbf{N}} \def\land{\mathrel{\&}} \parskip=\smallskipamount \hspace{\parindent} \textbf{1.1 Theorem} (Diaconescu [1975]). \emph{The axiom of choice implies the law of excluded middle, using separation and extensionality.} \emph{Proof.} Let a formula $\phi$ be given; we shall derive $\phi \lor \neg\phi$. Let $A = \{n\in\N: n = 0 \lor (n = 1 \land \phi)\}$. Let $B = \{n\in\N: n = 1 \lor (n = 0 \land \phi)\}$. Then $\forall\,x\in\{A,B\}\, \exists\,y\in\N\, (y\in x)$. Suppose $f$ is a choice function, so that $f(A)\in A$ and $f(B)\in B$. We have $f(A) = f(B) \lor f(A)\ne f(B)$, since the values are integers. If $f(A) = f(B)$ then $\phi$, so $\phi \lor \neg\phi$. If $f(A)\ne f(B)$, then $\neg\phi$ can be derived: suppose $\phi$. Then $A = B$ by extensionality, so $f(A) = f(B)$, contradiction. Hence in either case $\phi \lor \neg\phi$. \hfill$\Box$ \endgroup \subsection{Formal Proof Sketch: Informal Layout} \begingroup \parskip=\smallskipamount \def\land{\mathrel{\&}} \def\phi{\mbox{\it phi\,}} \hspace{\parindent}% \textbf{scheme} Diaconescu \emph{$\{ \phi[] \}$ : axiom\_of\_choice implies $\phi[]$ or not $\phi[]$} \emph{proof} assume axiom\_of\_choice; set $A = \{n : n = 0\mbox{ or }(n = 1 \land \phi[])\}$; set $B = \{n : n = 1\mbox{ or }(n = 0 \land \phi[])\}$; for $x$ st $x$ in $\{A,B\}$ holds ex $y$ st $y$ in $x$; consider $f$ being choice\_function such that $f$ is extensional; $f.A$ in $A \land f.B$ in $B$; $f.A = f.B$ or $f.A <> f.B$ by excluded\_middle\_on\_integers; per cases; suppose $f.A = f.B$; $\phi[]$; thus $\phi[]$ or not $\phi[]$; end; suppose $f.A <> f.B$; not $\phi[]$ proof assume $\phi[]$; $A = B$ by extensionality; $f.A = f.B$; thus contradiction; end; thus $\phi[]$ or not $\phi[]$; end; \hfill end; \endgroup \subsection{Formal Proof Sketch: Formal Layout} \begin{flushleft}\footnotesize \verb|scheme Diaconescu :: 1975|\\ \verb| { phi[] } : axiom_of_choice implies phi[] or not phi[]|\\ \verb|proof|\\ \verb| assume axiom_of_choice;|\\ \verb| set A = {n : n = 0 or (n = 1 & phi[])};|\\ \verb| set B = {n : n = 1 or (n = 0 & phi[])};|\\ \mizerror{4}\verb| for x st x in {A,B} holds ex y st y in x;|\\ \verb| consider f being choice_function such that|\\ \mizerror{4}\verb| f is extensional;|\\ \mizerror{4,4}\verb| f.A in A & f.B in B;|\\ \verb| f.A = f.B or f.A <> f.B by excluded_middle_on_integers;|\\ \verb| per cases;|\\ \verb| suppose f.A = f.B;|\\ \mizerror{4}\verb| phi[];|\\ \verb| thus phi[] or not phi[];|\\ \verb| end;|\\ \verb| suppose f.A <> f.B;|\\ \verb| not phi[]|\\ \verb| proof|\\ \verb| assume phi[];|\\ \mizerror{4}\verb| A = B by extensionality;|\\ \mizerror{4}\verb| f.A = f.B;|\\ \mizerror{1}\verb| thus contradiction;|\\ \verb| end;|\\ \verb| thus phi[] or not phi[];|\\ \verb| end;|\\ \verb|end;| \end{flushleft} \subsection{Formal Proof} \begin{flushleft}\footnotesize \xverb{scheme Diaconescu \char`\{ phi[] \char`\} :}\\ \verb| |\xverb{axiom\char`\_of\char`\_choice implies phi[] or not phi[]}\\ \xverb{proof}\\ \verb| |\xverb{assume}\\ \verb|A1: |\xverb{axiom\char`\_of\char`\_choice;}\\ \verb| |\xverb{set A = \char`\{n : n = 0 or (n = 1 \char`\&\ phi[])\char`\};}\\ \verb| |\xverb{set B = \char`\{n : n = 1 or (n = 0 \char`\&\ phi[])\char`\};}\\ \verb| deffunc F(Nat) = $1;|\\ \verb| defpred P[Nat] means $1 = 0 or ($1 = 1 & phi[]);|\\ \verb| {F(n) : P[n]} is Subset of NAT from COMPLSP1:sch 1;|\\ \verb| then reconsider A as Subset of NAT;|\\ \verb| defpred Q[Nat] means $1 = 1 or ($1 = 0 & phi[]);|\\ \verb| {F(n) : Q[n]} is Subset of NAT from COMPLSP1:sch 1;|\\ \verb| then reconsider B as Subset of NAT;|\\ \verb|A2: |\xverb{for x st x in \char`\{A,B\char`\}\ holds ex y st y in x}\\ \verb| proof|\\ \verb| let x;|\\ \verb| assume x in {A,B};|\\ \verb| then|\\ \verb|A3: x = A or x = B by TARSKI:def 2;|\\ \verb| per cases by A3;|\\ \verb| suppose|\\ \verb|A4: x = A;|\\ \verb| take 0;|\\ \verb| thus thesis by A4;|\\ \verb| end;|\\ \verb| suppose|\\ \verb|A5: x = B;|\\ \verb| take 1;|\\ \verb| thus thesis by A5;|\\ \verb| end;|\\ \verb| end|\xsemi\\ \verb| consider f being choice_function such that|\\ \verb|A6: f is extensional by A1,Def3;|\\ \verb| A in {A,B} & B in {A,B} by TARSKI:def 2;|\\ \verb| then (ex y st y in A) & (ex y st y in B) by A2;|\\ \verb| then|\\ \verb|A7: |\xverb{f.A in A \char`\&\ f.B in B}\verb| by Def1|\xverb{;}\\ \verb|A8: |\xverb{f.A = f.B or f.A <> f.B by excluded\char`\_middle\char`\_on\char`\_integers;}\\ \verb| |\xverb{per cases}\verb| by A8|\xsemi\\ \verb| |\xverb{suppose}\\ \verb|A9: |\xverb{f.A = f.B;}\\ \verb| set n = f.A;|\\ \verb|A10: n in A & n in B by A7,A9;|\\ \verb| then|\\ \verb|A11: ex n' st n = n' & (n' = 0 or (n' = 1 & phi[]));|\\ \verb| |\xverb{phi[]}\\ \verb| proof|\\ \verb| per cases by A11;|\\ \verb| suppose|\\ \verb|A12: n = 0;|\\ \verb| ex n' st n = n' & (n' = 1 or (n' = 0 & phi[])) by A10;|\\ \verb| hence thesis by A12;|\\ \verb| end;|\\ \verb| suppose n = 1 & phi[];|\\ \verb| hence thesis;|\\ \verb| end;|\\ \verb| end|\xsemi\\ \verb| |\xverb{hence phi[] or not phi[];}\\ \verb| |\xverb{end;}\\ \verb| |\xverb{suppose}\\ \verb|A13: |\xverb{f.A <> f.B;}\\ \verb| |\xverb{not phi[]}\\ \verb| |\xverb{proof}\\ \verb| |\xverb{assume}\\ \verb|A14: |\xverb{phi[];}\\ \verb| now|\\ \verb| let y;|\\ \verb| hereby|\\ \verb| assume y in A;|\\ \verb| then ex n st y = n & (n = 0 or (n = 1 & phi[]));|\\ \verb| then y = 0 or (y = 1 & phi[]);|\\ \verb| then y = 1 or (y = 0 & phi[]) by A14;|\\ \verb| hence y in B;|\\ \verb| end;|\\ \verb| hereby|\\ \verb| assume y in B;|\\ \verb| then ex n st y = n & (n = 1 or (n = 0 & phi[]));|\\ \verb| then y = 1 or (y = 0 & phi[]);|\\ \verb| then y = 0 or (y = 1 & phi[]) by A14;|\\ \verb| hence y in A;|\\ \verb| end;|\\ \verb| end;|\\ \verb| then |\xverb{A = B by extensionality;}\\ \verb| then |\xverb{f.A = f.B}\verb| by A6,Def2|\xsemi\\ \verb| |\xverb{hence contradiction}\verb| by A13|\xsemi\\ \verb| |\xverb{end;}\\ \verb| |\xverb{hence phi[] or not phi[];}\\ \verb| |\xverb{end;}\\ \xverb{end;} \end{flushleft} \subsection{Mizar Version} 7.0.04 -- 4.04.834 \section{Topology: Open Intervals are Connected} \subsection{Source} Paul Cairns and Jeremy Gow, \emph{Elements of Euclidean and Metric Topology}, online undergraduate course notes from the IMP project. Project web site at \url{}, course notes at \url{} and the frame of this specific proof at \url{}. \subsection{Informal Proof} \begingroup \parindent=0pt \textsf{\textbf{Theorem}} \parskip=.5em Open intervals are connected \begin{tabular}{ll} \textsc{given:}$\,$ & $a,b \in {\cal R}$ \\ \textsc{then:} & The open interval $(a,b)$ is connected \end{tabular} \textsf{\textbf{Proof}} \textsc{sketch:} The proof proceeds by contradiction. Suppose that $(a,b)$ were not connected. Then there would be a pair of non-empty disjoint proper open subsets, $U$, $V$ say, of $(a,b)$ whose union would be $(a,b)$. This implies a ``gap'' so we use the completeness of the real line to show that there can't be a gap. To do this, find a supremum of some interval which must be contained in $U$. Note that there is a small open ball about the supremum wich because $U$ and $V$ are open must be contained wholly within one or other of them. However, in both cases, this leads to a contradiction: if the ball is in $U$ then the ball contains points in $U$ exceeding the supremum; if the ball is in $V$ then there are points in the ball also in $U$ by definition of the supremum. \endgroup \subsection{Formal Proof Sketch: Informal Layout} \begingroup \parindent=0pt \textsf{\textbf{theorem}} \parskip=.5em $(.a,b.)$ is connected \textsf{\textbf{proof}} assume $(.a,b.)$ is not connected; consider $U, V$ being non empty open Subset of \textsc{real}, $u, v$ such that $U \mathop{\raise 1.5pt\hbox{\scriptsize /$\backslash$}\,} V = \{\} \mathrel{\&} U \mathop{\raise 1.5pt\hbox{\scriptsize $\backslash$/}\,} V = (.a,b.) \mathrel{\&} u \mathrel{\mbox{in}} U \mathrel{\&} v \mathrel{\mbox{in}} V$ \& $u < v$; reconsider $X = \big\{ x : (.u,x.) \mathrel{\mbox{\textsf{c}$=$}} U \big\}$ as Subset of \textsc{real}; set $s = \sup X$; per cases; suppose $s \mathrel{\mbox{in}} U$; consider $e$ such that $e > 0 \mathrel{\&} \mbox{Ball}(s,e) \mathrel{\mbox{\textsf{c}$=$}} U$; ex $x$ st $x \mathrel{\mbox{in}} \mbox{Ball}(s,e) \mathrel{\&} x > s$; thus contradiction; suppose $s \mathrel{\mbox{in}} V$; consider $e$ such that $e > 0 \mathrel{\&} \mbox{Ball}(s,e) \mathrel{\mbox{\textsf{c}$=$}} V$; ex $x$ st $x \mathrel{\mbox{in}} \mbox{Ball}(s,e) \mathrel{\&} x \mathrel{\mbox{in}} U$; thus contradiction; \textsc{end;} \endgroup \subsection{Formal Proof Sketch: Formal Layout} \begin{flushleft}\footnotesize \verb|theorem (.a,b.) is connected| \\ \verb|proof| \\ \verb| assume (.a,b.) is not connected;| \\ \verb| consider U,V being non empty open Subset of REAL, u,v such that | \\ \mizerror{4}\verb| U /\ V = {} & U \/ V = (.a,b.) & u in U & v in V & u < v;| \\ \mizerror{4}\verb| reconsider X = { x : (.u,x.) c= U } as Subset of REAL; | \\ \verb| set s = sup X;| \\ \mizerror{4}\verb| per cases;| \\ \verb| suppose s in U;| \\ \mizerror{4}\verb| consider e such that e > 0 & Ball(s,e) c= U;| \\ \mizerror{4}\verb| ex x st x in Ball(s,e) & x > s;| \\ \mizerror{1}\verb| thus contradiction;| \\ \verb| suppose s in V;| \\ \mizerror{4}\verb| consider e such that e > 0 & Ball(s,e) c= V;| \\ \mizerror{4}\verb| ex x st x in Ball(s,e) & x in U;| \\ \mizerror{1}\verb| thus contradiction;| \\ \verb|end;| \end{flushleft} \subsection{Formal Proof} \begin{flushleft}\footnotesize \xverb{theorem (.a,b.) is connected} \\ \xverb{proof} \\ \verb| |\xverb{assume (.a,b.) is not connected;} \\ \verb| then consider U,V being non empty open Subset of REAL such that| \\ \verb|A1: U /\ V = {} & U \/ V = (.a,b.) by Def8;| \\ \verb| consider u such that| \\ \verb|A2: u in U by Def1;| \\ \verb| consider v such that| \\ \verb|A3: v in V by Def1;| \\ \verb| ex U,V being non empty open Subset of REAL, u,v st| \\ \verb| U /\ V = {} & U \/ V = (.a,b.) & u in U & v in V & u < v| \\ \verb| proof| \\ \verb| per cases by AXIOMS:21;| \\ \verb| suppose| \\ \verb|A4: u < v;| \\ \verb| take U,V,u,v;| \\ \verb| thus thesis by A1,A2,A3,A4;| \\ \verb| suppose| \\ \verb|A5: u > v;| \\ \verb| take V,U,v,u;| \\ \verb| thus thesis by A1,A2,A3,A5;| \\ \verb| suppose u = v;| \\ \verb| hence thesis by A1,A2,A3,XBOOLE_0:def 3;| \\ \verb| end;| \\ \verb| then |\xverb{consider U,V being non empty open Subset of REAL, u,v such that} \\ \verb|A6: |\xverb{U /\char`\\\ V = \char`\{\char`\}\ \char`\&\ U \char`\\/ V = (.a,b.) \char`\&\ u in U \char`\&\ v in V \char`\&\ u < v;} \\ \verb| { x : (.u,x.) c= U } c= REAL from Fr_Set0;| \\ \verb| then |\xverb{reconsider X = \char`\{\ x : (.u,x.) c= U \char`\}\ as Subset of REAL;} \\ \verb| (.u,u.) = {} by RCOMP_1:12;| \\ \verb| then (.u,u.) c= U by XBOOLE_1:2;| \\ \verb| then| \\ \verb|A7: u in X;| \\ \verb|A8: for x st x in X holds x <= v| \\ \verb| proof| \\ \verb| let x;| \\ \verb| assume| \\ \verb|A9: x in X & v < x;| \\ \verb|A10: v in (.u,x.) by A6,A9,JORDAN6:45;| \\ \verb| ex x' st x = x' & (.u,x'.) c= U by A9;| \\ \verb| hence thesis by A6,A10,XBOOLE_0:def 3;| \\ \verb| end; | \\ \verb| for x being real number st x in X holds x <= v by A8;| \\ \verb| then reconsider X as non empty bounded_above Subset of REAL| \\ \verb| by A7,SEQ_4:def 1;| \\ \verb| |\xverb{set s = sup X;} \\ \verb| U c= (.a,b.) & V c= (.a,b.) by A6,XBOOLE_1:7;| \\ \verb| then a < u & u <= s & s <= v & v < b| \\ \verb| by A6,A7,A8,JORDAN6:45,SEQ_4:def 4,PSCOMP_1:10;| \\ \verb| then a < s & s < b by AXIOMS:22;| \\ \verb| then| \\ \verb|A11: s in (.a,b.) by JORDAN6:45;| \\ \verb| |\xverb{per cases}\verb| by A6,A11,XBOOLE_0:def 2|\xsemi \\ \verb| |\xverb{suppose s in U;} \\ \verb| then |\xverb{consider e such that} \\ \verb|A12: |\xverb{e > 0 \char`\&\ Ball(s,e) c= U}\verb| by Def7|\xsemi \\ \verb| |\xverb{ex x st x in Ball(s,e) \char`\&\ x > s} \\ \verb| proof| \\ \verb| take x = s + e/2;| \\ \verb| thus x in Ball(s,e) by A12,Th2;| \\ \verb| e/2 > 0 by A12,SEQ_2:3;| \\ \verb| hence thesis by REAL_1:69;| \\ \verb| end|\xsemi \\ \verb| then consider x such that| \\ \verb|A13: x in Ball(s,e) & x > s;| \\ \verb| (.u,x.) c= U| \\ \verb| proof| \\ \verb| let y be set;| \\ \verb| assume| \\ \verb|A14: y in (.u,x.);| \\ \verb| then reconsider y as Real;| \\ \verb|A15: u < y & y < x by A14,JORDAN6:45;| \\ \verb| per cases;| \\ \verb| suppose y < s;| \\ \verb| then consider y' such that| \\ \verb|A16: y' in X & y < y' & y' <= s by Def9;| \\ \verb| y in (.u,y'.) & ex y'' st y' = y'' & (.u,y''.) c= U| \\ \verb| by A15,A16,JORDAN6:45;| \\ \verb| hence thesis;| \\ \verb| suppose y >= s;| \\ \verb| then s in Ball(s,e) & x in Ball(s,e) & s <= y & y <= x| \\ \verb| by A12,A13,A14,Th1,JORDAN6:45;| \\ \verb| then y in Ball(s,e) by Th4;| \\ \verb| hence thesis by A12;| \\ \verb| end;| \\ \verb| then x in X;| \\ \verb| |\xverb{hence contradiction}\verb| by A13,SEQ_4:def 4|\xsemi \\ \verb| |\xverb{suppose s in V;} \\ \verb| then |\xverb{consider e such that} \\ \verb|A17: |\xverb{e > 0 \char`\&\ Ball(s,e) c= V}\verb| by Def7|\xsemi \\ \verb| |\xverb{ex x st x in Ball(s,e) \char`\&\ x in U} \\ \verb| proof| \\ \verb| per cases;| \\ \verb| suppose| \\ \verb|A18: u < s - e/2;| \\ \verb| take x = s - e/2;| \\ \verb| thus x in Ball(s,e) by A17,Th3;| \\ \verb| e/2 > 0 by A17,SEQ_2:3;| \\ \verb| then x < s by REAL_2:174;| \\ \verb| then consider x' such that| \\ \verb|A19: x' in X & x < x' & x' <= s by Def9;| \\ \verb| x in (.u,x'.) & ex x'' st x' = x'' & (.u,x''.) c= U| \\ \verb| by A18,A19,JORDAN6:45;| \\ \verb| hence thesis;| \\ \verb| suppose| \\ \verb|A20: s - e/2 <= u;| \\ \verb| take u;| \\ \verb| s - e/2 in Ball(s,e) & s in Ball(s,e) & s - e/2 <= u & u <= s| \\ \verb| by A7,A17,A20,Th1,Th3,SEQ_4:def 4;| \\ \verb| hence thesis by A6,Th4;| \\ \verb| end|\xsemi \\ \verb| |\xverb{hence contradiction}\verb| by A6,A17,XBOOLE_0:def 3|\xsemi \\ \xverb{end;} \end{flushleft} \subsection{Mizar Version} 6.3.02 -- 3.44.763 \iffalse \section{} \subsection{Source} \subsection{Informal Proof} \subsection{Formal Proof Sketch: Informal Layout} \subsection{Formal Proof Sketch: Formal Layout} \subsection{Formal Proof} \subsection{Mizar Version} 6.1.11 -- 3.33.722 \fi \section{Missing Subjects} \begin{itemize} \item Calculus \item Combinatorics \item Complex Variables \item Differential Equations \item Geometry \item Integration \item Probability Theory \end{itemize} \end{document}