Online Otter-λ

Examples

Examples -> FirstOrderLogic -> quantifiers5.prf

2 [] -P(x)| -P(i(x,y))|P(y).
3 [] P(i(x,i(y,x))).
5 [] P(i(i(x,y),i(i(x,n(y)),n(x)))).
10 [] P(i(all(lambda(x,Ap(y,x))),Ap(y,z))).
17 [] P(Ap(a,c)).
18 [] -P(n(all(lambda(x,n(Ap(a,x)))))).
19 [hyper,17,2,3] P(i(x,Ap(a,c))).
21 [hyper,19,2,5] P(i(i(x,n(Ap(a,c))),n(x))).
43 [ur,21,2,18] -P(i(all(lambda(x,n(Ap(a,x)))),n(Ap(a,c)))).
44 [binary,43.1,10.1] $F.