% This Prover9 input file can be used to prove that Frink's
% basis for Boolean algebra is correct.
% A first-order proof was presented by Padmanabhan in 1981
% (Algebra Universalis).
set(auto).
set(fold_eq). % introduce defined operations (join)
assign(new_constants, 0). % do not introduce new constants
clauses(sos).
% Frink's basis for Boolean algebra (meet, complementation, 0).
x ^ x = x.
x ^ y = y ^ x.
(x ^ y) ^ z = x ^ (y ^ z).
x ^ y != x | x ^ y' = 0.
x ^ y = x | x ^ y' != 0.
% Definitions of join and 1.
x v y = (x' ^ y')'.
1 = 0'.
end_of_list.
% Because we already have commutativity and associativity of
% meet, it is sufficient to derive the Huntington axiom.
% We also prove one of the distributive properties.
assign(max_proofs, 2).
clauses(goals).
% Denials
(A' ^ B)' ^ (A' ^ B')' != A # answer(Huntington_axiom).
A ^ (B v C) != (A ^ B) v (A ^ C) # answer(Distributivity).
end_of_list.