Online Otter-λ

Utility Link | Utility Link | Utility Link
ExternalSimplification | SetTheory | LambdaLogic | Induction | More >
-->

Examplessmall logo



Examples -> SetTheory -> cantor2.in


% Cantor's theorem and Russell's paradox

set(lambda).
set(demod_inf).
set(binary_res).
assign(max_distinct_vars,2).
assign(max_weight,24).
assign(pick_given_ratio,4).

% typings:
% Prop Ap(P(alpha),alpha).
% P(alpha) Ap(beta,alpha) where beta is the type of c
% so polymorphically, something Ap(something, alpha); the second arg always has type alpha
% Prop not(Prop).
% P(Alpha) c(alpha).
% alpha J(P(alpha)).

list(usable).
% x=x. not needed
w != not(w).
u != v | v = u.
end_of_list.

list(demodulators).
not(not(x)) = x.
end_of_list.

list(sos).
Ap(x,z) = Ap(Ap(c,J(x)),z) |$ANS(x) | $ANS(z). % "negated" goal. Says every x of type P(alpha) is extensionally equal to c(J(x)).
end_of_list.