Nine Formal Proof Sketches

Freek Wiedijk

University of Nijmegen

Abstract. This note collects the formal proof sketches that I have done.

1 Algebra: Irrationality of \sqrt{2}

1.1 Source

G.H. Hardy and E.M. Wright, An Introduction to the Theory of Numbers. 4th edition, Clarendon Press, Oxford, 1960. Pages 39–40.

1.2 Informal Proof

Theorem 43 (Pythagoras’ theorem). \sqrt{2} is irrational.

The traditional proof ascribed to Pythagoras runs as follows. If \sqrt{2} is rational, then the equation

a^{2} = 2b^{2}  (4.3.1)

is soluble in integers a, b with (a, b) = 1. Hence a^{2} is even, and therefore 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.

1.3 Formal Proof Sketch: Informal Layout

theorem Th43: sqrt 2 is irrational :: Pythagoras’ theorem

proof assume sqrt 2 is rational; consider a, b such that

4 3 1:  aˆ 2 = 2 ∗ bˆ 2

and a, b are relative prime; aˆ 2 is even; a is even; consider c such that a = 2 ∗ c; 4 ∗ cˆ 2 = 2 ∗ bˆ 2; 2 ∗ cˆ 2 = bˆ 2; b is even; thus contradiction; end;

1.4 Formal Proof Sketch: Formal Layout

theorem Th43: sqrt 2 is irrational
proof
 assume sqrt 2 is rational;
 consider a,b such that
4_3_1: a^2 = 2*b^2 and
  *4 a,b are_relative_prime;

*4 a^2 is even;
*4 a is even;
*4 consider c such that a = 2*c;
*4 4*c^2 = 2*b^2;
*4 2*c^2 = b^2;
*4 b is even;
*1 thus contradiction;
end;

1.5 Formal Proof

theorem Th43: sqrt 2 is irrational
\underline{proof}
assume sqrt 2 is rational;
then \underline{consider a,b such that}
A1: b <> 0 and
A2: sqrt 2 = a/b and
A3: \underline{a,b are_relative_prime} by Def1;
A4: b^2 <> 0 by A1,SQUARE_1:73;
2 = (a/b)^2 by A2,SQUARE_1:def 4
 .= a^2/b^2 by SQUARE_1:69;
then
\underline{4_3_1: a^2 = 2*b^2} by A4,REAL_1:43\underline{;}
\underline{a^2 is even} by 4_3_1,ABIAN:def 1\underline{;}
then
A5: \underline{a is even} by PYTHTRIP:2\underline{;}
then \underline{consider c such that}
A6: \underline{a = 2*c} by ABIAN:def 1\underline{;}
A7: \underline{4*c^2 =} (2*2)*c^2
 .= 2^2*c^2 by SQUARE_1:def 3
 .= \underline{2*b^2} by A6,4_3_1,SQUARE_1:68\underline{;}
2*(2*c^2) = (2*2)*c^2 by AXIOMS:16
 .= 2*b^2 by A7;
then \underline{2*c^2 = b^2} by REAL_1:9\underline{;}
then b^2 is even by ABIAN:def 1;
then \underline{b is even} by PYTHTRIP:2\underline{;}
then 2 divides a & 2 divides b by A5,Def2;
then
A8: 2 divides a gcd b by INT_2:33;
a gcd b = 1 by A3,INT_2:def 4;
\underline{hence contradiction} by A8,INT_2:17\underline{;}
\underline{end;}

1.6 Mizar Version

2 Algebra: Infinity of Primes

2.1 Source

The slides of a talk by Herman Geuvers, Formalizing an intuitionistic proof of the Fundamental Theorem of Algebra.

2.2 Informal Proof

Theorem There are infinitely many primes: for every number n there exists a prime p > n

Proof [after Euclid] Given n. Consider k = n! + 1, where n! = 1 · 2 · 3 · . . . · n. Let p be a prime that divides k. For this number p we have p > n: otherwise p ≤ n; but then p divides n!, so p cannot divide k = n! + 1, contradicting the choice of p. QED

2.3 Formal Proof Sketch: Informal Layout

theorem {n : n is prime} is infinite proof for n ex p st p is prime & p > n

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 proof assume p <= n; p divides n!; not p divides n! + 1; thus contradiction; end; end; thus thesis; end;

2.4 Formal Proof Sketch: Formal Layout

theorem {n: n is prime} is infinite
proof
 for n ex p st p is prime & p > n
 proof
  let n;
  set k = n! + 1;
  *4 consider p such that p is prime & p divides k;
  take p;
  *4 thus p is prime;
  thus p > n
  proof
   assume p <= n;

 *4 p divides n!;
 *4 not p divides n! + 1;
 *1 thus contradiction;
end;
end;
*4 thus thesis;
end;

2.5 Formal Proof

