# How to prove $\sqrt{2}$ is irrational in Type Theory?

Using Intuitionistic Type Theory, how would one go about proving $$\sqrt{2}$$ is irrational?

I read that we can not use law of excluded middle. (So does this mean we cannot use proof by contradiction).

So I assume we want to prove $$\forall a,b\in \mathbb{N^2}: \lnot (a^2 = 2 b^2)$$. In type theory this means we need to find an instance $$P$$ of the type corresponding to the theorem. The type would be something like $$\prod \limits_{a:\mathbb{N}}\prod \limits_{b:\mathbb{N}} NotEqualsQ(Square(a),Times(Two,Square(b))$$. I assume. Then we might have to define these function recursively?

I'm not sure how you would find an instance of this proof.

Negation is defined $$\neg A := A\to \bot$$, the type of naturals $$\mathbb N$$ is defined inductively, and addition and multiplication are defined recursively.
To prove $$\Pi_{a,b:\mathbb N}\neg(a^2=2b^2)$$ we can introduce variables $$a,b:\mathbb N$$ and a proof that $$a^2=2b^2$$ like so: $$a,b:\mathbb N, p : (a^2=2b^2) \vdash \bot$$ and the goal is to construct a term of type $$\bot$$. (Note: I suppose this could be called a "proof by contradiction" because we derive $$\neg A$$ from $$A\vdash\bot$$, but it does not require the excluded middle. A problematic "proof by contradiction" is when we derive $$A$$ from a proof of $$\neg A\vdash \bot$$.)
The idea is to construct $$c,d:\mathbb N$$ such that $$(c^2=2d^2)$$ and $$\neg(2\div d)$$, and then prove that $$2\div d$$, from which you obtain $$\bot$$. Constructing $$c$$ and $$d$$ can be done by splitting cases on whether $$a$$ and $$b$$ are even or odd, assuming you've proved something of the form $$(\forall k.\phi(2k)\times\phi(2k+1))\to(\forall n.\phi(n)).$$