set E = {} NAT;
set R = [:{{0}},NAT:];
A1: ( dom [:{{0}},NAT:] = {{0}} & rng [:{{0}},NAT:] = NAT ) by RELAT_1:160;
then [:{{0}},NAT:] is finitary ;
then reconsider R = [:{{0}},NAT:] as Rule ;
0 in NAT by ORDINAL1:def 12;
then A2: {0} c= NAT by TARSKI:def 1;
then {0} in Fin NAT by FINSUB_1:def 5;
then dom R c= Fin NAT by A1, TARSKI:def 1;
then reconsider R = R as Rule of NAT by A1, Def2;
reconsider P = ProofSystem(# NAT,({} NAT),R #) as non empty ProofSystem ;
take P ; :: thesis: ( P is consistent & not P is paraconsistent )
thus P is consistent :: thesis: not P is paraconsistent
proof
take a = the Element of NAT ; :: according to PROOFS_1:def 19 :: thesis: ( a in P & not P |- a )
thus a in P ; :: thesis: not P |- a
assume P |- a ; :: thesis: contradiction
then {} NAT,R |- a ;
then consider p being {} NAT,R -correct Formula-sequence such that
A10: a in rng p ;
set k = len p;
not p is empty by A10;
then len p >= 1 by FINSEQ_1:20;
then 1 in Seg (len p) by FINSEQ_1:1;
then A11: 1 in dom p by FINSEQ_1:def 3;
p is {} NAT,R -correct ;
then p,1 is_a_correct_step_wrt {} NAT,R by A11;
then consider Q being Formula-finset such that
A12: [Q,(p . 1)] in R and
A13: for t being Formula st t in Q holds
ex m being Nat st
( m in dom p & m < 1 & p . m = t ) ;
Q in {{0}} by A12, ZFMISC_1:87;
then Q = {0} by TARSKI:def 1;
then 0 in Q by TARSKI:def 1;
then consider m being Nat such that
A15: m in dom p and
A16: m < 1 and
p . m = 0 by A13;
m in Seg (len p) by A15, FINSEQ_1:def 3;
hence contradiction by A16, FINSEQ_1:1; :: thesis: verum
end;
reconsider S = {0} as finite Subset of P by A2;
for a being object st a in P \/ S holds
P \/ S |- a
proof
let a be object ; :: thesis: ( a in P \/ S implies P \/ S |- a )
assume a in P \/ S ; :: thesis: P \/ S |- a
then reconsider k = a as Element of NAT ;
set p = <*0,k*>;
len <*0,k*> = 2 by FINSEQ_1:44;
then A20: dom <*0,k*> = {1,2} by FINSEQ_1:2, FINSEQ_1:def 3;
then ( 2 in dom <*0,k*> & <*0,k*> . 2 = k ) by TARSKI:def 2;
then A22: k in rng <*0,k*> by FUNCT_1:3;
<*0,k*> is S,R -correct
proof
let m be Nat; :: according to PROOFS_1:def 7 :: thesis: ( m in dom <*0,k*> implies <*0,k*>,m is_a_correct_step_wrt S,R )
assume m in dom <*0,k*> ; :: thesis: <*0,k*>,m is_a_correct_step_wrt S,R
per cases then ( m = 1 or m = 2 ) by A20, TARSKI:def 2;
suppose A25: m = 2 ; :: thesis: <*0,k*>,m is_a_correct_step_wrt S,R
reconsider Q = {0} as Formula-finset ;
Q in {{0}} by TARSKI:def 1;
then A26: [Q,k] in R by ZFMISC_1:87;
for t being Formula st t in Q holds
ex n being Nat st
( n in dom <*0,k*> & n < m & <*0,k*> . n = t )
proof
let t be Formula ; :: thesis: ( t in Q implies ex n being Nat st
( n in dom <*0,k*> & n < m & <*0,k*> . n = t ) )
assume t in Q ; :: thesis: ex n being Nat st
( n in dom <*0,k*> & n < m & <*0,k*> . n = t )
then A28: t = 0 by TARSKI:def 1;
take n = 1; :: thesis: ( n in dom <*0,k*> & n < m & <*0,k*> . n = t )
thus n in dom <*0,k*> by A20, TARSKI:def 2; :: thesis: ( n < m & <*0,k*> . n = t )
thus n < m by A25; :: thesis: <*0,k*> . n = t
thus <*0,k*> . n = t by A28; :: thesis: verum
end;
hence <*0,k*>,m is_a_correct_step_wrt S,R by A25, A26; :: thesis: verum
end;
end;
end;
then S,R |- k by A22;
hence P \/ S |- a ; :: thesis: verum
end;
then P \/ S is inconsistent ;
then S is inconsistent ;
hence not P is paraconsistent ; :: thesis: verum