Online Otter-λ

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

Examplessmall logo



Examples -> PeanoArithmetic -> le.in


% definition of < and <= in PA in terms of exists
% and proofs of their transitivity

set(lambda).
set(demod_inf).
set(binary_res).
set(para_into).
set(para_from).
assign(max_distinct_vars,1).
assign(max_weight,32).
weight_list(pick_and_purge).
weight(junk,50).
weight(g($(0)),1). %every g-term counts like a constant
end_of_list.


list(usable).
x = x.
x + 1 != 0.
x + 1 != y + 1 | x = y.
%-ap(y,0) | ap(y,g(y)) | ap(y,z).
%-ap(y,0) | -ap(y,g(y)+1) | ap(y,z).
x+0 = x.
-Ap(Z,w) | exists(lambda(x, Ap(Z,x))). % first law of existence
-exists(lambda(x,Ap(Z,x))) | Ap(Z, e(Z)). % second law of existence
% e is Hilbert's epsilon ex.Zx = e(lambda(x,Ap(Z,x))) = e(Z).
% or, we could formulate this using Ap(e,Z) instead of e(Z).
end_of_list.

list(demodulators).
(x+y)+z = x + y+z.
(u <= v) = exists(lambda(x,u+x = v)).
end_of_list.

list(sos).
a <= b.
b <= c.
-(a <= c).
end_of_list.