Dear Mizar- Forum, I have problems with the correctness of the claculus in CQC_THE1. When you admit free variables in the antecedents (in CQC_THE1 it is X) the substituation rule is not a correct rule in the normal sense. I attached the Mizar file and the abstract of the proof. I proved the correctness of this calculus when you don´t allow free variables in X. Clearly the attention is that X stands for axioms. At last I gave up working with the calculus and have formalized a sequent calculus. Does someone know something more about correctness of the caclulus in CQC_THE1? With best regards Patrick Braselmann
Attachment:
incons.abs
Description: MPEG audio
environ
vocabulary CQC_LANG, QC_LANG1, QC_LANG3, FINSEQ_1, RELAT_1,
CQC_THE1, QMAX_1, ZF_LANG, ZF_MODEL, BOOLE, PRE_TOPC, FUNCT_1, FUNCT_4,
PARTFUN1, VALUAT_1, FINSET_1, CQC_THE3, CQC_SIM1, FUNCT_2,
FUNCOP_1, GROUP_2, SETFAM_1, SUBSET_1, FINSUB_1, MARGREL1,
CAT_1, FRAENKEL, ARYTM_3, QC_LANG2, MCART_1, INCONST;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ARYTM_0, ARYTM, NAT_1,
FINSEQ_1, FUNCT_1, QC_LANG1, QC_LANG2, QC_LANG3, PARTFUN1,
CQC_LANG, CQC_THE1, VALUAT_1, RELAT_1, FINSET_1, CQC_THE3, FUNCT_4,
FUNCOP_1, FINSUB_1, RELSET_1, FUNCT_2, FRAENKEL,
MARGREL1, CQC_SIM1, DOMAIN_1, CORRECT, MCART_1;
constructors QC_LANG3, DOMAIN_1, CQC_THE1, ARYTM, VALUAT_1, RELAT_1,
CQC_THE3, RECDEF_1, CQC_SIM1, FINSEQ_1, PARTFUN1, FUNCT_2,
MARGREL1, CQC_LANG, CORRECT, NAT_1, MCART_1, FUNCT_1;
clusters NAT_1, FINSEQ_1, ARYTM_0, RELSET_1, CQC_LANG, ARYTM, ARYTM_3,
XBOOLE_0, FUNCOP_1, SUBSET_1, QC_LANG1, MARGREL1, FUNCT_1,
CORRECT, PARTFUN1, FINSET_1;
requirements ARYTM, NUMERALS, SUBSET, BOOLE;
theorems TARSKI, FINSEQ_1, FINSEQ_3, FUNCT_1, MCART_1, VALUAT_1,
XBOOLE_0, FINSEQ_2, CQC_LANG, QC_LANG1, ZFMISC_1, CQC_THE2,
SUBSET_1, RELAT_1, QC_LANG3, PROCAL_1, CORRECT, FUNCOP_1,
MARGREL1, FUNCT_2, PARTFUN1, RELSET_1, BOOLE, FINSET_1,
QC_LANG2, ENUMSET1, CQC_THE1, CQC_THE3;
definitions TARSKI, XBOOLE_0, CQC_THE3, MARGREL1, FUNCT_1, CORRECT;
schemes FUNCT_1, FUNCT_2, FINSEQ_1, CQC_LANG, QC_LANG1, QC_LANG3, CQC_SIM1,
NAT_1, XBOOLE_0;
begin
reserve a,b1,b2,c,c1,c2,d for set;
reserve P,P' for QC-pred_symbol of 2;
reserve y,z for bound_QC-variable;
reserve i,j,k,n for Nat;
reserve P1,P2 for QC-pred_symbol;
reserve X for Subset of CQC-WFF;
reserve p for Element of CQC-WFF;
reserve A for non empty set;
reserve v for Element of Valuations_in A;
reserve J for interpretation of A;
reserve f for Function;
reserve fin1 for FinSequence;
set x = [4,0];
set y = [4,1];
set b = a.0;
set l = <*x,b*>;
theorem
Th1: x is bound_QC-variable &
y is bound_QC-variable & l is QC-variable_list of 2
proof
4 in {4} by TARSKI:def 1; then
A1: x is bound_QC-variable &
y is bound_QC-variable by ZFMISC_1:106,QC_LANG1:def 2; then
reconsider x as bound_QC-variable;
x in QC-variables & b in QC-variables; then
A2: l is FinSequence of QC-variables by FINSEQ_2:15;
len l = 2 by FINSEQ_1:61;
hence thesis by A1,A2,QC_LANG1:def 8;
end; then
reconsider x as bound_QC-variable;
reconsider y as bound_QC-variable by Th1;
reconsider l as QC-variable_list of 2 by Th1;
theorem
Th2: y <> x & (P!l).y in CQC-WFF & not y in still_not-bound_in (P!l)
proof
set ll = Subst(l,b .--> y);
thus y <> x by ZFMISC_1:33;
now let a such that A1: a in rng ll;
consider i such that A2: i in dom ll & ll.i = a by A1,FINSEQ_2:11;
A3: len l = len ll by CQC_LANG:def 3; then
i in dom l by A2,FINSEQ_3:31; then
i in Seg (len l) by FINSEQ_1:def 3; then
i in Seg 2 by FINSEQ_1:61; then
A4: i = 1 or i = 2 by TARSKI:def 2,FINSEQ_1:4;
1 <= i & i <= len ll by A2,FINSEQ_3:27; then
A5: 1 <= i & i <= len l by A3;
A6: now assume i = 1; then
A7: l.i = x by FINSEQ_1:61;
b = [6,0] by QC_LANG3:def 4; then
l.i <> b by A7,ZFMISC_1:33; then
ll.i = l.i by A5,CQC_LANG:11;
hence ll.i is bound_QC-variable by A7,TARSKI:def 3;
end;
now assume i = 2; then
l.i = b by FINSEQ_1:61;
hence ll.i is bound_QC-variable by A5,CQC_LANG:11;
end;
hence a in bound_QC-variables by A2,A4,A6;
end; then
A8: rng ll c= bound_QC-variables by TARSKI:def 3; then
len ll = len l by CQC_LANG:def 3; then
len ll = 2 by FINSEQ_1:61; then
reconsider ll as CQC-variable_list of 2 by A8,CQC_LANG:def 5;
P!ll in CQC-WFF;
hence (P!l).y in CQC-WFF by CQC_LANG:30;
A9: variables_in(l,bound_QC-variables) =
{l.k : 1 <= k & k <= len l & l.k in bound_QC-variables} by QC_LANG3:def 2;
variables_in(l,bound_QC-variables) c= {x}
proof
let a such that A10: a in variables_in(l,bound_QC-variables);
consider k such that A11: a = l.k & 1 <= k & k <= len l &
l.k in bound_QC-variables by A9,A10,QC_LANG3:def 2;
1 <= k & k <= 2 by A11,FINSEQ_1:61; then
k in Seg 2 by FINSEQ_1:3; then
A12: k = 1 or k = 2 by TARSKI:def 2,FINSEQ_1:4;
A13: now assume k = 1; then
l.k = x by FINSEQ_1:61;
hence thesis by A11,TARSKI:def 1;
end;
now assume k = 2; then
A14: l.k = b by FINSEQ_1:61;
not 6 in {4} by TARSKI:def 1; then
not [6,0] in bound_QC-variables by ZFMISC_1:106,QC_LANG1:def 2; then
not b in bound_QC-variables by QC_LANG3:def 4;
hence contradiction by A11,A14;
end;
hence thesis by A12,A13;
end; then
still_not-bound_in l c= {x} by QC_LANG3:6; then
A15: still_not-bound_in (P!l) c= {x} by QC_LANG3:9;
now assume y in still_not-bound_in (P!l); then
y in {x} by A15,TARSKI:def 3; then
y = x by TARSKI:def 1;
hence contradiction by ZFMISC_1:33;
end;
hence thesis;
end;
set l1 = <*x,y*>;
theorem
Th3: l1 is CQC-variable_list of 2
proof
A1: l1 is FinSequence of QC-variables by FINSEQ_2:15;
len l1 = 2 by FINSEQ_1:61; then
reconsider l1 as QC-variable_list of 2 by A1,QC_LANG1:def 8;
l1 is FinSequence of bound_QC-variables by FINSEQ_2:15; then
A2: rng l1 c= bound_QC-variables by FINSEQ_1:def 4;
len l1 = 2 by FINSEQ_1:61;
hence thesis by A2,CQC_LANG:def 5;
end; then
reconsider l1 as CQC-variable_list of 2;
theorem
Th4: (P!l).y = P!l1
proof
set ll = Subst(l,a.0.-->y);
(P!l).y = P!ll by CQC_LANG:30; then
A1: (P!l).y = <*P*>^ll by QC_LANG1:23;
A2: P!l1 = <*P*>^l1 by QC_LANG1:23;
len ll = len l by CQC_LANG:def 3; then
A3: len ll = 2 by QC_LANG1:def 8; then
A4: len ll = len l1 by QC_LANG1:def 8;
now let j such that A5: j in Seg len ll;
j in {1,2} by A3,A5,FINSEQ_1:4; then
A6: j = 1 or j = 2 by TARSKI:def 2;
1 <= j & j <= len ll by A5,FINSEQ_1:3; then
A7: 1 <= j & j <= len l by CQC_LANG:def 3;
A8: now assume A9: j = 1; then
A10: l.j = x by FINSEQ_1:61;
b = [6,0] by QC_LANG3:def 4; then
l.j <> b by A10,ZFMISC_1:33; then
ll.j = x by A7,A10,CQC_LANG:11;
hence ll.j = l1.j by A9,FINSEQ_1:61;
end;
now assume A10: j = 2; then
l.j = b by FINSEQ_1:61; then
ll.j = y by A7,CQC_LANG:11;
hence ll.j = l1.j by A10,FINSEQ_1:61;
end;
hence ll.j = l1.j by A6,A8;
end; then
ll = l1 by A4,FINSEQ_2:10;
hence thesis by A1,A2;
end;
set l2 = <*x,x*>;
theorem
Th5: l2 is CQC-variable_list of 2
proof
A1: l2 is FinSequence of QC-variables by FINSEQ_2:15;
len l2 = 2 by FINSEQ_1:61; then
reconsider l2 as QC-variable_list of 2 by A1,QC_LANG1:def 8;
l2 is FinSequence of bound_QC-variables by FINSEQ_2:15; then
A2: rng l2 c= bound_QC-variables by FINSEQ_1:def 4;
len l2 = 2 by FINSEQ_1:61;
hence thesis by A2,CQC_LANG:def 5;
end; then
reconsider l2 as CQC-variable_list of 2;
theorem
Th6: (P!l).x = P!l2
proof
set ll = Subst(l,a.0.-->x);
(P!l).x = P!ll by CQC_LANG:30; then
A1: (P!l).x = <*P*>^ll by QC_LANG1:23;
A2: P!l2 = <*P*>^l2 by QC_LANG1:23;
len ll = len l by CQC_LANG:def 3; then
A3: len ll = 2 by QC_LANG1:def 8; then
A4: len ll = len l2 by QC_LANG1:def 8;
now let j such that A5: j in Seg len ll;
j in {1,2} by A3,A5,FINSEQ_1:4; then
A6: j = 1 or j = 2 by TARSKI:def 2;
1 <= j & j <= len ll by A5,FINSEQ_1:3; then
A7: 1 <= j & j <= len l by CQC_LANG:def 3;
A8: now assume A9: j = 1; then
A10: l.j = x by FINSEQ_1:61;
b = [6,0] by QC_LANG3:def 4; then
l.j <> b by A10,ZFMISC_1:33; then
ll.j = x by A7,A10,CQC_LANG:11;
hence ll.j = l2.j by A9,FINSEQ_1:61;
end;
now assume A10: j = 2; then
l.j = b by FINSEQ_1:61; then
ll.j = x by A7,CQC_LANG:11;
hence ll.j = l2.j by A10,FINSEQ_1:61;
end;
hence ll.j = l2.j by A6,A8;
end; then
ll = l2 by A4,FINSEQ_2:10;
hence thesis by A1,A2;
end;
theorem
Th7: ('not' (P!l)).y in CQC-WFF & not y in still_not-bound_in ('not' (P!l))
proof
((P!l).y) is Element of CQC-WFF by Th2; then
A1: 'not' ((P!l).y) is Element of CQC-WFF by CQC_LANG:18;
('not' (P!l)).y = 'not' ((P!l).y) by CQC_LANG:32;
hence ('not' (P!l)).y in CQC-WFF by A1;
still_not-bound_in (P!l) = still_not-bound_in ('not' (P!l))
by QC_LANG3:11;
hence thesis by Th2;
end;
theorem
Th8: ('not' (P!l)).x in CQC-WFF
proof
P!l2 is Element of CQC-WFF; then
(P!l).x is Element of CQC-WFF by Th6; then
'not' ((P!l).x) is Element of CQC-WFF by CQC_LANG:18; then
('not' (P!l)).x is Element of CQC-WFF by CQC_LANG:32;
hence thesis;
end;
theorem
Th9: 'not' (P!l1) = ('not' (P!l)).y
proof
('not' (P!l)).y = 'not' ((P!l).y) by CQC_LANG:32;
hence thesis by Th4;
end;
theorem
Th10: 'not' (P!l2) = ('not' (P!l)).x
proof
('not' (P!l)).x = 'not' ((P!l).x) by CQC_LANG:32;
hence thesis by Th6;
end;
theorem
Th11: {'not' (P!l1)} |- 'not' (P!l2)
proof
'not' (P!l1) in {'not' (P!l1)} by TARSKI:def 1; then
{'not' (P!l1)} |- 'not' (P!l1) by CQC_THE3:1; then
A1: {'not' (P!l1)} |- ('not' (P!l)).y by Th9,Th10;
('not' (P!l)).y in CQC-WFF & ('not' (P!l)).x in CQC-WFF &
not y in still_not-bound_in ('not' (P!l)) by Th7,Th8; then
{'not' (P!l1)} |- ('not' (P!l)).x by A1,CQC_THE1:95;
hence thesis by Th9,Th10;
end;
definition let A,J,v,X;
pred J,v |= X means :Def1: p in X implies J,v |= p;
end;
definition let X,p;
pred X |= p means :Def2: J,v |= X implies J,v |= p;
end;
reserve fin for FinSequence of {0,1};
definition
mode inc_Int -> interpretation of {0,1}
means :Def3: for P1 being (Element of QC-pred_symbols),
r being Element of relations_on {0,1} st it.P1 = r holds
(the_arity_of P1 <> 2 implies r = empty_rel({0,1})) &
the_arity_of P1 = 2 implies for a holds a in r iff
ex c st c in {0,1} & a = <*c,c*>;
existence
proof
set A = QC-pred_symbols;
A1: for a,b1,b2 st a in A &
(for P1 st P1 = a holds
(the_arity_of P1 <> 2 implies b1 = empty_rel({0,1})) &
(the_arity_of P1 = 2 implies for d holds
d in b1 iff ex c1 st c1 in {0,1} & d = <*c1,c1*>)) &
(for P1 st P1 = a holds
(the_arity_of P1 <> 2 implies b2 = empty_rel({0,1})) &
(the_arity_of P1 = 2 implies for d holds
d in b2 iff ex c1 st c1 in {0,1} & d = <*c1,c1*>))
holds b1 = b2
proof
let a,b1,b2 such that A2: a in A &
(for P1 st P1 = a holds
(the_arity_of P1 <> 2 implies b1 = empty_rel({0,1})) &
(the_arity_of P1 = 2 implies for c holds
c in b1 iff ex c1 st c1 in {0,1} & c = <*c1,c1*>)) &
(for P1 st P1 = a holds
(the_arity_of P1 <> 2 implies b2 = empty_rel({0,1})) &
(the_arity_of P1 = 2 implies for c holds
c in b2 iff ex c1 st c1 in {0,1} & c = <*c1,c1*>));
reconsider P2 = a as Element of QC-pred_symbols by A2;
A3: (the_arity_of P2 <> 2 implies b1 = empty_rel({0,1})) &
(the_arity_of P2 = 2 implies for c holds
c in b1 iff ex c1 st c1 in {0,1} & c = <*c1,c1*>) by A2;
A4: (the_arity_of P2 <> 2 implies b2 = empty_rel({0,1})) &
(the_arity_of P2 = 2 implies for c holds
c in b2 iff ex c1 st c1 in {0,1} & c = <*c1,c1*>) by A2;
A5: now assume the_arity_of P2 <> 2;
hence thesis by A3,A4;
end;
now assume the_arity_of P2 = 2; then
A6: (for c holds c in b1 iff ex c1 st c1 in {0,1} & c = <*c1,c1*>) &
(for c holds c in b2 iff ex c1 st c1 in {0,1} & c = <*c1,c1*>)
by A3,A4;
now let c;
(c in b1 iff ex c1 st c1 in {0,1} & c = <*c1,c1*>) &
(c in b2 iff ex c1 st c1 in {0,1} & c = <*c1,c1*>) by A6;
hence c in b1 iff c in b2;
end;
hence thesis by TARSKI:2;
end;
hence thesis by A5;
end;
A7: for a st a in A ex c st (for P1 st P1 = a holds
(the_arity_of P1 <> 2 implies c = empty_rel({0,1})) &
(the_arity_of P1 = 2 implies for d holds
d in c iff ex c1 st c1 in {0,1} & d = <*c1,c1*>))
proof
let a such that A8: a in A;
reconsider P2 = a as Element of QC-pred_symbols by A8;
A9: now assume A10: the_arity_of P2 <> 2;
take c = empty_rel({0,1});
thus for P2 st P2 = a holds
(the_arity_of P2 <> 2 implies c = empty_rel({0,1})) &
(the_arity_of P2 = 2 implies for d holds
d in c iff ex c1 st c1 in {0,1} & d = <*c1,c1*>)
proof
let P2 such that A11: P2 = a;
thus thesis by A10,A11;
end;
end;
now assume A12: the_arity_of P2 = 2;
consider c such that A13: for d holds d in c iff d in ({0,1})* &
ex c1 st c1 in {0,1} & d = <*c1,c1*> from Separation;
A14: d in c iff ex c1 st c1 in {0,1} & d = <*c1,c1*>
proof
thus d in c implies ex c1 st c1 in {0,1} & d = <*c1,c1*> by A13;
thus (ex c1 st c1 in {0,1} & d = <*c1,c1*>) implies d in c
proof
given c1 such that A15: c1 in {0,1} & d = <*c1,c1*>;
reconsider d as FinSequence by A15;
len d = 2 by A15,FINSEQ_1:61; then
A16: dom d = Seg 2 by FINSEQ_1:def 3;
d is FinSequence of {0,1} by A15,FINSEQ_2:15; then
d in {0,1}* by FINSEQ_1:def 11;
hence thesis by A13,A15;
end;
end;
take c;
thus for P2 st P2 = a holds
(the_arity_of P2 <> 2 implies c = empty_rel({0,1})) &
(the_arity_of P2 = 2 implies for d holds
d in c iff ex c1 st c1 in {0,1} & d = <*c1,c1*>)
proof
let P2 such that A15: P2 = a;
thus thesis by A12,A14,A15;
end;
end; then
A11: ex c st for P2 st P2 = a holds
(the_arity_of P2 <> 2 implies c = empty_rel({0,1})) &
(the_arity_of P2 = 2 implies for d holds
d in c iff ex c1 st c1 in {0,1} & d = <*c1,c1*>) by A9;
hence thesis by A11;
end;
consider f such that A12: dom f = A & for a st a in A holds
(for P1 st P1 = a holds
(the_arity_of P1 <> 2 implies f.a = empty_rel({0,1})) &
(the_arity_of P1 = 2 implies for c holds
c in f.a iff ex c1 st c1 in {0,1} & c = <*c1,c1*>)) from FuncEx(A1,A7);
A13: for P1 being (Element of QC-pred_symbols),
r being Element of relations_on {0,1} st f.P1 = r holds
(the_arity_of P1 <> 2 implies r = empty_rel({0,1})) &
the_arity_of P1 = 2 implies for a holds a in r iff
ex c st c in {0,1} & a = <*c,c*>
proof
let P1 being (Element of QC-pred_symbols),
r being Element of relations_on {0,1} such that A14: f.P1 = r;
A15: now assume the_arity_of P1 <> 2;
thus thesis by A12,A14;
end;
now assume the_arity_of P1 = 2;
thus thesis by A12,A14;
end;
hence thesis by A15;
end;
A16: for P1 being (Element of QC-pred_symbols),
r being Element of relations_on {0,1} st f.P1 = r holds
r = empty_rel({0,1}) or the_arity_of P1 = the_arity_of r
proof
let P1 being (Element of QC-pred_symbols),
r being Element of relations_on {0,1} such that
A17: f.P1 = r;
assume A18: r <> empty_rel({0,1}); then
A19: the_arity_of P1 = 2 by A12,A17; then
A20: for d holds d in r iff ex c1 st c1 in {0,1} & d = <*c1,c1*> by A12,A17;
d in r implies d is FinSequence of {0,1}
proof
assume d in r; then
consider c1 such that A21: c1 in {0,1} & d = <*c1,c1*> by A20;
thus thesis by A21,FINSEQ_2:15;
end; then
A21: for d being FinSequence of {0,1} holds
d in r implies ex c1 st c1 in {0,1} & d = <*c1,c1*> by A20;
fin in r implies len fin = 2
proof
assume fin in r; then
consider c1 such that A22: c1 in {0,1} & fin = <*c1,c1*> by A21;
thus len fin = 2 by A22,FINSEQ_1:61;
end; then
the_arity_of r = 2 by A18,MARGREL1:def 11;
hence thesis by A18,A19,MARGREL1:def 11;
end;
for b being set st b in rng f holds b in relations_on {0,1}
proof
let b being set;
assume b in rng f; then
consider a such that A21: a in dom f & b = f.a by FUNCT_1:def 5;
a in A by A12,A21; then
reconsider P2 = a as Element of QC-pred_symbols by A21;
A22: now assume the_arity_of P2 <> 2; then
b = empty_rel({0,1}) by A12,A21;
hence thesis;
end;
now assume the_arity_of P2 = 2; then
A23: for c holds c in b iff ex c1 st c1 in {0,1} & c = <*c1,c1*> by A12,A21;
c in b implies c in {0,1}*
proof
assume c in b; then
consider c1 such that A24: c1 in {0,1} & c = <*c1,c1*> by A23;
c is FinSequence of {0,1} by A24,FINSEQ_2:15;
hence c in {0,1}* by FINSEQ_1:def 11;
end; then
A25: b c= {0,1}* by TARSKI:def 3;
A26: for fin,fin' being FinSequence of {0,1} st fin in b & fin' in b
holds len fin = len fin'
proof
let fin,fin' being FinSequence of {0,1};
assume A27: fin in b & fin' in b; then
consider c1 such that A28: c1 in {0,1} & fin = <*c1,c1*> by A23;
consider c2 such that A29: c2 in {0,1} & fin' = <*c2,c2*> by A23,A27;
len fin' = 2 & len fin = 2 by A28,A29,FINSEQ_1:61;
hence len fin' = len fin;
end;
hence thesis by A25,MARGREL1:def 8;
end;
hence thesis by A22;
end; then
rng f c= relations_on {0,1} by TARSKI:def 3; then
reconsider f as Function of A,relations_on {0,1} by A12,FUNCT_2:4;
reconsider f as interpretation of {0,1} by A16,VALUAT_1:def 10;
take f;
thus thesis by A13;
end;
end;
reserve J for inc_Int;
x = [4,0];
y = [4,1];
b = a.0;
l = <*x,b*>;
b = a.0;
l2 = <*x,x*>;
l1 = <*x,y*>;
X is Subset of CQC-WFF;
p is Element of CQC-WFF;
theorem
Th6: for P being QC-pred_symbol holds
P is (QC-pred_symbol of k) &
P is (QC-pred_symbol of i) implies k = i
proof
let P being QC-pred_symbol;
assume A1: P is (QC-pred_symbol of k) &
P is (QC-pred_symbol of i);
then P in k-ary_QC-pred_symbols;
then P in {P1 : the_arity_of P1 = k} by QC_LANG1:def 7;
then consider P1 such that A2: P1 = P &
the_arity_of P1 = k;
P in i-ary_QC-pred_symbols by A1;
then P in {P2 : the_arity_of P2 = i} by QC_LANG1:def 7;
then consider P2 such that A3: P2 = P &
the_arity_of P2 = i;
the_arity_of P = k & the_arity_of P = i by A2,A3;
hence thesis;
end;
theorem
Th7: {'not' (P!l1)} |= 'not' (P!l2) implies contradiction
proof
assume A1: {'not' (P!l1)} |= 'not' (P!l2);
A2: for a,b1,b2 st a in bound_QC-variables &
((a = [4,0] implies b1 = 0) & (a = [4,1] implies b1 = 1) &
((a <> [4,0] & a <> [4,1]) implies b1 = 0)) &
((a = [4,0] implies b2 = 0) & (a = [4,1] implies b2 = 1) &
((a <> [4,0] & a <> [4,1]) implies b2 = 0)) holds b1 = b2
proof
let a,b1,b2 such that
A3: a in bound_QC-variables &
((a = [4,0] implies b1 = 0) & (a = [4,1] implies b1 = 1) &
((a <> [4,0] & a <> [4,1]) implies b1 = 0)) &
((a = [4,0] implies b2 = 0) & (a = [4,1] implies b2 = 1) &
((a <> [4,0] & a <> [4,1]) implies b2 = 0));
consider c1,c2 such that
A4: c1 in {4} & c2 in NAT & a = [c1,c2]
by A3,QC_LANG1:def 2,ZFMISC_1:def 2;
A5: now assume a = [4,0];
hence thesis by A3;
end;
A6: now assume a = [4,1];
hence thesis by A3;
end;
now assume (a <> [4,1] or a <> [4,1]);
hence thesis by A3;
end;
hence thesis by A5,A6;
end;
A7: for a st a in bound_QC-variables ex c st
((a = [4,0] implies c = 0) & (a = [4,1] implies c = 1) &
((a <> [4,0] & a <> [4,1]) implies c = 0))
proof
let a such that A8: a in bound_QC-variables;
A9: [4,0] <> [4,1] by ZFMISC_1:33;
A10: now assume A11: a = [4,0];
take c = 0;
thus thesis by A9,A11;
end;
now assume A12: (a <> [4,0] & a <> [4,1]);
take c = 0;
thus thesis by A12;
end;
hence thesis by A10;
end;
consider f such that A13: dom f = bound_QC-variables &
for a st a in bound_QC-variables holds
((a = [4,0] implies f.a = 0) & (a = [4,1] implies f.a = 1) &
((a <> [4,0] & a <> [4,1]) implies f.a = 0)) from FuncEx(A2,A7);
now let b being set such that A14: b in rng f;
consider a such that A15: a in dom f & f.a = b by A14,FUNCT_1:def 5;
A16: now assume a = [4,0]; then
b = 0 by A13,A15;
hence b in {0,1} by TARSKI:def 2;
end;
A17: now assume a = [4,1]; then
b = 1 by A13,A15;
hence b in {0,1} by TARSKI:def 2;
end;
now assume a <> [4,0] & a <> [4,1]; then
b = 0 by A13,A15;
hence b in {0,1} by TARSKI:def 2;
end;
hence b in {0,1} by A16,A17;
end; then
rng f c= {0,1} by TARSKI:def 3; then
f in Funcs(bound_QC-variables,{0,1}) by A13,FUNCT_2:def 2; then
reconsider v = f as Element of Valuations_in {0,1} by VALUAT_1:def 1;
P is (Element of QC-pred_symbols);
J.P is Element of relations_on {0,1};
set k = the_arity_of P;
P is (QC-pred_symbol of 2) &
P is (QC-pred_symbol of k) by Th6,QC_LANG3:3; then
A18: k = 2 by Th6,QC_LANG3:3;
consider J;
now assume J,v |= P!l1; then
Valid(P!l1,J).v = TRUE by VALUAT_1:def 12; then
v*'l1 in J.P by VALUAT_1:16; then
consider c such that A19: c in {0,1} & v*'l1 = <*c,c*> by A18,Def3;
A20: len l1 = 2 by FINSEQ_1:61;
A21: c = 0 or c = 1 by A19,TARSKI:def 2;
A22: now assume A24: c = 1;
l1.1 = x by FINSEQ_1:61; then
A23: v.(l1.1) = 0 by A13;
1 <= 1 & 1 <= 2;
v*'l1.1 = 0 by A20,A23,VALUAT_1:def 8;
hence contradiction by A19,A24,FINSEQ_1:61;
end;
now assume A24: c = 0;
l1.2 = y by FINSEQ_1:61; then
A25: v.(l1.2) = 1 by A13;
1 <= 2 & 2<= 2;
v*'l1.2 = 1 by A20,A25,VALUAT_1:def 8;
hence contradiction by A19,A24,FINSEQ_1:61;
end;
hence contradiction by A21,A22;
end; then
not J,v |= P!l1; then
A26: J,v |= 'not' (P!l1) by VALUAT_1:28;
now let p such that A27: p in {'not' (P!l1)};
p = 'not' (P!l1) by A27,TARSKI:def 1;
hence J,v |= p by A26;
end; then
J,v |= {'not' (P!l1)} by Def1; then
J,v |= 'not' (P!l2) by A1,Def2; then
Valid('not' (P!l2),J).v = TRUE by VALUAT_1:def 12; then
'not' (Valid(P!l2,J).v) = TRUE by VALUAT_1:20; then
Valid(P!l2,J).v = FALSE by MARGREL1:41; then
not (v*'l2 in J.P) by VALUAT_1:17; then
A27: for c holds not c in {0,1} or not v*'l2 = <*c,c*> by A18,Def3;
set c = 0;
c in {0,1} by TARSKI:def 2; then
A28: not v*'l2 = <*c,c*> by A27;
A29: len (v*'l2) = 2 by VALUAT_1:def 8; then
A30: len (v*'l2) = len <*c,c*> by FINSEQ_1:61;
now let j such that A31: j in Seg 2;
A32: j = 1 or j = 2 by A31,TARSKI:def 2,FINSEQ_1:4;
A33: now assume A34: j = 1; then
l2.j = x by FINSEQ_1:61; then
A35: v.(l2.j) = c by A13; then
1 <= j & j <= 2 by A34; then
v*'l2.j = c by A35,VALUAT_1:def 8;
hence v*'l2.j = <*c,c*>.j by A34,FINSEQ_1:61;
end;
now assume A36: j = 2; then
l2.j = x by FINSEQ_1:61; then
A37: v.(l2.j) = c by A13; then
1 <= j & j <= 2 by A36; then
v*'l2.j = c by A37,VALUAT_1:def 8;
hence v*'l2.j = <*c,c*>.j by A36,FINSEQ_1:61;
end;
hence v*'l2.j = <*c,c*>.j by A32,A33;
end;
hence thesis by A28,A29,A30,FINSEQ_2:10;
end;