theorem {p: p is prime} is infinite
\underline{proof}
A1: \underline{for n ex p st p is prime & p > n}
\underline{proof}
\underline{let n;}
\underline{set k = n! + 1;}
n! > 0 by NEWTON:23;
then n! >= 0 + 1 by NAT_1:38;
then k >= 1 + 1 by REAL_1:55;
then \underline{consider p such that}
A2: \underline{p is prime & p divides k} by INT_2:48\underline{;}
\underline{take p;}
\underline{thus p is prime} by A2\underline{;}
\underline{assume}
A3: \underline{p <= n;}
p <> 0 by A2,INT_2:def 5;
then
A4: \underline{p divides n!} by A3,NAT_LAT:16\underline{;}
p > 1 by A2,INT_2:def 5;
then not p divides 1 by NAT_1:54;
\underline{hence contradiction} by A2,A4,NAT_1:57\underline{;}
\underline{end;}
\underline{thus thesis} from Unbounded(A1)\underline{;}
\underline{end;}

2.6 Mizar Version

6.1.11 – 3.33.722

3 Algebra: Image of Left Unit Element

3.1 Source

Rob Nederpelt, 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.

3.2 Informal Proof

Theorem. Let G be a set with a binary operation · and left unit element e. Let H be a set with binary operation ∗ and assume that ϕ is a homomorphism of G onto H. Then H has a left unit element as well.

Proof. Take e′ = ϕ(e). Let h ∈ H. There is g ∈ G such that ϕ(g) = h. Then

e′ ∗ h = ϕ(e) ∗ ϕ(g) = ϕ(e · g) = ϕ(g) = h,

hence e′ is left unit element of H. □

3.3 Formal Proof Sketch: Informal Layout

let G, H be non empty HGrStr; let e be Element of G such that e is left unit of G; let phi be map of G, H such that phi is homomorphism G, H and phi is onto; thus ex e′ being Element of H st e′ is left unit of H

proof take e′ = phi.e; now let h be Element of H; consider g being Element of G such that phi.g = h; thus

e′ ∗ h = phi.e ∗ phi.g .= phi.(e ∗ g) .= phi.g .= h;

end; hence e′ is left unit of H; end;

3.4 Formal Proof Sketch: Formal Layout

 let G,H be non empty HGrStr;
 let e be Element of G such that e is_left_unit_of G;
 let phi be map of G,H such that
  phi is_homomorphism G,H and phi is onto;
 thus ex e' being Element of H st e' is_left_unit_of H
proof
 take e' = phi.e;
 now
  let h be Element of H;
  *4 consider g being Element of G such that phi.g = h;
  *4*4*4*4 thus e' * h = phi.e * phi.g .= phi.(e * g) .= phi.g .= h;
 end;
 *4 hence e' is_left_unit_of H;
end;

3.5 Formal Proof

 let G,H be non empty HGrStr;

let e be Element of G such that H1: \underline{e is_left_unit_of G;} let phi be map of G,H such that H2: \underline{phi is_homomorphism G,H and}

H3: \underline{phi is onto;}
 thus ex e' being Element of H st e' is_left_unit_of H
\underline{proof}
 take e' = phi.e;
 \underline{now}
  let h be Element of H;
  consider g being Element of G such that
A1: \underline{phi.g = h} by H3,Th1\underline{;}
  \underline{thus e' * h = phi.(e * g)} by A1,H2,Def2
   \underline{.= h} by A1,H1,Def1\underline{;}
 \underline{end;}
 \underline{hence e' is_left_unit_of H} by Def1\underline{;}
\underline{end;}

3.6 Mizar Version

6.1.11 – 3.33.722

4 Algebra: Lagrange’s Theorem

4.1 Source

B.L. van der Waerden, Algebra. 5th edition, Springer-Verlag, Berlin, 1966. Page 26.

4.2 Informal Proof

Zwei Nebenklassen a𝔤, b𝔤 können sehr wohl gleich sein, ohne daß a = b ist. Immer dann nämlich, wenn a^{−1}b in 𝔤 liegt, gilt

b𝔤 = aa^{−1}b𝔤 = a(a^{−1}b𝔤) = a𝔤.

Zwei verschiedene Nebenklassen haben kein Element gemeinsam. Denn wenn die Nebenklassen a𝔤 und b𝔤 ein Element gemein haben, etwa

ag_{1} = bg_{2},

so folgt

g_{1}g_{2}^{−1} = a^{−1}b.

so daß a^{−1}b in 𝔤 liegt; nach dem Vorigen sind also a𝔤 und b𝔤 identisch.

Jedes Element a gehört einer Nebenklasse an, nämlich der Nebenklasse a𝔤. Diese enthält ja sicher das Element ae = a. Nach dem eben Bewiesenen gehört das Element a auch nur einer Nebenklasse an. Wir können demnach jedes Element a als Repräsentanten der a enthaltenden Nebenklass a𝔤 ansehen.

Nach dem vorhergehenden bilden die Nebenklassen eine Klasseneinteilung der Gruppe 𝔊. Jedes Element gehört einer und nur einer Klasse an.

Je zwei Nebenklassen sind gleichmächtig. Denn durch a𝔤 → b𝔤 ist eine eineindeutige Abbildung von a𝔤 auf b𝔤 definiert.

Die Nebenklassen sind, mit Ausnahme von 𝔤 selbst, keine Gruppen; denn eine Gruppe müßte das Einselelement enthalten.

Die Anzahl der verschiedenen Nebenklassen einer Untergruppe 𝔤 in 𝔊 heißt der Index von 𝔤 in 𝔊. Der Index kann endlich oder unendlich sein.

Ist N die als (endlich angenommene) Ordnung von 𝔊, n die von 𝔤, j der Index, so gilt die Relation

(2)  N = jn;

denn 𝔊 ist ja in j Klassen eingeteilt, deren jede n Elemente enthält. Man kann für endliche Gruppen aus (2) den Index j berechnen:

j = \frac{N}{n}

Folge. Die Ordnung einer Untergruppe einer endlichen Gruppe ist ein Teiler der Ordnung der Gesamtgruppe.

4.3 Formal Proof Sketch: Informal Layout

now let a,b; assume a ^{ˆ −1} ∗ b in G; 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) <> {}; consider g_{1}, g_{2} such that

a ∗ g_{1} = b ∗ g_{2};
g_{1} ∗ g_{2} ^{ˆ −1} = a ^{ˆ −1} ∗ b;

a ^{ˆ −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 in H} is a ṗartition 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 for g holds f.(a ∗ g) = b ∗ g; f is bijective; 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

’2’:  N = j ∗ n;  end;

thus card G divides card H; 4.4 Formal Proof Sketch: Formal Layout

now
 let a,b;
 assume a^-1*b in G;
 *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) <> {};
  *4 consider g1,g2 such that a*g1 = b*g2;
  *4 g1*g2^-1 = a^-1*b;
  *4 a^-1*b in G;
  *4 thus a*G = b*G;
 end;
 *4 thus thesis;
