PROOFS AND DEFINITIONS USING ELLIPSIS
━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
Notes for a talk at the Stockholm PhD student seminar in theoretical philosophy
June 4, 2018
Anders Lundstedt
anders.lundstedt@philosophy.su.se
§0 Preliminaries
────────────────
─ ℕ = the natural numbers = {0,1,2,...}.
─ ℕ⁺ = the positive natural numbers = {1,2,3,...}.
─ "x", "y" and "z" will denote natural numbers and "i", "j", "k", "m", "n"
will denote positive natural numbers, when the context does not dictate
otherwise.
─ [n,m] = {i in ℕ : n ≤ i ≤ m} = {n,n+1,...,m-1,m}.
─ Binary operators associate to the left, unless otherwise noted.
─ If f : A → B and A' ⊆ A then f↓A' is the restriction of f to A', that is,
f↓A' : A' → B is given by
f↓A'(a) := f(a).
─ For functions f : A→B' and g : B→C with B' ⊆ B their composition A→C is
denoted "gf":
f g gf
A → B' ⊆ B → C = A → C.
Composition associates to the right:
hgf = h(gf).
∗∗
§1 Introduction
───────────────
To get things going, let us look at two definitions of exponentiation and for
each definition a corresponding proof of the identity xⁿxᵐ = xⁿ⁺ᵐ. The first
definition uses ellipsis (three dots──"...") while the second definition is by
recursion. For simplicity we define xⁿ only for x in ℕ and n in ℕ⁺, thus
avoiding a separate case for x⁰ in the first definition, which would introduce
unnecessary complications.
∗∗
Definition 1.1.
–⁻ : ℕ×ℕ⁺→ℕ,
xⁿ := x⋅x⋅⋅⋅x (n factors).
∗∗
Definition 1.2.
–⁻ : ℕ×ℕ⁺→ℕ,
x¹ := x,
xⁿ⁺¹ := xⁿ⋅x.
∗∗
Examples.
─ Computing 2³ using Definition 1.1:
2³ = 2⋅2⋅2 (by Definition 1.1).
─ Computing 2³ using Definition 1.2:
2³ = 2²⁺¹
= 2²⋅2 (by Definition 1.2)
= 2¹⁺¹⋅2
= 2¹⋅2⋅2 (by Definition 1.2)
= 2⋅2⋅2 (by Definition 1.2).
∗∗
Fact 1.3. Definition 1.1 and Definition 1.2 define the same function.
Proof. See Appendix A. □
∗∗
Fact 1.4.
xⁿ⋅xᵐ = xⁿ⁺ᵐ.
Proof 1.4.1. Using Definition 1.1:
xⁿ⋅xᵐ = (x⋅x⋅⋅⋅x)⋅(x⋅x⋅⋅⋅x) (by Definition 1.1)
n factors m factors
= x⋅x⋅⋅⋅x (n+m factors)
= xⁿ⁺ᵐ (by Definition 1.1). □
Proof 1.4.2. Using Definition 1.2 and induction on m:
─ Base case: We want to prove xⁿx¹ = xⁿ⁺¹. This is easy:
xⁿ⋅x¹ = xⁿ⋅x (by Definition 1.2)
= xⁿ⁺¹ (by Definition 1.2).
─ Induction step: The induction hypothesis is
(IH) xⁿ⋅xᵐ = xⁿ⁺ᵐ
and we want to prove
xⁿ⋅xᵐ⁺¹ = xⁿ⁺ᵐ⁺¹.
We have
xⁿ⋅xᵐ⁺¹ = xⁿ⋅xᵐ⋅x (by Definition 1.2)
= xⁿ⁺ᵐ⋅x (by (IH))
= xⁿ⁺ᵐ⁺¹ (by Definition 1.2). □
∗∗
Here are some points regarding Definitions 1.1 and 1.2 and regarding
Proofs 1.4.1 and 1.4.2:
─ Definition 1.1, which is formulated using ellipsis, is easier to
understand than Definition 1.2, which is formulated by recursion. One does
not have to understand recursion to understand Definition 1.1. Indeed,
Definition 1.1 (possibly amended with a separate treatment of the special
case x⁰) is the definition found in schoolbooks and school children are
expected to understand it before they get to learn about recursion.
Definition 1.1 is also the one currently found in the Wikipedia article on
exponentiation.
─ Proof 1.4.1, which uses the ellipsis-formulated Definition 1.1, is easier
to understand than Proof 1.4.2, which is an induction proof using the
recursion-formulated Definition 1.2. One does not have to understand the
principle of mathematical induction to understand Proof 1.4.1. Indeed,
Proof 1.4.1 is the proof found in schoolbooks and school children are
expected to understand it before they get to learn about mathematical
induction.
─ Proof 1.4.2 presupposes that we know what we want to prove. This is not
the case for Proof 1.4.1, which would work just as well to answer the
question "What is another useful expression for xⁿ⋅xᵐ?"
─ The above points often generalize. It is very common that ellipsis
formulations are simpler to understand and simpler to reason about and
with.
∗∗
Given the above it seems that we would prefer definitions and proofs formulated
using ellipsis instead of recursion and induction. This is indeed the case in
non-formalized mathematics, where ellipsis usage is widespread in both
definitions and proofs. This is the case even in logic, consider e.g. common
formulations such as
φ(x₁,...,xₙ),
∀x₁⋅⋅⋅∀xₙ.φ(x₁,...,xₙ).
∗∗
Compared to non-formalized mathematics, ellipsis is not at all as common in
formalized mathematics. Definition by recursion and proof by induction are often
used instead. For example, if one wants to use first-order arithmetic to reason
about exponentiation, the straightforward way to go is to add a function symbol
and the defining recursive equations. For another example, the standard library
of the popular proof assistant Coq defines exponentiation recursively. The
corresponding proof of xⁿ⋅xᵐ = xⁿ⁺ᵐ is a proof by induction that, at least on
the surface, does not resemble Proof 1.4.1.
∗∗
It might not be too surprising that ellipsis is less common in popular
formalisms, such as first-order logic and type theory, since these have no
obvious syntactic counterpart to the ellipsis. This is in sharp contrast with
recursively defined functions──these can be almost literally translated to both
first-order logic and to type theory (for example, in the first-order logic case
just add needed function symbols to the language and their defining equations as
axioms).
∗∗
My starting point then is the question
How should ellipsis be formalized?
There are good reasons for trying to answer this question:
─ It is not obvious how ellipsis should be formalized.
─ A formalization of ellipsis would make it easier to formalize
non-formalized mathematics where ellipsis is used.
─ A formalization of ellipsis would dispense with the possible worry that
there is something fishy with ellipsis usage in mathematics. One might
have the worry that some ellipsis usages are non-formalizable, or even
that some ellipsis usages do not even produce valid definitions and
proofs.
─ A formalization of ellipis would allow us to study ellipsis mathematics
metamathematically. In particular, we would be able to make precise
comparisons of induction proofs and ellipsis proofs. I would expect this
to lead to some novel and surprising insights.
∗∗
I do not aim to give a definitive answer to how ellipsis should be formalized.
I only want to show that at least some common usages of ellipsis are indeed
formalizable. I will do this by providing formalization-friendly definitions and
proofs that do capture the spirit of corresponding definitions and proofs that
are formulated using ellipsis.
∗∗
I do not claim any novelty in my formalization-friendly reformulations (nor do I
claim that there is nothing novel). I will use a "fold" function and in computer
science, the relation between "fold" functions and ellipsis definitions is
already well known.
∗∗
The structure of these notes are as follows.
─ In §2 I will look at proofs of the result
(xⁿ)ᵐ = xⁿᵐ.
─ In §3 I will consider the function σ : ℕ⁺→ℕ such that σ(n) is the sum of
the first n positive integers. I will look at definitions of σ and proofs
of the result that
2⋅σ(n) = n⋅(n+1).
─ In §4 I will provide another definition of σ and another proof of the
above result. I think this definition and this proof should be seen as
formalization-friendly reformulations of the corresponding ellipsis
versions in §3.
─ In §5 I dispense with some of the worries we might have that there is
something fishy about ellipsis usage in mathematics. I do this by
showing how the formalizing-friendly formulations in §4 are close in
spirit to the ellipsis formulations in §3.
∗∗
§2 More exponentiation
──────────────────────
Fact 2.1.
(xⁿ)ᵐ = xⁿᵐ.
Proof 2.1.1. Using Definition 1.1:
(xⁿ)ᵐ = xⁿ⋅xⁿ⋅xⁿ (m factors) (by Definition 1.1)
= (x⋅x⋅⋅⋅x)⋅(x⋅x⋅⋅⋅x)⋅⋅⋅(x⋅x⋅⋅⋅x) (by Definition 1.1)
n factors n factors n factors
m factors
= x⋅x⋅⋅⋅x (n⋅m factors)
= xⁿᵐ (by Definition 1.1). □
Proof 2.1.2. Using Definition 1.2 and induction on m:
─ Base case: We want to prove (xⁿ)¹ = x¹ⁿ. This is immediate from
Definition 1.2.
─ Induction step: The induction hypothesis is
(IH) (xⁿ)ᵐ = xⁿᵐ
and we want to prove
(xⁿ)ᵐ⁺¹ = xⁿ⁽ᵐ⁺¹⁾.
We have
(xⁿ)ᵐ⁺¹ = (xⁿ)ᵐ⋅xⁿ (by Definition 1.2)
= xⁿᵐ⋅xⁿ (by (IH))
= xⁿᵐ⁺ⁿ (by Fact 1.4)
= xⁿ⁽ᵐ⁺¹⁾. □
∗∗
§3 The sum of initial segments of the positive integers
───────────────────────────────────────────────────────
Let σ : ℕ⁺→ℕ be the function such that σ(n) is the sum of the first n positive
integers. Here are a definition of σ formulated using ellipsis and a definition
of σ formulated using recursion.
∗∗
Definition 3.1.
σ : ℕ⁺ → ℕ
σ(n) := 1+2+⋅⋅⋅+n.
∗∗
Definition 3.2.
σ : ℕ⁺ → ℕ
σ(1) := 1,
σ(n+1) := σ(n)+n+1.
∗∗
Examples.
─ Computing σ(3) using Definition 3.1:
σ(3) = 1+2+3 (by Definition 3.1)
= 6.
─ Computing σ(3) using Definition 3.2:
σ(3) = σ(2+1)
= σ(2)+2+1 (by Definition 3.2)
= σ(1+1)+3
= σ(1)+1+1+3 (by Definition 3.2)
= σ(1)+2+3
= 1+2+3 (by Definition 3.2)
= 6.
∗∗
Fact 3.3. Definitions 3.1 and 3.2 define the same function.
Proof. See Appendix A. □
∗∗
Fact 3.4.
2⋅σ(n) = n⋅(n+1).
Proof 3.4.1. Using Definition 3.1 we have
(1) σ(n) = 1 + 2 + ⋅⋅⋅ + (n-1) + n (by Definition 3.1),
(2) σ(n) = n + (n-1) + ⋅⋅⋅ + 2 + 1 (by reversing the
order in (1)),
(3) 2⋅σ(n) = (1+n) + (2+(n-1)) + ⋅⋅⋅ + ((n-1)+2) + (n+1) (by summing
same-column terms
from (1) and (2))
= (n+1)+(n+1)+⋅⋅⋅+(n+1) (n terms)
= n⋅(n+1). □
Proof 3.4.2. Using Definition 3.2 and induction on n:
─ Base case: We want to prove 2⋅σ(1) = 1⋅(1+1). This is easy:
2⋅σ(1) = 2⋅1 (by Definition 3.2)
= 1⋅(1+1).
─ Induction step: The induction hypothesis is
(IH) 2⋅σ(n) = n⋅(n+1)
and we want to prove
2⋅σ(n+1) = (n+1)⋅(n+2).
We have
2⋅σ(n+1) = 2⋅(σ(n)+n+1) (by Definition 3.2)
= 2⋅σ(n)+2⋅(n+1)
= n⋅(n+1)+2⋅(n+1) (by (IH))
= (n+1)⋅(n+2). □
∗∗
§4 Using tuples to capture ellipsis reasoning
─────────────────────────────────────────────
In the following I will limit myself to tuples of natural numbers, but the
definitions and facts not mentioning tuples and functions specific to the
natural numbers should immediately generalize.
∗∗
Using ellipsis notation we can write
"⟨x₁,...,xₙ⟩"
to denote a tuple of length n whose element at position i is xᵢ. Several
definitions without ellipsis are possible. I will use the following.
∗∗
Definition 4.1. The set ℕⁿ of ∗tuples (of natural numbers) of length n∗ is the
set of functions [1,n]→ℕ.
∗∗
Notation. "tᵢ" and "t[i]" will mean "t(i)" when t is a tuple.
∗∗
Definition 4.1 relates to the ellipsis notation of tuples by
for all tuples t of length n: t = ⟨t₁,...,tₙ⟩.
Since the point of this section is to avoid ellipsis I will not rely on ellipsis
notation in definitions and proofs. (I will still use ellipsis notation for some
purely illustrative purposes.)
∗∗
Examples.
─ The identity function on [1,n] is in ℕⁿ. (Ellipsis notation: ⟨1,...,n⟩.)
─ The [1,3]→ℕ function i↦4-i is in ℕ³. (Alternative notation: ⟨3,2,1⟩.)
─ For any x in ℕ, the constant [1,n] function –↦x is in ℕⁿ. (Ellipsis
notation: ⟨x,...,x⟩.)
─ For any t in ℕⁿ⁺¹ and any m in [1,n], t↓[1,m] is in ℕₘ. (Ellipsis
notation: ⟨t₁,...,tₘ⟩.)
─ For any f : ℕ⁺→ℕ, f↓[1,n] is in ℕⁿ. (Ellipsis notation: ⟨f(1),...,f(n)⟩.)
─ For any f : [1,n]→[1,n] and any t in ℕⁿ, tf is in ℕⁿ. (Ellipsis notation:
⟨t[f(1)],...,t[f(n)]⟩.)
∗∗
Definition 4.2.
─ ιₙ is the identity function on [1,n].
─ The ℕⁿ×ℕ→ℕⁿ⁺¹ function t,x↦t::x is defined by
t::x(i) := t(i) if i ≤ n,
t::x(n+1) := x.
∗∗
Remark. In ellipsis notation, Definition 4.2 would become
─ ιₙ = ⟨1,...,n⟩,
─ ⟨x₁,...,xₙ⟩::xₙ₊₁ = ⟨x₁,...,xₙ,xₙ₊₁⟩.
∗∗
Notation.
─ "⟨x⟩", for x in ℕ, abbreviates the tuple –↦x in ℕ¹.
─ "f(u,v)", for f : ℕ×ℕ→ℕ and u and v in ℕⁿ, abbreviates the tuple
i↦f(u(i),v(i)) in ℕⁿ.
∗∗
Remark. In ellipsis notation, the last notation above becomes
f(⟨u₁,...,uₙ⟩,⟨v₁,...,vₙ⟩) = ⟨f(u₁,v₁),...,f(uₙ,vₙ)⟩.
∗∗
Fact 4.3. For all t in ℕⁿ⁺¹:
t = t↓[1,n]::tₙ₊₁.
Proof. See Appendix A. □
∗∗
By Fact 4.3, every tuple u in ℕⁿ⁺¹ is of the form v::x. This allows us to define
functions on ℕⁿ by recursion on n, as the following definition illustrates.
∗∗
Definition 4.4. The functions lfₙ : (ℕ×ℕ→ℕ)×ℕⁿ→ℕ are defined by
lf₁(∗,⟨x⟩) := x,
lfₙ₊₁(∗,t::x) := lfₙ(∗,t)∗x.
∗∗
Remark. With ellipsis notation and using parentheses to emphasize the
associativity, Definition 4.4 becomes
lfₙ(∗,⟨x₁,x₂,x₃,...,xₙ⟩) := ((x₁∗x₂)∗x₃)∗⋅⋅⋅∗xₙ.
∗∗
Remark. "lf" is short for "left fold", which is the common computer science name
for this function. The operation ∗ associates to the left in the ellipsis
version of the left fold definition. There is also the "right fold", in the
ellipsis definition of which the operation ∗ associates to the right.
∗∗
Example. Computing lf₃(+,ι₃):
lf₃(+,ι₃) = lf₃(+,ι₃↓[1,2]::ι₃[3]) (by Fact 4.3)
= lf₃(+,ι₂::3)
= lf₂(+,ι₂)+3 (by Definition 4.4)
= lf₂(+,ι₂↓[1,1]::ι₂[2])+3 (by Fact 4.3)
= lf₂(+,ι₁::2)+3
= lf₁(+,ι₁)+2+3 (by Definition 4.4)
= lf₁(+,⟨1⟩)+2+3
= 1+2+3 (by Definition 4.4)
= 6.
∗∗
Fact 4.5. For all associative and commutative ∗:
lfₙ(∗,u)∗lfₙ(∗,v) = lfₙ(∗,u∗v).
Proof. See Appendix A. □
∗∗
Remark. In ellipsis notation, the equation in Fact 4.5 becomes
(u₁∗⋅⋅⋅∗uₙ)∗(v₁∗⋅⋅⋅∗vₙ) = (u₁∗v₁)∗⋅⋅⋅∗(uₙ∗vₙ).
∗∗
Fact 4.6. For all commutative and associative ∗ and all bijections
b : [1,n]→[1,n]:
lfₙ(∗,tb) = lfₙ(∗,t).
Proof. See Appendix A. □
∗∗
Remark. In ellipsis notation, the equation in Fact 4.6 becomes
t₁∗⋅⋅⋅∗tₙ = tb(1)∗⋅⋅⋅∗tb(n).
∗∗
Definition 4.7.
σ(n) := lfₙ(+,ιₙ).
∗∗
Remark. In ellipsis notation, Definition 4.7 becomes
σ(n) := ιₙ[1]+⋅⋅⋅+ιₙ[n],
which unfolds to
σ(n) = 1+⋅⋅⋅+n.
∗∗
Fact 4.8. Definition 4.7 defines the same function as Definitions 3.1 and 3.2.
Proof. See Appendix A. □
∗∗
Fact 4.9.
lfₙ(+,–↦x) = n⋅x.
Proof. The proof depends on how we define multiplication. One way is to simply
define multiplication on ℕ⁺×ℕ by the above equation. □
∗∗
Fact 4.10.
2⋅σ(n) = n⋅(n+1).
Proof. Let revₙ be the "reverse order" bijection [1,n]→[1,n], that is, revₙ is
defined by
revₙ(i) := n+1-i,
by which revₙ is a bijection. For all i in [1,n] we have
(ιₙ+ιₙrevₙ)(i) = ιₙ(i)+ιₙrevₙ(i)
= ιₙ(i)+ιₙ(n+1-i)
= i+n+1-i
= n+1.
Thus
(∗) ιₙ+ιₙrevₙ = –↦n+1.
Then
2⋅σ(n) = 2⋅lfₙ(+,ιₙ) (by Definition 4.7)
= lfₙ(+,ιₙ)+lfₙ(+,ιₙ)
= lfₙ(+,ιₙ)+lfₙ(+,ιₙrevₙ) (by Fact 4.6)
= lfₙ(+,ιₙ+ιₙrevₙ) (by Fact 4.5)
= lfₙ(+,–↦n+1) (by (∗))
= n⋅(n+1) (by Fact 4.9). □
∗∗
§5 Conclusion
─────────────
Let us compare the proof of Fact 4.10 with Proof 3.4.1. First, let us just
simply slightly reorganize Proof 3.4.1 (the reader may want to verify that the
structure of the proof remains the same):
2⋅σ(n) = σ(n) + σ(n)
= 1 + 2 + ⋅⋅⋅ + (n-1) + n
+ 1 + 2 + ⋅⋅⋅ + (n-1) + n (by Definition 3.1)
= 1 + 2 + ⋅⋅⋅ + (n-1) + n (by reversing the
+ n + (n-1) + ⋅⋅⋅ + 2 + 1 lower sum)
= (1+n) + (2+(n-1)) + ⋅⋅⋅ + ((n-1)+2) + (n+1) (by summing terms in
same column)
= (n+1)+(n+1)+⋅⋅⋅+(n+1) (n terms)
= n⋅(n+1).
∗∗
Now let us look at how closely Proof 3.4.1 is mirrored in the proof of
Fact 4.10:
─ The equation
1 + 2 + ⋅⋅⋅ + (n-1) + n
+ 1 + 2 + ⋅⋅⋅ + (n-1) + n
= 1 + 2 + ⋅⋅⋅ + (n-1) + n (by reversing the
+ n + (n-1) + ⋅⋅⋅ + 2 + 1 lower sum)
corresponds to
lfₙ(+,ιₙ)+lfₙ(+,ιₙ) = lfₙ(+,ιₙ)+lfₙ(+,ιₙrevₙ) (by Fact 4.6).
─ The equation
1 + 2 + ⋅⋅⋅ + (n-1) + n
+ n + (n-1) + ⋅⋅⋅ + 2 + 1
= (1+n) + (2+(n-1)) + ⋅⋅⋅ + ((n-1)+2) + (n+1) (by summing
same-column terms)
corresponds to
lfₙ(+,ιₙ)+lfₙ(+,ιₙrevₙ) = lfₙ(+,ιₙ+ιₙrevₙ) (by Fact 4.5).
─ The equation
(1+n) + (2+(n-1)) + ⋅⋅⋅ + ((n-1)+2) + (n+1)
= (n+1)+(n+1)+⋅⋅⋅+(n+1) (n terms)
corresponds to
lfₙ(+,ιₙ+ιₙrevₙ) = lfₙ(+,–↦n+1) (by (∗)).
─ The equation
(n+1)+⋅⋅⋅+(n+1) = n⋅(n+1)
n terms
corresponds to
lfₙ(+,–↦n+1) = n⋅(n+1) (by Fact 4.9).
∗∗
Given the above, I think it should be clear that §4 provides a
formalization-friendly version of the ellipsis formulations in §3. In
particular, we have a proof that do not use any ellipsis but still closely
mirrors the ellipsis proof in §3.
∗∗
I claim that, using similar techniques, Definition 1.1 and Proofs 1.4.1 and
2.1.1 can be reformulated in a formalization-friendly way. This is something I
leave for future work.
∗∗
To show that the formulation in §4 really is formalization-friendly, one could
construct an actual formalization of it. I think proof assistants based on
dependent type theory, for example Coq or Agda, would be a suitable choice for
this. For now, I leave this for future work.
∗∗
Appendix A: Some proofs
───────────────────────
Fact 1.3. Definition 1.1 and Definition 1.2 define the same function.
Proof. Let us denote exp according to Definition 1.1 by exp₁ and let us denote
exp according to Definition 1.2 by exp₂. We need to prove
for all x in ℕ and all n in ℕ⁺: exp₁(x,n) = exp₂(x,n).
We prove this by induction on n.
─ Base case: We want to prove exp₁(x,1) = exp₂(x,1). This follows directly
from the definitions:
exp₁(x,1) = x (by Definition 1.1)
= exp₂(x,1) (by Definition 1.2).
─ Induction step: The induction hypothesis is
(IH) exp₁(x,n) = exp₂(x,n)
and we want to prove
exp₁(x,n+1) = exp₂(x,n+1).
We have
exp₁(x,n+1) = x⋅x⋅⋅⋅x (by Definition 1.1)
n+1 factors
= (x⋅x⋅⋅⋅x)⋅x
n factors
= exp₁(x,n)⋅x (by Definition 1.1)
= exp₂(x,n)⋅x (by (IH))
= exp₂(x,n+1) (by Definition 1.2).
∗∗
Fact 3.3. Definitions 3.1 and 3.2 define the same function.
Proof. Let us denote σ according to Definition 3.1 by σ₁ and let us denote σ
according to Definition 3.2 by σ₂. We need to prove
for all n in ℕ⁺: σ₁(n) = σ₂(n).
We prove this by induction on n.
─ Base case: We want to prove σ₁(1) = σ₂(1). This follows directly from the
definitions:
σ₁(1) = 1 (by Definition 3.1)
= σ₂(1) (by Definition 3.2).
─ Induction step: The induction hypothesis is
(IH) σ₁(n) = σ₂(n)
and we want to prove
σ₁(n+1) = σ₂(n+1).
We have
σ₁(n+1) = 1+2+⋅⋅⋅+n+n+1 (by Definition 2.1)
= σ₁(n)+n+1 (by Definition 2.1)
= σ₂(n)+n+1 (by (IH))
= σ₂(n+1) (by Definition 2.2). □
∗∗
Fact 4.3. For all t in ℕⁿ⁺¹:
t = t↓[1,n]::tₙ₊₁.
Proof.
t = i ↦ t(i)
= i ↦ (t↓[1,n](i) if i ≤ n otherwise tₙ₊₁)
= t↓[1,n]::tₙ₊₁ (by Definition 4.2). □
∗∗
Fact 4.5. For all associative and commutative ∗:
lfₙ(∗,u)∗lfₙ(∗,v) = lfₙ(∗,u∗v).
Proof. Induction on n.
─ Base case: We want to prove
for all u and v in ℕ¹: lf₁(∗,u)∗lf₁(∗,v) = lf₁(∗,u∗v).
We have
lf₁(∗,u)∗lf₁(∗,v) = lf₁(∗,⟨u₁⟩)∗lf₁(∗,⟨v₁⟩)
= u₁∗v₁ (by Definition 4.4)
= lf₁(∗,⟨u₁∗v₁⟩) (by Definition 4.4)
= lf₁(∗,u∗v).
─ Induction step: The induction hypothesis is
(IH) for all u and v in ℕⁿ: lfₙ(∗,u)∗lfₙ(∗,v) = lfₙ(∗,u∗v)
and we want to prove
for all u and v in ℕⁿ⁺¹: lfₙ₊₁(∗,u)∗lfₙ₊₁(∗,v) = lfₙ₊₁(∗,u∗v).
We have
lfₙ₊₁(∗,u)∗lfₙ₊₁(∗,v) = (lfₙ(∗,u↓[1,n])∗uₙ₊₁)∗(lfₙ(∗,v↓[1,n])∗vₙ₊₁)
(by Fact 4.3 and Definition 4.4)
= (lfₙ(∗,u↓[1,n])∗lfₙ(∗,v↓[1,n]))∗(uₙ₊₁∗vₙ₊₁)
(by associativity and commutativity)
= (lfₙ(∗,u↓[1,n]∗v↓[1,n])∗(uₙ₊₁∗vₙ₊₁)
(by (IH))
= (lfₙ(∗,(u∗v)↓[1,n])∗(u∗v)ₙ₊₁
= lfₙ₊₁(∗,u∗v)
(by Fact 4.3 and Definition 4.4). □
∗∗
Fact 4.6. For all commutative and associative ∗ and all bijections
b : [1,n]→[1,n]:
lfₙ(∗,tb) = lfₙ(∗,t).
Proof. Induction on n using n = 1 and n = 2 as base cases.
─ Base case n = 1: Trivial since the bijection i↦i is the unique function
[1,1]→[1,1].
─ Base case n = 2: We want to prove
for all bijections b : [1,2]→[1,2] and all t in ℕ²:
lf₂(∗,tb) = lf₂(∗,t).
There are two different bijections b : [1,2]→[1,2].
─ Case b = i↦i: Trivial.
─ Case b = i↦3-i: We have
lf₂(∗,tb)
= lf₂(∗,(tb)↓[1,1])∗tb(2) (by Fact 4.3 and Definition 4.4)
= lf₂(∗,⟨t₂⟩)∗t₁
= t₂∗t₁ (by Definition 4.4)
= t₁∗t₂ (by commutativity)
= lf₂(∗,⟨t₁⟩)∗t₂ (by Definition 4.4)
= lf₂(∗,t↓[1:1])∗t₂
= lf₂(∗,t) (by Fact 4.3 and Definition 4.4).
─ Induction step n = m+2: The induction hypothesis is
(IH) for all bijections b : [1,m+1]→[1,m+1] and all t in ℕᵐ⁺¹:
lfₘ₊₁(∗,tb) = lfₘ₊₁(∗,t).
We want to prove
for all bijections b : [1,m+2]→[1,m+2] and all t in ℕᵐ⁺²:
lfₘ₊₂(∗,tb) = lfₘ₊₂(∗,t).
─ Case b(m+2) = m+2: Then b↓[1,m+1] is a bijection [1,m+1]→[1,m+1] and
(∗) (tb)↓[1,m+1] = t↓[1,m+1]b↓[1,m+1].
Thus
lfₘ₊₂(∗,tb)
= lfₘ₊₁(∗,(tb)↓[1,m+1])∗tb(m+2) (by Fact 4.3 and
Definition 4.4)
= lfₘ₊₁(∗,t↓[1,m+1]b↓[1,m+1])∗tb(m+2) (by (∗))
= lfₘ₊₁(∗,t↓[1,m+1])∗tb(m+2) (by (IH))
= lfₘ₊₁(∗,t↓[1,m+1])∗tₘ₊₂
= lfₘ₊₂(∗,t) (by Fact 4.3 and
Definition 4.4).
─ Case b(m+2) ≠ m+2: Let i be the unique number in [1,m+1] such that
b(i) = m+2. Using ellipsis, for illustrative purposes, we then have
lfₘ₊₂(∗,tb)
= lfₘ₊₂(∗,⟨tb(1),...,tb(i),...,tb(m+1),tb(m+2)⟩)
= lfₘ₊₁(∗,⟨tb(1),...,tb(i),...,tb(m+1)⟩)∗tb(m+2)
= lfₘ₊₁(∗,⟨tb(1),...,tb(m+1),...,tb(i)⟩)∗tb(m+2)
(by (IH))
= lfₘ(∗,⟨tb(1),...,tb(m+1),...,tb(m)⟩)∗tb(i)∗tb(m+2)
= lfₘ(∗,⟨tb(1),...,tb(m+1),...,tb(m)⟩)∗tb(m+2)∗tb(i)
(by associativity and commutativity)
= lfₘ₊₁(∗,⟨tb(1),...,tb(m+1),...,tb(m),tb(m+2)⟩)∗tb(i)
= lfₘ₊₁(∗,⟨t₁,...,tₘ₊₁⟩)∗tb(i)
(by (IH))
= lfₘ₊₁(∗,⟨t₁,...,tₘ₊₁⟩)∗tₘ₊₂
= lfₘ₊₂(∗,⟨t₁,...,tₘ₊₂⟩)
= lfₘ₊₂(∗,t).
We formulate the above without ellipsis as follows. Define
b' : [1,m+1]→[1,m+1] by
b'(j) := j if j ≠ i and j ≠ m+1,
b'(i) := m+1,
b'(m+1) := i.
Define b'' : [1,m+1]→[1,m+1] by
b''(j) := bb'(j) if j ≠ m+1,
b''(m+1) := b(m+2).
Then b' and b'' are bijections [1,m+1]→[1,m+1]. We have
lfₘ₊₂(∗,tb)
= lfₘ₊₁(∗,(tb)↓[1,m+1])∗tb(m+2)
(by Fact 4.3 and Definition 4.4)
= lfₘ₊₁(∗,(tb)↓[1,m+1]b')∗tb(m+2)
(by (IH))
= lfₘ₊₁(∗,tbb')∗tb(m+2)
= lfₘ(∗,(tbb')↓[1,m])∗tbb'(m+1)∗tb(m+2)
(by Fact 4.3 and Definition 4.4)
= lfₘ(∗,(tbb')↓[1,m])∗tb(m+2)∗tbb'(m+1)
(by associativity and commutativity)
= lfₘ(∗,(tb'')↓[1,m])∗tb''(m+1)∗tbb'(m+1)
(by definition of b'')
= lfₘ₊₁(∗,(tb'')↓[1,m+1])∗tbb'(m+1)
(by Fact 4.3 and Definition 4.4)
= lfₘ₊₁(∗,t↓[1,m+1]b'')∗tbb'(m+1)
= lfₘ₊₁(∗,t↓[1,m+1])∗tbb'(m+1)
(by (IH))
= lfₘ₊₁(∗,t↓[1,m+1])∗tb(i)
= lfₘ₊₁(∗,t↓[1,m+1])∗tₘ₊₂
= lfₘ₊₂(∗,t)
(by Fact 4.3 and Definition 4.4). □
∗∗
Fact 4.8. Definition 4.7 defines the same function as Definitions 3.1 and 3.2.
Proof. We have already shown that Definitions 3.1 and 3.2 define the same
function so it suffices to show that Definitions 3.2 and 4.7 define the same
function. Let us denote σ according to Definition 3.2 by σ₂ and let us denote σ
according to Definition 4.7 by σ₃. We want to prove
for all n in ℕ⁺: σ₂(n) = σ₃(n).
We prove this by induction on n.
─ Base case: We want to prove σ₂(1) = σ₃(1). This follows directly from
definitions:
σ₂(1) = 1 (by Definition 3.2)
= lf₁(+, ⟨1⟩) (by Definition 4.4)
= lf₁(+, ι₁) (by Definition 4.2)
= σ₃(1) (by Definition 4.7).
─ Induction step: The induction hypothesis is
(IH) σ₂(n) = σ₃(n)
and we want to prove
σ₂(n+1) = σ₃(n+1).
We have
σ₂(n+1) = σ₂(n)+n+1 (by Definition 3.2)
= σ₃(n)+n+1 (by (IH))
= lfₙ(+, ιₙ)+n+1 (by Definition 4.7)
= lfₙ₊₁(+, ιₙ::(n+1)) (by Definition 4.4)
= lfₙ₊₁(+, ιₙ₊₁) (by Definition 4.2)
= σ₃(n+1) (by Definition 4.7). □
∗∗