% Prove that sqrt(2) is irrational (when this is fed into prover9). % This file was created by David A. Wheeler, and is % inspired by the Otter proof from Larry Wos, % by Michael Beeson and William McCune, % that was published in "The Seventeen Provers of the World" % compiled by Freek Wiedijk. (http://www.cs.ru.nl/~freek/comparison/). % This version's notation is much easier to read, because it uses capabilities % such as infix operators, implies (->), and iff (<->). % Usage: % prover9 -f sqrt2.in > sqrt2.out % This proof presumes numbers only range over positive integers (1,2,...). % It's a proof by contradiction; the assumptions are entered, and prover9 % shows that there is a contradiction. formulas(assumptions). 1*x = x. % identity x*1 = x. x*(y*z) = (x*y)*z. % associativity x*y = y*x. % commutativity (x*y = x*z) -> y = z. % cancellation (0 is not allowed, so x!=0). % Now let's define divides(x,y), which is true iff x divides y. % For example, divides(2,6) is true because 2*3=6. % The older Otter proof used the clausal form: % -divides(x,y) | (x*f(x,y)) = y. % x*z != y | divides(x,y). % but I find this clausal form rather confusing. I think expressing it % using traditional first-order logic is MUCH clearer as an input. % Prover9 will immediately convert this into the clausal form: divides(x,y) <-> (exists z x*z = y). divides(2,x*y) -> (divides(2,x) | divides(2,y)). % If 2 divides x*y, it divides x or y. 2 != 1. % Original author almost forgot this. % Now, assert that we can have a rational fraction for sqrt(2), reduced % to lowest terms (we can't, and that's the point of the proof): a*a = (2*(b*b)). % a/b = sqrt(2), so a^2 = 2 * b^2. (x != 1) -> -(divides(x,a) & divides(x,b)). % a/b is in lowest terms end_of_list.