The irrational to irrational is rational example.

[andrejbauer]

In section 5.5 around theorem 5.1, there is a discussion about how the LEM proof of "irrational to irrational is rational" is a bit unsatisfying because we do not know which numbers in particular give "irrational to irrational is rational". To bolster this point we could point out that there is a simple proof which gives explicit numbers and is intuitionistically valid: take a = \sqrt{3} and b = \log_3(4). Then a^b = 3^(\log_3(4) * 0.5) = 4^0.5 = 2. I hope I got that right.

[rzach]

Thanks!

Thanks! I think the point of the example is that it is supposed to be unsatisfying, hence to motivate why one might be critical of LEM.

I'll leave this open for when we add a separate chapter on Intuitionistic Logic, which will happen eventually. It does add the extra issue of proving/explaining why \log_3 (4) is irrational.

For reference, this concerns file https://github.com/OpenLogicProject/OpenLogic/blob/master/first-order-logic/beyond/intuitionistic-logic.tex by @avigad

[andrejbauer]

I understand it's supposed to be unsatisfying. I am suggesting that we bolster the fact that it is unsatisfying by mentioning that we could easily provide an explicit example. This makes the proof even more unsatisfying. And if I am not mistaken, section 5.5 is about intuitionistic logic. Are you planing to expand on it?

[andrejbauer]

The proof that \log_3(4) is irrational is exactly as complicated as the proof that \sqrt{2} is irrational: suppose \log_3(4) = p/q with p and q integers. Then 3^(\log_3(4)) = 3^(p/q), hence 4 = 3^(p/q) hence 4^q = 3^p, hence p = q = 0, which won't do.

[rzach]

Yes I'm hoping to add a part on intuitionistic logic.

[rzach]

fixed with commit https://github.com/OpenLogicProject/OpenLogic/commit/1eaee3bd1ae98825623c12d6847a977dc6a32dfc