#################################################
#################################################
#################################################
9 Appendix: LWB and Prolog code to generate formulae
#################################################
#################################################
#################################################
#################################################
#################################################
# 9.0 General utilities
#################################################
# for the LWB
# Don't forget to include these if needed
proc : p(i)
# takes an integer > 0, returns an atom
# eg from 123 it returns p123
begin
return symbol("p", i);
end;
#------------------------------------------------
# Here is how to test some problems:
# modify this appropriately...
for j := 1 to 8 do
begin
ct :== clockticks(); # :== is silent
provable(class_n(j));
clockticks() - ct;
end;
%================================================
% for Prolog
% Prolog operator definitions
:- op(425, fy, ~ ).
:- op(450, yfx, &). % left associative
:- op(475, yfx, v ). % left associative
:- op(500, xfx, <-> ). % non associative
:- op(500, xfy, ->). % right associative
%%% WARNING, this overwrites Prolog's ->
% Timing tools differ between implementations...
#################################################
#################################################
# 9.1 de Bruijn formulae
#################################################
load(ipc);
proc : de_bruijn_p(n)
# generates the 2n+1^th "de Bruijn" formula
# should be provable
local a, c, i, last;
begin
c := p(1);
last := 2 mult n+1;
for i := 2 to last do c := c & p(i) ;
a := true;
for i := 1 to last-1 do
a := a & ((p(i) <-> p(i+1)) -> c);
a := a & ((p(last) <-> p(1)) -> c);
return ( a -> c );
end; #de_bruijn_p
proc : de_bruijn_n(n)
# generates the 2n^th "de Bruijn" formula
# should be not provable
# tweaked to make them classically provable...
local a, c, i, last;
begin
c := p(1);
last := 2 mult n;
for i := 2 to last do c := c & p(i) ;
a := true;
for i := 1 to last-1 do
a := a & ((p(i) <-> p(i+1)) -> c);
a := a & ((p(last) <-> p(1)) -> c);
return ( a -> ( p(0) v c v ~p(0) ));
end; #de_bruijn_n
%Prolog code--------------------------------------
de_bruijn_p(N, F ) :-
N1 is 2*N + 1,
dB(N1, F).
de_bruijn_n(N, F ) :-
N1 is 2*N,
dB(N1, A -> C),
F = A -> ( p0 v C v ~p0 ).
dB(N, A -> C) :-
atoms(N, N, [], Ps),
conj(Ps, C),
make(Ps, C, As),
conj(As, A).
atoms(_, M, Atoms, Atoms) :- M =< 0.
atoms(N, M, Atoms, Result) :-
M > 0,
M1 is M-1,
atoms(N, M1, [p(M) | Atoms], Result).
conj( [H], H).
conj( [H1, H2 | Tail], C) :-
conj( [H1 & H2 | Tail], C).
make([ P0 | Ps], C, As ) :-
make4([ P0 | Ps], P0, C, As).
make4( [Pn], P0, C, [(Pn<->P0)->C] ).
make4( [P1, P2 | Tail], P0, C, [(P1<->P2)->C | Rest] ) :-
make4( [P2 | Tail], P0, C, Rest).
#################################################
#################################################
#9.2 Pigeonhole formulae
#################################################
load(ipc);
proc : ph_p(n)
begin
return ( left(n) -> right(n) );
end; # ph_p
proc : ph_n(n)
begin
return ( left_n(n) -> right(n) );
end; # ph_p
proc : conjoin( c1, c2)
begin
if c1 = true then return c2 ; else return c1 & c2;
end; #conjoin
proc : disjoin( d1, d2 )
begin
if d1 = false then return d2 ; else return d1 v d2;
end; # disjoin
proc : right(n)
local d, h, p1, p2 ;
begin
d := false;
for h := 1 to n do
for p1 := 1 to n+1 do
for p2 := p1+1 to n+1 do
d := disjoin(d, (o(p1, h) & o(p2, h))) ;
return d;
end; # right
proc : left(n)
local c, d, p, h;
begin
c := true;
for p := 1 to n+1 do
begin
d := false;
for h := 1 to n do
d := disjoin(d, o(p,h) );
c := conjoin(c,d);
end;
return c;
end; # left
proc : left_n(n)
# uses DN to make non-provable
local c, d, p, h, oph;
begin
c := true;
for p := 1 to n+1 do
begin
d := false;
for h := 1 to n do
begin
oph := o(p,h);
if h = n then oph := ~ ~oph;
d := disjoin(d, oph);
end;
c := conjoin(c,d);
end;
return c;
end; # left_n
%Prolog code--------------------------------------
ph_p(N, L -> R ) :-
left(N, pos, L),
right(N,R).
ph_n(N, L -> R ) :-
left(N, neg, L),
right(N,R).
right(N, R) :-
disj(N, 1, false, R).
disj( N, H, D, D ) :-
H > N.
disj( N, H, D, D1 ) :-
H =< N,
N1 is N+1,
disj1(N1, H, 1, D, D0),
H1 is H+1,
disj(N, H1, D0, D1).
disj1( N1, _, P1, D, D ) :-
P1 > N1.
disj1( N1, H, P1, D, D1 ) :-
P1 =< N1,
P11 is P1 + 1,
disj2(N1, H, P1, P11, D, D0),
disj1(N1, H, P11, D0, D1).
disj2( N1, _, _, P2, D, D ) :-
P2 > N1.
disj2( N1, H, P1, P2, D, D1 ) :-
P2 =< N1,
P21 is P2+1,
disjoin(D, o(P1,H) & o(P2,H), DC),
disj2(N1, H, P1, P21, DC, D1).
left( N, Sign, L ) :-
N1 is N+1,
conj(N1, N, 1, Sign, true, L).
conj(N1, _, P, _, C, C ) :-
P > N1.
conj(N1, N, P, Sign, C, C1 ) :-
P =< N1,
cd(N, 1, P, false, Sign, D),
P1 is P+1,
conjoin(C, D, CD),
conj(N1, N, P1, Sign, CD, C1).
cd( N, H, _, D, _, D ) :-
H > N.
cd( N, H, P, D, Sign, D1 ) :-
H =< N,
H1 is H+1,
signify(Sign, o(P,H), H-N, SOPH),
disjoin(D, SOPH, DOPH),
cd(N, H1, P, DOPH, Sign, D1).
signify( neg, X, H - H, ~ ~X) :- !.
signify( _, X, _ - _, X).
disjoin(false, D, D) :- !.
disjoin(D1, D, D1 v D).
conjoin(true, D, D) :- !.
conjoin(D1, D, D1 & D).
#################################################
#################################################
9.3
#################################################
# Examples of Franzen
# con_p(n) requires n contractions in LJ
# con_n(n) similar but unprovable
#################################################
load(ipc);
proc : nix( a )
begin
return ( a -> f) ;
end; # nix
# like negation, but to avoid use of Glivenko's theorem
proc : trans_e(n)
# n >= 1
local d, i;
begin
d := nix(p(1)) ;
for i := 2 to n do d := d v nix(p(i));
return d;
end; #trans_e
proc : trans_en(n)
# n >= 1
local d, i;
begin
d := ~ ~nix(p(1)) ;
for i := 2 to n do d := d v nix(p(i));
return d;
end; #trans_e
proc : trans_a(n)
# n >= 1
local c, i;
begin
c := p(1) ;
for i := 2 to n do c := c & p(i);
return c;
end; #trans_a
proc : con_p( n )
# n >= 0
begin
return (nix (nix (trans_a(n) v trans_e(n))));
end; # con_p
proc : con_n( n )
# n >= 1
begin
return (nix (nix (trans_a(n) v trans_en(n))));
end; # con_n
%Prolog code--------------------------------------
con_p(N, ( (C v D) -> f) -> f ) :-
disjs(N, pos, D),
conjs(N, C).
con_n(N, ( (C v D) -> f) -> f ) :-
disjs(N, neg, D),
conjs(N, C).
conjs(1, p(1)).
conjs(N, C & p(N) ) :-
N > 1,
N1 is N-1,
conjs(N1, C).
disjs(1, pos, p(1) -> f).
disjs(1, neg, ( ~ ~p(1)) -> f).
disjs(N, Sign, D v ( p(N) -> f) ) :-
N > 1,
N1 is N-1,
disjs(N1, Sign, D).
#################################################
#################################################
9.4
#################################################
# Schwichtenberg's formulae
# normal natural deduction of schwicht_p(n) has size exponential in n
% easy for sequent calculus-based systems
#################################################
load(ipc);
proc : schwicht_p( n )
# n >= 0
local ant, i;
begin
ant := p(n);
for i:= 1 to n do
ant := ant & ( p(i) -> p(i) -> p(i-1));
return (ant -> p(0) );
end; #schwicht_p
proc : schwicht_n( n )
# n >= 0
local ant, i;
begin
ant := ~ ~p(n);
for i:= 1 to n do
ant := ant & ( p(i) -> p(i) -> p(i-1));
return (ant -> p(0)) ;
end; #schwicht_n
%Prolog code------------------------------------------------
schwicht_p( N, A -> p(0) ) :-
ant(N, 1, p(N), A).
schwicht_n( N, A -> p(0) ) :-
ant(N, 1, ~ ~p(N), A).
ant( N, I, A, A ) :- I > N.
ant( N, I, A, A1 ) :-
I =< N,
I1 is I+1, IM1 is I-1,
ant(N, I1, A & ( p(I) -> p(I) -> p(IM1)) , A1).
#################################################
#################################################
9.5
#################################################
# Korn & Kreitz's formulae
# modified to avoid use of Glivenko theorem
#################################################
load(ipc);
proc : nix( a )
# like negation, but to avoid use of Glivenko's theorem
begin
return ( a -> f) ;
end; # nix
proc : kk_p( n )
# n >= 1
local lhs, lhsr, i;
begin
lhs := nix(a(0)) & ((b(n)->b(0))->a(n));
for i := 1 to n do
lhs := lhs & ((b(i-1)->a(i))->a(i-1));
lhsr := ((b(n)->b(0))->a(n)) & nix(a(0));
for i := 1 to n do
lhsr := ((b(i-1)->a(i))->a(i-1)) & lhsr ;
return( nix(lhs) & nix(lhsr) );
end; #kk_p
proc : kk_n( n )
# n >= 1
# use of double negation to
# maintain classical provability but
# destroy intuitionistic provability
local lhs, i;
begin
lhs := nix(a(0)) & ((~ ~b(n)->b(0))->a(n));
for i := 1 to n do
lhs := lhs & ((~ ~b(i-1)->a(i))->a(i-1));
return( nix(lhs));
end; #kk_n
%Prolog code--------------------------------------
kk_p(N, (A->f) & (AR->f) ) :- kk_p(N, N, A), kkr(N,N,AR).
kk_p(N, 0, (a(0) -> f) & ((b(N)->b(0))-> ( a(N)) ) ).
kk_p(N, I, LHS & ((b(I1)->a(I))->( a(I1))) ) :-
0 < I,
I1 is I-1,
kk_p(N, I1, LHS).
kkr(N, 0, ((b(N)->b(0))-> a(N) ) & (a(0) -> f) ).
kkr(N, I, ((b(I1)->a(I))-> a(I1) ) & LHS ) :-
0 < I,
I1 is I-1,
kkr(N, I1, LHS).
kk_n(N, A -> f ) :- kk_n(N, N, A).
kk_n(N, 0, (a(0) -> f) & ((~ ~b(N)->b(0))-> ( a(N)) ) ).
kk_n(N, I, LHS & ((~ ~b(I1)->a(I))->( a(I1))) ) :-
0 < I,
I1 is I-1,
kk_n(N, I1, LHS).
#################################################
#################################################
# 9.6 Equivalences
#################################################
proc : equiv_p(n)
# n >= 1
local l, r, i ;
begin
l := a(1); r := a(1);
for i := 2 to n do
begin
l := l <-> a(i);
r := a(i) <-> r ;
end;
return ( l <-> r);
end; #equiv_p
proc : equiv_n(n)
# n >= 1
local l, r, i ;
begin
l := ~ ~a(1); r := a(1);
for i := 2 to n do
begin
l := l <-> a(i);
r := a(i) <-> r ;
end;
return ( l <-> r);
end; #equiv_n
%Prolog code--------------------------------------
equiv_p( N, A ) :- equiv( N, p, A).
equiv_n( N, A ) :- equiv( N, n, A).
equiv( 1, n, (~ ~a(1)) <-> a(1) ).
equiv( 1, p, a(1) <-> a(1) ).
equiv(N, S, AB <-> BA ) :-
N > 1,
N1 is N-1, AN = a(N),
equiv( N1, S, A1 <-> A2),
AB = A1 <-> AN,
BA = AN <-> A2.
#################################################
#################################################
#################################################
#################################################
#################################################
#################################################
#################################################