% 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.