end;
for a holds a in a*G
proof
 let a;
 *4 a*e(G) = a;
 *4 thus thesis;
end;
*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
  *4 for g holds f.(a*g) = b*g;
 *4 f is bijective;
 *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
*4 '2': N = j*n;
end;
*4 thus card G divides card H;

4.5 Formal Proof

A1: \underline{now}
 \underline{let a,b;}
 \underline{assume}
A2: \underline{a^-1*b in G;}

\underline{thus b*G =} e(H)*b*G by GROUP_1:def 5
.= \underline{a*a^-1*b*G} by GROUP_1:def 6
.= a*(a^-1*b)*G by GROUP_1:def 4
\underline{.= a*(a^-1*b*G)} by GROUP_2:127
.= a*(carr G) by A2,GROUP_2:136
\underline{.= a*G} by GROUP_2:def 13\underline{;}
\underline{end;}
A3: \underline{for a,b st a*G <> b*G holds (a*G) /\ (b*G) = \{\}}
\underline{proof}
\underline{let a,b;}
\underline{now}
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;
\underline{consider g1} such that
A6: x = a*g1 by A5,Th5;
consider \underline{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: \underline{a*g1 =} a*g1G by Th2
 .= \underline{b*g2} by A6,A7,Th2\underline{;}
g1G*g2G^-1 = g1*g2G^-1 by Th3
 .= \underline{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
 .\underline{= a^-1*b} by GROUP_1:def 5\underline{;}
then \underline{a^-1*b in G} by STRUCT_0:def 5\underline{;}
\underline{hence a*G = b*G} by A1\underline{;}
\underline{end;}
hence thesis;
\underline{end;}
A9: \underline{for a holds a in a*G}
\underline{proof}
\underline{let a;}
\underline{a*e(G) =} a*e(H) by Th2,GROUP_2:53
.= \underline{a} by GROUP_1:def 5\underline{;}
hence thesis;
\underline{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;
\underline{\{a*G : a in H\} is a_partition of H} by A11\underline{;}
A15: \underline{for a,b holds card(a*G) = card(b*G)}
\underline{proof}
\underline{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;
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);

 \underline{for g holds f.(a*g) = b*g} by A18\underline{;}
 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\underline{;}
 \underline{hence thesis} by EUCLID_7:3\underline{;}
\underline{end;}
set 'Index' = card {a*G : a in H};
'Index' = card X;
then reconsider 'Index' as natural number;
\underline{now}
 let N such that
A23: \underline{N = card H;}
 let n such that
A24: \underline{n = card G;}
 let j such that
A25: \underline{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;
 \underline{hence N = j*n} by A23,A25,A26,Th1\underline{;}
\underline{end;}
then card H = 'Index'*card G;
\underline{hence card G divides card H} by INT_1:def 9\underline{;}

4.6 Mizar Version

5 Analysis: successor has no fixed point

5.1 Source Fairouz Kamareddine, Manuel Maarek and J.B. Wells, MathLang: experiencedriven development of a new mathematical language, draft. Page 11.

Quoted from: Edmund Landau, Foundations of Analysis. Translated by F. Steinhardt, Chelsea, 1951.

5.2 Informal Proof Theorem 2

x′ ≠ x

Proof Let 𝔐 be the set of all x for which this holds true. I) By Axiom 1 and Axiom 3,

1′ ≠ 1;

therefore 1 belongs to 𝔐. II) If x belongs to 𝔐, then

x′ ≠ x,

and hence by Theorem 1,

(x′)′ ≠ x′,

so that x′ belongs to 𝔐. By Axiom 5, 𝔐 therefore contains all the natural numbers, i.e. we have for each x that

x′ ≠ x.

5.3 Formal Proof Sketch: Informal Layout Theorem 2:

x ′ <> x

proof set 𝔐 = {y : y ′ <> y}; I: now

1 ′ <> 1

by Axiom 1, Axiom 3; hence 1 in 𝔐; end; II: now let x; assume x in 𝔐; then

x ′ <> x;

then

(x ′)′ <> x ′

by Theorem 1; hence x ′ in 𝔐; end; for x holds x in 𝔐 by Axiom 5; hence

x ′ <> x;  end;

5.4 Formal Proof Sketch: Formal Layout

Theorem_2: x ' <> x
proof
set M = {y : y ' <> y};
I: now
 1 ' <> 1 by Axiom_1, Axiom_3;
 *4 hence 1 in M;
end;
II: now let x;
 assume x in M;
 *4 then x ' <> x;
 then (x ')' <> x ' by Theorem_1;
 hence x ' in M;
end;
*4 for x holds x in M by Axiom_5;
*4 hence x ' <> x;
end;

5.5 Formal Proof

Theorem_2: x ' <> x
\underline{proof}
\underline{set M = \{y : y ' <> y\};}
\underline{I: now}
 \underline{1 ' <> 1 by Axiom_3;}
 hence 1 in M by Axiom_1;
\underline{end;}
\underline{now let x;}
 assume x in M;
 \underline{then} ex y st x = y & \underline{y ' <> y;}
 \underline{then (x ')' <> x '} by Axiom_4\underline{;}
 hence x ' in M;
\underline{end;}
then \underline{x in M by} I,\underline{Axiom_5;}
then ex y st x = y & y ' <> y;
\underline{hence x ' <> x;}
\underline{end;}

5.6 Mizar Version

6.4.01 – 3.60.795

6 Linear Algebra: Linear Independence

6.1 Source

Jean Gallier, Basics of Algebra and Analysis For Computer Science. Published at

⟨http://www.cis.upenn.edu/^{∼}jean/gbook.html⟩, University of Pennsylvania,

2001. Page 16.

6.2 Informal Proof

Lemma 2.1. Given a linearly independent family (u_{i})_{i∈I} of elements of a vector space E, if v ∈ E is not a linear combination of (u_{i})_{i∈I}, then the family (u_{i})_{i∈I}∪_{k} (v) obtained by adding v to the family (u_{i})_{i∈I} is linearly independent (where k ∉ I).

Proof. Assume that μv + ∑_{i∈I} λ_{i}u_{i} = 0, for any family (λ_{i})_{i∈I} of scalars in K. If μ ≠ 0, then μ has an inverse (because K is a field), and thus we have v = − ∑_{i∈I}(μ^{−1}λ_{i})u_{i}, showing that v is a linear combination of (u_{i})_{i∈I} and contradicting the hypothesis. Thus, μ = 0. But then, we have ∑_{i∈I} λ_{i}u_{i} = 0, and since the family (u_{i})_{i∈I} is linearly independent, we have λ_{i} = 0 for all i ∈ I. □

6.3 Formal Proof Sketch: Informal Layout

theorem Lem21: u is linearly-independent & not v in Lin(u) implies u \/ {v} is linearly-independent

proof assume u is linearly-independent & not v in Lin(u); assume u \/ {v} is linearly-dependent; consider m being Element of K, l being Linear Combination of u such that m∗v +Sum(l) = 0.E; now assume m <> 0.K; v = −m”∗Sum(l); v in Lin(u); thus contradiction; end; m = 0.K; Sum(l) = 0.E; Carrier(l) = {}; thus contradiction; end;

6.4 Formal Proof Sketch: Formal Layout

theorem Lem21:
 u is linearly-independent & not v in Lin(u) implies
  u \/ {v} is linearly-independent
proof
 assume u is linearly-independent & not v in Lin(u);
 assume u \/ {v} is linearly-dependent;
 consider m being Element of K,
  l being Linear_Combination of u such that
   *4 m*v + Sum(l) = 0.E;
 now
  assume m <> 0.K;
  *4 v = -m"*Sum(l);
  *4 v in Lin(u);
  *1 thus contradiction;
 end;
 *4 m = 0.K;
 *4 Sum(l) = 0.E;
 *4 Carrier(l) = {};
 *1 thus contradiction;
end;

6.5 Formal Proof

theorem Lem21:
u is linearly-independent & not v in Lin(u) implies
 u \/ {v} is linearly-independent
\underline{proof}
\underline{assume}
A1: \underline{u is linearly-independent & not v in Lin(u);}
given l' being Linear_Combination of u \/ {v} such that
A2: Sum(l') = 0.E & Carrier(l') <> {};
\underline{consider} m' being Linear_Combination of \{v\},
 l being Linear_Combination of u such that
A3: l' = m' + l by Th2;
set m = m'.v;
A4: \underline{m*v + Sum(l) =} Sum(m') + Sum(l) by VECTSP_6:43
 .= \underline{0.E} by A2,A3,VECTSP_6:77\underline{;}
A5: \underline{now}
 \underline{assume}
A6: \underline{m <> 0.K;}
 m*v = -Sum(l) by A4,RLVECT_1:def 10;
 then \underline{v =} m"*(-Sum(l)) by A6,VECTSP_1:67
  .= \underline{-m"*Sum(l)} by VECTSP_1:69\underline{;}
 then
A7: v = (-m")*Sum(l) by VECTSP_1:68;
 Sum(l) in Lin(u) by VECTSP_7:12;
 \underline{hence contradiction} by A1,A7,VECTSP_4:29\underline{;}
\underline{end;}
\underline{Sum(l) =} 0.E + Sum(l) by VECTSP_1:7
 .= \underline{0.E} by A4,A5,VECTSP_1:59\underline{;}
then
A8: \underline{Carrier(l) = \{\}} by A1,VECTSP_7:def 1\underline{;}
now
 let x be set;
A9: Carrier(m') c= {v} by VECTSP_6:def 7;
 not v in Carrier(m') by A5,VECTSP_6:20;
 hence not x in Carrier(m') by A9,TARSKI:def 1;
end;
then Carrier(m') = {} by BOOLE:def 1;
then Carrier(l) \/ Carrier(m') = {} by A8;
then Carrier(l') c= {} by A3,VECTSP_6:51;
\underline{hence contradiction} by A2,BOOLE:30\underline{;}
\underline{end;}

6.6 Mizar Version

7 Mathematical Logic: Newman’s Lemma

7.1 Source

Henk Barendregt, The Lambda Calculus: Its Syntax and Semantics. North Holland, 1984. Page 58.

7.2 Informal Proof

3.1.25. Proposition. For notions of reduction one has

SN ∧ WCR ⇒ CR

Proof. By SN each term R-reduces to an R-nf. It suffices to show that this R-nf is unique. Call M ambiguous if M R-reduces to two distinct R-nf’s. For such M one has M →_{R} M′ with M′ ambiguous (use WCR, see figure 3.3). Hence by SN ambiguous terms do not exist.

[figure: M; M; M′; or; M′; M_{1}; M_{3}; M_{2}; M_{1}; M_{2}]

fig. 3.3.

7.3 Formal Proof Sketch: Informal Layout

theorem 3 1 25:

R is SN & R is WCR implies R is CR

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} <> M_{2}; now now let M such that ambiguous[M]; thus ex M′ st M ---> M′ & ambiguous[M′]

proof consider M_{1}, M_{2} such that M -->> M_{1} & M -->> M_{2} & M_{1} <>
M_{2}; per cases; suppose not ex M′ st M ---> M′ & M′ -->> M_{1} &
M′ -->> M_{2}; consider M′ such that M ---> M′ & M′ -->> M_{1}; consider
M′′ such that M ---> M′′ & M′′ -->> M_{2}; consider M′′′ such that
M′ -->> M′′′ & M′′ -->> M′′′; consider M_{3} such that M′′′ -->> M_{3};
take M′; thus thesis; suppose ex M′ st M ---> M′ & M′ -->> M_{1} &
M′ -->> M_{2}; consider M′ such that M ---> M′ & M′ -->> M_{1} &
M′ -->> M_{2}; take M′; thus thesis; end;

end; thus not ex M st ambiguous[M]; end; thus thesis; end; 7.4 Formal Proof Sketch: Formal Layout

theorem 3_1_25:
R is SN & R is WCR implies R is CR
proof
assume that R is SN and R is WCR;
*4 for M ex M1 st M reduces_to M1;
(for M,M1,M2 st M reduces_to M1 & M reduces_to M2 holds M1 = M2)
 *4 implies R is CR;
defpred ambiguous[Term of R] means
 ex M1,M2 st $1 reduces_to M1 & $1 reduces_to M2 & M1 <> M2;
now
 now
  let M such that ambiguous[M];
  thus ex M' st M ---> M' & ambiguous[M']
  proof :: begin fig 3.3
   *4 consider M1,M2 such that M -->> M1 & M -->> M2 & M1 <> M2;
   per cases;
   suppose not ex M' st M ---> M' & M' -->> M1 & M' -->> M2;
    *4 consider M' such that M ---> M' & M' -->> M1;
    *4 consider M'' such that M ---> M'' & M'' -->> M2;
    *4 consider M''' such that M' -->> M''' & M'' -->> M''';
    *4 consider M3 such that M''' -->> M3;
    take M';
    *4,4 thus thesis;
   suppose ex M' st M ---> M' & M' -->> M1 & M' -->> M2;
    *4 consider M' such that M ---> M' & M' -->> M1 & M' -->> M2;
    take M';
    *4,4 thus thesis;
  end; :: end fig 3.3
 end;
 *4 thus not ex M st ambiguous[M];
end;
*4 thus thesis;
end;

7.5 Formal Proof

\underline{theorem 3_1_25:}
R is SN & R is WCR implies R is CR
\underline{proof}
\underline{assume that}
A1: \underline{R is SN and}
A2: \underline{R is WCR;}
A3: R is WN by A1,Th9;
then \underline{for M ex M1 st M reduces_to M1} by Def10;
A4: \underline{(for M,M1,M2 st M reduces_to M1 & M reduces_to M2 holds M1 = M2)}
 implies R is CR
proof
 assume

A5: for M,M1,M2 st M reduces_to M1 & M reduces_to M2 holds M1 = M2;
  let M,M',M'';
  assume
A6: M -->> M' & M -->> M'';
  consider M1 such that
A7: M' -->> M1 by A3,Def10;
  consider M2 such that
A8: M'' -->> M2 by A3,Def10;
  M -->> M1 & M -->> M2 by A6,A7,A8,Th6;
  then M' -->> M1 & M'' -->> M1 by A5,A7,A8;
  hence thesis;
 end\underline{;}
 defpred ambiguous[Term of R] means
  ex M1,M2 st $1 reduces_to M1 & $1 reduces_to M2 & M1 <> M2;
A9: \underline{now}
A10: \underline{now}
   let M such that
A11: \underline{ambiguous[M];}
   thus ex M' st M ---> M' & ambiguous[M']
   proof :: begin fig 3.3
    consider M1,M2 such that
A12: \underline{M -->> M1 & M -->> M2 & M1 <> M2} by A11\underline{;}
    \underline{per cases;}
    \underline{suppose}
A13:  \underline{not ex M' st M ---> M' & M' -->> M1 & M' -->> M2;}
     M1 is_nf & M2 is_nf by Def9;
     then
A14:  M <> M1 & M <> M2 by A12,Th8;
     then \underline{consider M' such that}
A15:  \underline{M ---> M' & M' -->> M1} by A12,Th7\underline{;}
     consider M'' such that
A16:  \underline{M ---> M'' & M'' -->> M2} by A12,A14,Th7\underline{;}
     consider M''' such that
A17:  \underline{M' -->> M''' & M'' -->> M'''} by A2,A15,A16,Def11\underline{;}
     consider M3 such that
A18:  \underline{M''' -->> M3} by A3,Def10\underline{;}
     \underline{take M';}
     M' -->> M3 & M'' -->> M3 by A17,A18,Th6;
     then M' -->> M1 & M' -->> M3 & M1 <> M3 by A13,A15,A16;
     \underline{hence thesis} by A15\underline{;}
    suppose ex M' st M ---> M' & M' -->> M1 & M' -->> M2;
     then \underline{consider M' such that}
A19:  \underline{M ---> M' & M' -->> M1 & M' -->> M2;}
     \underline{take M';}
     \underline{thus thesis} by A12,A19\underline{;}
   end; :: end fig 3.3
  \underline{end;}
  \underline{thus not ex M st ambiguous[M]} from SN_induction1(A1,A10)\underline{;}
 \underline{end;}
 \underline{thus thesis} by A4,A9\underline{;}

\underline{end;}

7.6 Mizar Version

6.1.11 – 3.33.722

8 Mathematical Logic: Diaconescu’s Theorem

8.1 Source

Michael Beeson, Foundations of Constructive Mathematics. Springer-Verlag, 1985.

8.2 Informal Proof

1.1 Theorem (Diaconescu [1975]). The axiom of choice implies the law of excluded middle, using separation and extensionality.

Proof. Let a formula ϕ be given; we shall derive ϕ ∨ ¬ϕ. Let A = {n ∈ N : n = 0 ∨ (n = 1 & ϕ)}. Let B = {n ∈ N : n = 1 ∨ (n = 0 & ϕ)}. Then ∀ x ∈ {A, B} ∃ y ∈ N (y ∈ x). Suppose f is a choice function, so that f(A) ∈ A and f(B) ∈ B. We have f(A) = f(B) ∨ f(A) ≠ f(B), since the values are integers. If f(A) = f(B) then ϕ, so ϕ ∨ ¬ϕ. If f(A) ≠ f(B), then ¬ϕ can be derived: suppose ϕ. Then A = B by extensionality, so f(A) = f(B), contradiction. Hence in either case ϕ ∨ ¬ϕ. □

8.3 Formal Proof Sketch: Informal Layout

scheme Diaconescu {phi []} : axiom of choice implies phi [] or not phi [] proof assume axiom of choice; set A = {n : n = 0 or (n = 1 & phi [])}; set

B = {n : n = 1 or (n = 0 & 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 & 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; end;

8.4 Formal Proof Sketch: Formal Layout

scheme Diaconescu :: 1975
 { phi[] } : axiom_of_choice implies phi[] or not phi[]
proof
 assume axiom_of_choice;
 set A = {n : n = 0 or (n = 1 & phi[])};
 set B = {n : n = 1 or (n = 0 & phi[])};
 *4 for x st x in {A,B} holds ex y st y in x;

consider f being choice_function such that
 *4 f is extensional;
*4,4 f.A in A & 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;
 *4 phi[];
 thus phi[] or not phi[];
end;
suppose f.A <> f.B;
 not phi[]
 proof
  assume phi[];
  *4 A = B by extensionality;
  *4 f.A = f.B;
  *1 thus contradiction;
 end;
 thus phi[] or not phi[];
end;
end;

8.5 Formal Proof

scheme Diaconescu {phi[] }:
axiom_of_choice implies phi[] or not phi[]
\underline{proof}
\underline{assume}
A1: \underline{axiom_of_choice;}
set A = {n : n = 0 or (n = 1 & phi[])};
set B = {n : n = 1 or (n = 0 & phi[])};
deffunc F(Nat) = $1;
defpred P[Nat] means $1 = 0 or ($1 = 1 & phi[]);
{F(n) : P[n]} is Subset of NAT from COMPLSP1:sch 1;
then reconsider A as Subset of NAT;
defpred Q[Nat] means $1 = 1 or ($1 = 0 & phi[]);
{F(n) : Q[n]} is Subset of NAT from COMPLSP1:sch 1;
then reconsider B as Subset of NAT;
A2: \underline{for x st x in \{A,B\} holds ex y st y in x}
proof
 let x;
 assume x in {A,B};
 then
A3: x = A or x = B by TARSKI:def 2;
 per cases by A3;
 suppose
A4: x = A;
  take 0;
  thus thesis by A4;
 end;
 suppose

A5: x = B;
   take 1;
   thus thesis by A5;
  end;
 end\underline{;}
 consider f being choice_function such that
A6: f is extensional by A1,Def3;
 A in {A,B} & B in {A,B} by TARSKI:def 2;
 then (ex y st y in A) & (ex y st y in B) by A2;
 then
A7: \underline{f.A in A & f.B in B} by Def1\underline{;}
A8: \underline{f.A = f.B or f.A <> f.B by excluded_middle_on_integers;}
 \underline{per cases} by A8\underline{;}
 \underline{suppose}
A9: \underline{f.A = f.B;}
  set n = f.A;
A10: n in A & n in B by A7,A9;
  then
A11: ex n' st n = n' & (n' = 0 or (n' = 1 & phi[]));
  \underline{phi[]}
  proof
   per cases by A11;
   suppose
A12: n = 0;
    ex n' st n = n' & (n' = 1 or (n' = 0 & phi[])) by A10;
    hence thesis by A12;
   end;
   suppose n = 1 & phi[];
    hence thesis;
   end;
  end\underline{;}
  hence phi[] or not phi[];
 \underline{end;}
 \underline{suppose}
A13: \underline{f.A <> f.B;}
  \underline{not phi[]}
  \underline{proof}
   \underline{assume}
A14: \underline{phi[];}
   now
    let y;
    hereby
     assume y in A;
     then ex n st y = n & (n = 0 or (n = 1 & phi[]));
     then y = 0 or (y = 1 & phi[]);
     then y = 1 or (y = 0 & phi[]) by A14;
     hence y in B;
    end;
    hereby
     assume y in B;

     then ex n st y = n & (n = 1 or (n = 0 & phi[]));
     then y = 1 or (y = 0 & phi[]);
     then y = 0 or (y = 1 & phi[]) by A14;
     hence y in A;
    end;
   end;
   then \underline{A = B by extensionality;}
   then \underline{f.A = f.B} by A6,Def2\underline{;}
   \underline{hence contradiction} by A13\underline{;}
  \underline{end;}
  hence phi[] or not phi[];

 \underline{end;} \underline{end;}

8.6 Mizar Version

7.0.04 – 4.04.834

9 Topology: Open Intervals are Connected

9.1 Source

Paul Cairns and Jeremy Gow, Elements of Euclidean and Metric Topology, online undergraduate course notes from the IMP project. Project web site at ⟨http:

//www.uclic.ucl.ac.uk/imp/⟩, course notes at ⟨http://www.uclic.ucl.ac.
uk/topology/⟩ and the frame of this specific proof at ⟨http://www.uclic.ucl.
ac.uk/topology/ConnectedInterval.html⟩.

9.2 Informal Proof

Theorem

Open intervals are connected

given: a, b ∈ R
then: The open interval (a, b) is connected

Proof

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.

9.3 Formal Proof Sketch: Informal Layout

theorem

(.a, b.) is connected

proof

assume (.a, b.) is not connected; consider U, V being non empty open Subset of real, u, v such that U ^{/\} V = {} & U ^{\/} V = (.a, b.) & u in U & v in V & u < v; reconsider X = {x : (.u, x.) c= U} as Subset of real; set s = sup X; per cases; suppose s in U; consider e such that e > 0 & Ball(s, e) c= U; ex x st x in Ball(s, e) & x > s; thus contradiction; suppose s in V; consider e such that e > 0 & Ball(s, e) c= V; ex x st x in Ball(s, e) & x in U; thus contradiction;

end;

9.4 Formal Proof Sketch: Formal Layout

theorem (.a,b.) is connected
proof
assume (.a,b.) is not connected;
consider U,V being non empty open Subset of REAL, u,v such that
 *4 U /\ V = {} & U \/ V = (.a,b.) & u in U & v in V & u < v;
*4 reconsider X = { x : (.u,x.) c= U } as Subset of REAL;
set s = sup X;
*4 per cases;
suppose s in U;
 *4 consider e such that e > 0 & Ball(s,e) c= U;
 *4 ex x st x in Ball(s,e) & x > s;
 *1 thus contradiction;
suppose s in V;
 *4 consider e such that e > 0 & Ball(s,e) c= V;
 *4 ex x st x in Ball(s,e) & x in U;
 *1 thus contradiction;
end;

9.5 Formal Proof

theorem (.a,b.) is connected
\underline{proof}
assume (.a,b.) is not connected;
then consider U,V being non empty open Subset of REAL such that
A1: U /\ V = {} & U \/ V = (.a,b.) by Def8;
consider u such that
A2: u in U by Def1;
consider v such that
A3: v in V by Def1;
ex U,V being non empty open Subset of REAL, u,v st
 U /\ V = {} & U \/ V = (.a,b.) & u in U & v in V & u < v
proof

 per cases by AXIOMS:21;
 suppose
A4: u < v;
  take U,V,u,v;
  thus thesis by A1,A2,A3,A4;
 suppose
A5: u > v;
  take V,U,v,u;
  thus thesis by A1,A2,A3,A5;
 suppose u = v;
  hence thesis by A1,A2,A3,XBOOLE_0:def 3;
end;
then \underline{consider U,V being non empty open Subset of REAL, u,v such that}
A6: \underline{U /\ V = \{\} & U \/ V = (.a,b.) & u in U & v in V & u < v;}
{ x : (.u,x.) c= U } c= REAL from Fr_Set0;
then \underline{reconsider X = \{ x : (.u,x.) c= U \} as Subset of REAL;}
(.u,u.) = {} by RCOMP_1:12;
then (.u,u.) c= U by XBOOLE_1:2;
then
A7: u in X;
A8: for x st x in X holds x <= v
proof
 let x;
 assume
A9: x in X & v < x;
A10: v in (.u,x.) by A6,A9,JORDAN6:45;
 ex x' st x = x' & (.u,x'.) c= U by A9;
 hence thesis by A6,A10,XBOOLE_0:def 3;
end;
for x being real number st x in X holds x <= v by A8;
then reconsider X as non empty bounded_above Subset of REAL
 by A7,SEQ_4:def 1;
set s = sup X;
U c= (.a,b.) & V c= (.a,b.) by A6,XBOOLE_1:7;
then a < u & u <= s & s <= v & v < b
 by A6,A7,A8,JORDAN6:45,SEQ_4:def 4,PSCOMP_1:10;
then a < s & s < b by AXIOMS:22;
then
A11: s in (.a,b.) by JORDAN6:45;
\underline{per cases} by A6,A11,XBOOLE_0:def 2\underline{;}
suppose s in U;
 then \underline{consider e such that}
A12: \underline{e > 0 & Ball(s,e) c= U} by Def7\underline{;}
 ex x st x in Ball(s,e) & x > s
 proof
  take x = s + e/2;
  thus x in Ball(s,e) by A12,Th2;
  e/2 > 0 by A12,SEQ_2:3;
  hence thesis by REAL_1:69;
 end\underline{;}

then consider x such that
A13: x in Ball(s,e) & x > s;
(.u,x.) c= U
proof
let y be set;
assume
A14: y in (.u,x.);
then reconsider y as Real;
A15: u < y & y < x by A14,JORDAN6:45;
per cases;
suppose y < s;
then consider y' such that
A16: y' in X & y < y' & y' <= s by Def9;
y in (.u,y'.) & ex y'' st y' = y'' & (.u,y''.) c= U
 by A15,A16,JORDAN6:45;
hence thesis;
suppose y >= s;
then s in Ball(s,e) & x in Ball(s,e) & s <= y & y <= x
 by A12,A13,A14,Th1,JORDAN6:45;
then y in Ball(s,e) by Th4;
hence thesis by A12;
end;
then x in X;
\underline{hence contradiction} by A13,SEQ_4:def 4\underline{;}
suppose s in V;
then \underline{consider e such that}
A17: \underline{e > 0 & Ball(s,e) c= V} by Def7\underline{;}
ex x st x in Ball(s,e) & x in U
proof
per cases;
suppose
A18: u < s - e/2;
take x = s - e/2;
thus x in Ball(s,e) by A17,Th3;
e/2 > 0 by A17,SEQ_2:3;
then x < s by REAL_2:174;
then consider x' such that
A19: x' in X & x < x' & x' <= s by Def9;
x in (.u,x'.) & ex x'' st x' = x'' & (.u,x''.) c= U
 by A18,A19,JORDAN6:45;
hence thesis;
suppose
A20: s - e/2 <= u;
take u;
s - e/2 in Ball(s,e) & s in Ball(s,e) & s - e/2 <= u & u <= s
 by A7,A17,A20,Th1,Th3,SEQ_4:def 4;
hence thesis by A6,Th4;
end\underline{;}
\underline{hence contradiction} by A6,A17,XBOOLE_0:def 3\underline{;}
\underline{end;}

9.6 Mizar Version

6.3.02 – 3.44.763

10 Missing Subjects

– Calculus

– Combinatorics

– Complex Variables

– Differential Equations – Geometry

– Integration

– Probability Theory