#mathsies

We do a lot of proofs in mathematics. So it's relevant to have some general intuition for the informal notions of how we talk about proofs, so that there is intuition that more precise notions can crystallise around.

While there are more developed and formalised systems of proofs capable of proving things more clearly and precisely that are able to be studied in their own right, the goal here is to introduce some basic ideas and intuitions for proofs. These don't tend to be used individually, but mixed and matched and represent a more general notion of things.

Constructive Proofs

These are their own whole rabbit hole on their own, and there are whole branches of math devoted to this. Most notably, type theory.

One simple and intuitive way you might want to try to prove something is to just provide an example of the thing.

Let's say you want to prove that 4 is even. Well a number is even if it is a multiple of 2. So if we provide "2*2=4", then we have a proof that 4 is even.

"Any even number plus 2 is even."

So it takes an even number x. Since we know that x is even, we have an element y such that 2y=x.

2y+2=x+2

2(y+1)=x+2

Therefore, we found our candidate. If x is a number, and it has a proof y that it is even, x+2 has a proof that it is even, namely y+1.

How can you prove that there exists a number such that the sum of its factors equals its squares? By providing a number: 6, and checking the computation.

This kind of proof is called a Constructive Proof. Proof by construction can be surprisingly strong at times. But it has a handful of large weaknesses.

We often call the provided proof in a constructive proof a witness.

For example: Can you proved a witness to the claim that 64 is a perfect square?

Proof by Exhaustion

This is just a proof where you brute force the thing. For example, you can prove that every number less than ten thousand that ends in 0 is a multiple of ten by manually checking each one. That's a waste of time in that specific case but technically possible.

If you have reduced something to a finite list of things, you can just try all of them. Very often people don't manually do proof by exhaustion, but rather have a computer check a bunch of cases. An example of an exhaustion step was how all the base cases were checked for the four-colouring problem.

There isn't much to say on this one.

Proof by Cases

This is kind of the same thing as proof by exhaustion, where you prove it when one thing is true, and again if it was false. I have listed it separately because it's a special case of proof by exhaustion. You can nest these to get more cases, and thus do arbitrary proof by exhaustion. The vibe is sort of different, though.

An example is the proof that n²+n is always even. There are two cases, n is even, and n is odd. If n is even, it is 2m, and thus n²+n=4m²+2m=2(2m²+m)

And if it is not even, then it is 2m+1, and hence

n²+n=4m²+4m+1 + 2m+ 1= 4m²+6m+2=2(2m²+3m+1)

And hence is even.

Proof by Assumption

Let's say you want to prove that whenever A is true, B is also true. In that case you begin by assuming A, and then you can see what else is true.

For example, if a divides k, then a divides bk for every b.

First you assume that a divides k. That means there is some n such that na=k

And then that means that for every b such:

bna=bk

Hence an also divides bk.

Proof by Contrapositive

This is a special case of proof by assumption. Instead of assuming the premise, you assume the end goal is false, and show the premise must be false.

For example, if n² is even, then n is even.

If n is not even then n=2m+1 for some integer m. And thus n²=4m²+4m+1, which is an even number plus one. n²=2(2m²+2m)+1 hence if n is not even, n² is not even.

Therefore, by contrapositive, n² is even means that n is even.

Proof by Contradiction

Proof by contradiction is where you begin by assuming that something is not true, and you show that that doesn't make any sense.

For example, √2 is irrational:

Let's begin by assuming the opposite, that it is rational. In that case

a/b=√2

And thus there is some smallest pair a and b such that

a²/b²=2

Where this is as simplified as you can make it. But the goal is to show it can still be simplified, because it doesn't make sense if either number is odd.

Or:

a²=2b²

This means a² is even.

And an odd number squared is odd, so a² being even implies a is even. Let's call hald of a as n.

Notably, this means a²=(2n)²=4n², hence

4n²=2b²

And thus

2n²=b²

But that means b is even, or equal to some 2m.

But if a/b is made of two even numbers, then n/m is the same as a/b. n/m is thus a more simplified version of a/b. Which contradicts where we said a/b was the most simplified version. Therefore, there is no such rational a/b.

Hence the square root of 2 is irrational.

Inductive Proof

Proof by induction! This is where I come in! (Ordinals are the structure that induction works on.)

This is where you prove something by showing it is true for some smallest case, and then if it is true for all the smaller cases, then it must be true for the next case.

For example, every natural number is either 2m or 2m+1.

Base case: 0

This follows by construction by the witness m=0

Inductive step: n+1

Now we prove it for any n+1.

If you already know it's true for every number less than n+1, then that means you know n is equal to some 2k or some 2k+1.

Proof by case:

Case: n=2k

Then you have the witness m=k, that shows n+1 equals 2m+1.

Case: n=2k+1

n+1=2k+1+1=2k+2

And thus the witness m=k+1 shows that n+1=2m for some m.

Formal Proof

Language

Since we're going to get into more formal mathematics, it quickly becomes useful to make rules for what's a valid statement to write down and check things about. And one way you can do that is by defining a language.

The above explains it fairly well, a language is just the decision of what's a valid statement to say, it includes valid variables, functions, constants, and relations. It is where you put all your syntax and grammar.

For example, a language for talking about the natural numbers might be:

S,+,*,0,1,2,3,4,5,6,7,8,9,x,y,z,<,=

With rules describing the arity (how many "arguments" something takes in before being valid. 0 has arity 0, because 0 is already a natural number, while + has arity 2, because it need to take in two valid expressions, one in each side, in order to be valid) and order of operations and the fact that you can put digits next to each other. And denoting which of these form "terms" (that being actual elements of what you are talking about.) and which of these form sentences (true false statements, relations checking whether or not something is true, such as < and =)

