On the Irrationality of the Square Root of 2

Abstract

This paper presents a proof of the irrationality of √2 which not only avoids use of paradoxes of implication but also eschews the principle of contraction. The actual theorem proved, in the relevant arithmetic B-sharp, is
¬∃ x ∃ y(x'.x' = 2.y.y)
which is the theorem of natural number theory standardly expressing the irrationality of √2. The key move in the argument is to use provable cases of the law of the excluded middle, P ∨ ¬P, or its close relative P ∨ (P → (0 < 0)) to mimic the effect of contraction.