By convention, the usual logical symbols are allowed to connect sentences, but are not usually considered part of the language. The = sign is conventionally default as well. Those symbols are the underlying symbols that so much of mathematics uses we consider explicitly notating them a waste of time. They are part of the proof system you choose.

You also distinguish between constants and variables. This is because constants need something to be assigned to them, but variables do not matter (it changes nothing to allow them to be assigned, but it's not worth the effort to write an assignment). Variables must always be terms of arity 0.

Notably, at the moment, it is devoid of meaning beyond terms and sentences. We don't know what are variables and what are actual things. This only denotes what are valid ways to construct sentences. S(2)=8 is a valid sentence. 9=1 is valid. +=* is not, since the grammar rules aren't followed.

We usually like more minimal language that we can build syntactic sugar on later. That is, if you can express something in terms of other things in the language, instead of adding it in as a separate symbol, you can just claim that it is a shorthand for some other thing. An example of this is the standard language of sets, which only uses the operation ∈ . x⊂y is defined as a shorthand for "∀z z∈x⇒z∈y ".

Structures

A structure is a universe with an assignment of meaning to the language by providing an explicit construction.

Universes are collections of objects and functions and relations that act on the whole universe cannot take things outside of the universe.

For example, you can look at the natural numbers, and make a universe with one object, with functions that take it to itself, and assign that one object to every term. And assign true to every relation.

In this universe, 3=4, 1+1=0, 4<2, 2<4.

This is not the usual structure of the natural numbers. And not a useful one to think about. So we need a way to specify which structures actually count for what we are talking about.

Theories

A theory is a language, equipped with some sentences that must be guaranteed to be true, called our axioms. They are our wishlist for the structure. For example, the theory of groups can be stated as:

Language:

∙ with arity 2, 1, with arity 1.

a,b,c,x,y,z, x₀,x₁,x₂,x₃,x₄... as our variables, with arity 0. Because we'll want to use variables.

And then some sentences we wish to guarantee are true:

∀a 1∙a=a ⋀ a=a∙1

∀a∀b∀c (a∙b)∙c=a∙(b∙c)

∀a∃b ab=1 ⋀ 1=ba

That is it! The theory of groups! As a shorthand I will label these G0, G1, G2.

We often use the syntactic sugar thar xy is the same as x∙y.

We can use the axioms to figure out other things that also must be true beyond our wishlist. For example, we can prove that 1 must be unique in having the property that it is an identity. Since if we assume that:

xy=x

Then there is some z such that zx=1, hence

z(xy)=zx

And thus

(zx)y=zx

1y=1

y=1

Tadah!

We use thw turnstile symbol, ⊢ to claim that the theory with the sentences on the left of it "entail" the sentences on the right, or, in other words, any structure that satisfies the theory must also satisfy something on the right.

In order to do this formally, we use systems like lk-sequent calculus, or hilbert systems. Or a bunch of others.

I will use Groups to refer to all the axioms of groups packaged up. G0, G1, G2.

Details of the formality may look a bit silly, but I will likely do a later post explaining proof systems much more thoroughly. For now, a glimpse:

First I make all the substitutions I want:

1. ⊢ zx=zx

2. xy=x ⊢ z(xy)=zx

3. xy=x, z(xy)=(zx)y ⊢ (zx)y=zx

4. xy=x, z(xy)=(zx)y, zx=1 ⊢ 1y=1

5. xy=x, z(xy)=(zx)y, zx=1, 1y=y ⊢ y=1

And then I slowly show that most of these substitutions follow from the axioms, mostly by claiming that if I can prove it from specific assumptions about x, y, and z, then I can prove it if those assumptions hold everywhere. (∀-left).

6. xy=x, (zx)y=z(xy), zx=1, 1y=y ⊢ y=1

7. xy=x, ∀a∀b∀c (ab)c=a(bc), zx=1, 1y=y ⊢ y=1

Notably, that's G1, hence:

8. G1, xy=x, zx=1, 1y=y ⊢ y=1

9. G1, xy=x, zx=1, 1y=y ⋀ y=1y ⊢ y= 1

10. G1, xy=x, zx=1, ∀a 1∙a=a ⋀ a=a∙1 ⊢ y=1

But that's G0.

11. G0, G1, xy=x, zx=1 ⊢ y=1

12. G0, G1, xy=x, 1=zx ⊢ y=1

13. G0, G1, xy=x, xz=1 ⋀ 1=zx ⊢ y=11

14. G0, G1, xy=x, ∃b xb=1 ⋀ 1=bx ⊢ y=1

15. G0, G1, xy=x, ∀a∃b ab=1 ⋀ 1=ba ⊢ y=1

But that's G2.

16. G0, G1, G2, xy=x ⊢ y=1

17. Groups, ∃a ay=a ⊢ y=1

18. Groups ⊢ ∃a ay=a ⇒ y=1

Deductrium is an excellent free online game for actually learning about formal proofs. (Particularly in a hilbert system.)

Models

All a model is, is a structure that satisfies a theory. That is, a structure in which the axioms are true.

For example:

A universe 0,1 along with + where 0 is assigned to 1 in the theory, + is assigned to ∙. Under the following construction:

0+0=0

0+1=1

1+0=1

1+1=0

It's quite easy to check your way through G0 and G2. G1 is somewhat tedious.

Therefore that universe under that assignment is a model of the theory of groups.

We can say that this structure "models" the theory of groups. Or that this structure is a group.