Copyright (c) 1990 Association of Mizar Users
environ
vocabulary FUNCT_2, QC_LANG1, FRAENKEL, FUNCT_1, RELAT_1, MARGREL1, BOOLE,
ZF_LANG, CQC_LANG, FINSEQ_1, ARYTM_3, FUNCOP_1, ZF_MODEL, QC_LANG3,
CAT_1, VALUAT_1;
notation TARSKI, XBOOLE_0, SUBSET_1, XREAL_0, NAT_1, RELAT_1, FUNCT_1,
FUNCT_2, FINSEQ_1, FRAENKEL, QC_LANG1, QC_LANG3, CQC_LANG, MARGREL1;
constructors QC_LANG3, CQC_LANG, MARGREL1, XREAL_0, XCMPLX_0, MEMBERED,
XBOOLE_0;
clusters RELSET_1, MARGREL1, CQC_LANG, QC_LANG1, ARYTM_3, FINSEQ_1, FUNCT_1,
MEMBERED, ZFMISC_1, XBOOLE_0;
requirements NUMERALS, SUBSET, BOOLE;
definitions TARSKI, MARGREL1;
theorems TARSKI, FINSEQ_1, FUNCT_1, FUNCT_2, FUNCOP_1, FRAENKEL, QC_LANG1,
QC_LANG2, QC_LANG3, CQC_LANG, MARGREL1, RELSET_1, RELAT_1, FINSEQ_3,
XBOOLE_0, XBOOLE_1;
schemes QC_LANG1, CQC_LANG, FUNCT_1, FUNCT_2;
begin
reserve i,j,k for Nat,
A,D for non empty set;
definition let A be set;
func Valuations_in A -> set equals
:Def1: Funcs(bound_QC-variables, A);
coherence;
end;
definition let A;
cluster Valuations_in A -> non empty functional;
coherence
proof
Valuations_in A = Funcs(bound_QC-variables, A) by Def1;
hence thesis;
end;
end;
canceled;
theorem
Th2: for x being set st x is Element of Valuations_in A holds
x is Function of bound_QC-variables ,A
proof let x be set;
assume x is Element of Valuations_in A;
then x in Valuations_in A;
then x in Funcs(bound_QC-variables,A) by Def1;
then ex f being Function st
x = f & dom f = bound_QC-variables & rng f c= A by FUNCT_2:def 2;
hence thesis by FUNCT_2:def 1,RELSET_1:11;
end;
definition
let A;
redefine func Valuations_in A -> FUNCTION_DOMAIN of bound_QC-variables, A;
coherence
proof
for x be Element of Valuations_in A holds
x is Function of bound_QC-variables ,A by Th2;
hence Valuations_in A is FUNCTION_DOMAIN of bound_QC-variables, A
by FRAENKEL:def 2;
end;
end;
definition let f be Function;
attr f is boolean-valued means
:Def2: rng f c= BOOLEAN;
end;
definition
cluster boolean-valued Function;
existence
proof take {};
thus rng {} c= BOOLEAN by RELAT_1:60,XBOOLE_1:2;
end;
end;
definition let f be boolean-valued Function, x be set;
cluster f.x -> boolean;
coherence
proof
per cases;
suppose not x in dom f;
then f.x = 0 by FUNCT_1:def 4;
hence f.x in BOOLEAN by MARGREL1:def 12,TARSKI:def 2;
suppose x in dom f;
then A1: f.x in rng f by FUNCT_1:def 5;
rng f c= BOOLEAN by Def2;
hence f.x in BOOLEAN by A1;
end;
end;
definition let A be set;
cluster -> boolean-valued Element of Funcs(A,BOOLEAN);
coherence
proof let F be Element of Funcs(A,BOOLEAN);
ex f being Function st F = f & dom f = A & rng f c= BOOLEAN
by FUNCT_2:def 2;
hence rng F c= BOOLEAN;
end;
end;
definition
let p be boolean-valued Function;
func 'not' p -> Function means
:Def3: dom it = dom p &
for x being set st x in dom p holds it.x = 'not'(p.x);
existence
proof
deffunc F(set) = 'not'(p.$1);
consider q being Function such that
A1: dom q = dom p and
A2: for x being set st x in dom p holds q.x = F(x) from Lambda;
take q;
thus thesis by A1,A2;
end;
uniqueness
proof let q1,q2 be Function such that
A3: dom q1 = dom p and
A4: for x being set st x in dom p holds q1.x = 'not'(p.x) and
A5: dom q2 = dom p and
A6: for x being set st x in dom p holds q2.x = 'not'(p.x);
for x being set st x in dom p holds q1.x = q2.x
proof let x be set;
assume x in dom p;
then q1.x = 'not'(p.x) & q2.x = 'not'(p.x) by A4,A6;
hence thesis;
end;
hence thesis by A3,A5,FUNCT_1:9;
end;
let q be boolean-valued Function;
func p '&' q -> Function means
:Def4: dom it = dom p /\ dom q &
for x being set st x in dom it holds it.x = (p.x) '&' (q.x);
existence
proof
deffunc F(set) = (p.$1) '&' (q.$1);
consider s being Function such that
A7: dom s = dom p /\ dom q and
A8: for x being set st x in dom p /\ dom q
holds s.x = F(x) from Lambda;
take s;
thus thesis by A7,A8;
end;
uniqueness
proof let s1,s2 be Function such that
A9: dom s1 = dom p /\ dom q and
A10: for x being set st x in dom s1 holds s1.x = (p.x) '&' (q.x) and
A11: dom s2 = dom p /\ dom q and
A12: for x being set st x in dom s2 holds s2.x = (p.x) '&' (q.x);
for x being set st x in dom s1 holds s1.x = s2.x
proof let x be set;
assume x in dom s1;
then s1.x = (p.x) '&' (q.x) & s2.x = (p.x) '&' (q.x) by A9,A10,A11,
A12;
hence thesis;
end;
hence thesis by A9,A11,FUNCT_1:9;
end;
commutativity;
end;
definition
let p be boolean-valued Function;
cluster 'not' p -> boolean-valued;
coherence
proof let x be set;
assume x in rng 'not' p;
then consider y being set such that
A1: y in dom 'not' p and
A2: x = ('not' p).y by FUNCT_1:def 5;
A3: y in dom p by A1,Def3;
then A4: x = 'not'(p.y) by A2,Def3;
A5: rng p c= BOOLEAN by Def2;
p.y in rng p by A3,FUNCT_1:def 5;
then p.y = FALSE or p.y = TRUE by A5,MARGREL1:37,TARSKI:def 2;
then x = FALSE or x = TRUE by A4,MARGREL1:def 16;
hence x in BOOLEAN;
end;
let q be boolean-valued Function;
cluster p '&' q -> boolean-valued;
coherence
proof let x be set;
assume x in rng(p '&' q);
then consider y being set such that
A6: y in dom(p '&' q) and
A7: x = (p '&' q).y by FUNCT_1:def 5;
A8: x = (p.y) '&' (q.y) by A6,A7,Def4;
p.y = TRUE & q.y = TRUE or not(p.y = TRUE & q.y = TRUE);
then x = FALSE or x = TRUE by A8,MARGREL1:def 17;
hence x in BOOLEAN;
end;
end;
reserve f1,f2 for Element of Funcs(Valuations_in A,BOOLEAN),
x,x1,y for bound_QC-variable,
v,v1 for Element of Valuations_in A;
definition let A;
redefine
let p be Element of Funcs(A,BOOLEAN);
func 'not' p -> Element of Funcs(A,BOOLEAN) means
:Def5: for x being Element of A holds it.x = 'not'(p.x);
coherence
proof
ex f being Function st p = f & dom f = A & rng f c= BOOLEAN
by FUNCT_2:def 2;
then A1: dom 'not' p = A by Def3;
rng 'not' p c= BOOLEAN by Def2;
hence thesis by A1,FUNCT_2:def 2;
end;
compatibility
proof let IT be Element of Funcs(A,BOOLEAN);
hereby assume
A2: IT = 'not' p;
let x be Element of A;
x in A;
then x in dom p by FUNCT_2:def 1;
hence IT.x = 'not'(p.x) by A2,Def3;
end;
assume
A3: for x being Element of A holds IT.x = 'not'(p.x);
A4: dom IT = A by FUNCT_2:def 1;
A5: dom p = A by FUNCT_2:def 1;
then for x being set st x in dom p holds IT.x = 'not'(p.x) by A3;
hence IT = 'not' p by A4,A5,Def3;
end;
let q be Element of Funcs(A,BOOLEAN);
func p '&' q -> Element of Funcs(A,BOOLEAN) means
:Def6: for x being Element of A holds it.x = (p.x) '&' (q.x);
coherence
proof
A6: ex f being Function st p = f & dom f = A & rng f c= BOOLEAN
by FUNCT_2:def 2;
ex f being Function st q = f & dom f = A & rng f c= BOOLEAN
by FUNCT_2:def 2;
then A7: dom(p '&' q) = A /\ A by A6,Def4 .= A;
rng(p '&' q) c= BOOLEAN by Def2;
hence thesis by A7,FUNCT_2:def 2;
end;
compatibility
proof let IT be Element of Funcs(A,BOOLEAN);
hereby assume
A8: IT = p '&' q;
let x be Element of A;
A9: dom p = A by FUNCT_2:def 1;
dom q = A by FUNCT_2:def 1;
then dom(p '&' q) = A /\ A by A9,Def4 .= A;
hence IT.x = (p.x) '&' (q.x) by A8,Def4;
end;
assume
A10: for x being Element of A holds IT.x = (p.x) '&' (q.x);
A11: dom IT = A by FUNCT_2:def 1;
A12: dom q = A by FUNCT_2:def 1;
A13: dom IT = A /\ A by FUNCT_2:def 1 .= dom p /\ dom q by A12,FUNCT_2:def 1;
for x being set st x in dom IT holds IT.x = (p.x) '&' (q.x) by A10,A11;
hence IT = p '&' q by A13,Def4;
end;
end;
definition
let A, x;
let p be Element of Funcs(Valuations_in A,BOOLEAN);
func FOR_ALL(x,p) -> Element of Funcs(Valuations_in A,BOOLEAN) means
:Def7: for v holds
it.v = ALL{p.v' where v' is Element of Valuations_in A:
for y st x <> y holds v'.y = v.y};
existence
proof
deffunc F(Function) = ALL{p.v' where v' is Element of Valuations_in A:
for y st x <> y holds v'.y = $1.y};
consider f being Function of Valuations_in A, BOOLEAN such that
A1: for v holds f.v = F(v) from LambdaD;
dom f = Valuations_in A & rng f c= BOOLEAN by FUNCT_2:def 1,RELSET_1:12;
then reconsider f as Element of Funcs(Valuations_in A,BOOLEAN) by FUNCT_2:
def 2;
take f;
thus thesis by A1;
end;
uniqueness
proof let f1,f2;
assume that
A2: for v holds f1.v = ALL{p.v' where v' is Element of Valuations_in A:
for y st x <> y holds v'.y = v.y} and
A3: for v holds f2.v = ALL{p.v' where v' is Element of Valuations_in A:
for y st x <> y holds v'.y = v.y};
for v holds f1.v = f2.v
proof let v;
f1.v = ALL{p.v' where v' is Element of Valuations_in A:
for y st x <> y holds v'.y = v.y} &
f2.v = ALL{p.v'' where v'' is Element of Valuations_in A:
for y st x <> y holds v''.y = v.y} by A2,A3;
hence thesis;
end;
hence thesis by FUNCT_2:113;
end;
end;
canceled 4;
theorem
Th7: for p being Element of Funcs(Valuations_in A,BOOLEAN) holds
FOR_ALL(x,p).v = FALSE iff ex v1 st p.v1 = FALSE &
for y st x <> y holds v1.y = v.y
proof let p be Element of Funcs(Valuations_in A,BOOLEAN);
A1: now
assume FOR_ALL(x,p).v = FALSE;
then ALL{p.v'' where v'' is Element of Valuations_in A:
for y st x <> y holds v''.y = v.y} = FALSE by Def7;
then FALSE in {p.v'' where v'' is Element of Valuations_in A:
for y st x <> y holds v''.y = v.y} by MARGREL1:53;
hence ex v1 st p.v1 = FALSE & for y st x <> y holds v1.y = v.y;
end;
now assume
ex v1 st p.v1 = FALSE & for y st x <> y holds v1.y = v.y;
then FALSE in {p.v'' where v'' is Element of Valuations_in A:
for y st x <> y holds v''.y = v.y};
then ALL{p.v'' where v'' is Element of Valuations_in A:
for y st x <> y holds v''.y = v.y} = FALSE by MARGREL1:53;
hence FOR_ALL(x,p).v = FALSE by Def7;
end;
hence thesis by A1;
end;
theorem
Th8: for p being Element of Funcs(Valuations_in A,BOOLEAN) holds
FOR_ALL(x,p).v = TRUE iff for v1 st for y st x <> y holds v1.y = v.y holds
p.v1 = TRUE
proof let p be Element of Funcs(Valuations_in A,BOOLEAN);
A1: now
assume FOR_ALL(x,p).v = TRUE;
then ALL{p.v'' where v'' is Element of Valuations_in A:
for y st x <> y holds v''.y = v.y} = TRUE by Def7;
then A2: not FALSE in {p.v'' where v'' is Element of Valuations_in A:
for y st x <> y holds v''.y = v.y} by MARGREL1:53;
thus for v1 st for y st x <> y holds v1.y = v.y holds p.v1 = TRUE
proof let v1;
assume for y st x <> y holds v1.y = v.y;
then not p.v1 = FALSE by A2;
hence (p.v1 = TRUE) by MARGREL1:43;
end;
end;
now assume
A3: for v1 st for y st x <> y holds v1.y = v.y holds p.v1 = TRUE;
for v1 st for y st x <> y holds v1.y = v.y holds not p.v1 = FALSE
proof let v1;
assume for y st x <> y holds v1.y = v.y;
then p.v1 = TRUE by A3;
hence not (p.v1 = FALSE) by MARGREL1:43;
end;
then not ex v1 st p.v1 = FALSE & for y st x <> y holds v1.y = v.y;
then not FALSE in {p.v'' where v'' is Element of Valuations_in A:
for y st x <> y holds v''.y = v.y};
then ALL{p.v'' where v'' is Element of Valuations_in A:
for y st x <> y holds v''.y = v.y} = TRUE by MARGREL1:53;
hence FOR_ALL(x,p).v = TRUE by Def7;
end;
hence thesis by A1;
end;
reserve ll for CQC-variable_list of k;
definition
let A, k, ll, v;
redefine
func v*ll -> FinSequence of A means
:Def8: len it = k & for i st 1 <= i & i <= k holds it.i = v.(ll.i);
coherence
proof
dom v = bound_QC-variables by FUNCT_2:def 1;
then A1: rng ll c= dom v by CQC_LANG:def 5;
A2: len ll = k by QC_LANG1:def 8;
dom(v*ll) = dom ll by A1,RELAT_1:46
.= Seg k by A2,FINSEQ_1:def 3;
then A3: v*ll is FinSequence-like by FINSEQ_1:def 2;
A4: rng v c= A by RELSET_1:12;
rng(v*ll) c= rng v by RELAT_1:45;
then rng( v*ll) c= A by A4,XBOOLE_1:1;
hence v*ll is FinSequence of A by A3,FINSEQ_1:def 4;
end;
compatibility
proof let IT be FinSequence of A;
dom v = bound_QC-variables by FUNCT_2:def 1;
then A5: rng ll c= dom v by CQC_LANG:def 5;
A6: len ll = k by QC_LANG1:def 8;
thus IT = v*ll implies
len IT = k & for i st 1 <= i & i <= k holds IT.i = v.(ll.i)
proof assume
A7: IT = v*ll;
then A8: dom ll = dom IT by A5,RELAT_1:46;
hence len IT = k by A6,FINSEQ_3:31;
let i;
assume 1 <= i & i <= k;
then i in dom IT by A6,A8,FINSEQ_3:27;
hence IT.i = v.(ll.i) by A7,FUNCT_1:22;
end;
assume that
A9: len IT = k and
A10: for i st 1 <= i & i <= k holds IT.i = v.(ll.i);
A11: for x being set holds x in dom IT iff x in dom ll & ll.x in dom v
proof let x be set;
thus x in dom IT implies x in dom ll & ll.x in dom v
proof assume x in dom IT;
hence x in dom ll by A6,A9,FINSEQ_3:31;
then ll.x in rng ll by FUNCT_1:def 5;
hence ll.x in dom v by A5;
end;
assume x in dom ll & ll.x in dom v;
hence x in dom IT by A6,A9,FINSEQ_3:31;
end;
for x being set st x in dom IT holds IT.x = v.(ll.x)
proof let x be set;
assume
A12: x in dom IT;
then reconsider i = x as Nat;
1 <= i & i <= k by A9,A12,FINSEQ_3:27;
hence IT.x = v.(ll.x) by A10;
end;
hence IT = v*ll by A11,FUNCT_1:20;
end;
synonym v*'ll;
end;
definition
let A, k, ll;
let r be Element of relations_on A;
func ll 'in' r -> Element of Funcs(Valuations_in A,BOOLEAN) means
:Def9: for v being Element of Valuations_in A holds
(v*'ll in r implies it.v = TRUE) &
(not v*'ll in r implies it.v = FALSE);
existence
proof
deffunc F(set) = FALSE;
deffunc T(set) = TRUE;
defpred C[set] means ex v being Element of Valuations_in A st $1 = v &
v*'ll in r;
A1: for x being set st x in Valuations_in A holds
(C[x] implies T(x) in BOOLEAN) &
(not C[x] implies F(x) in BOOLEAN);
consider f being Function of Valuations_in A, BOOLEAN such that
A2: for x being set st x in Valuations_in A holds
(C[x] implies f.x = T(x)) &
(not C[x] implies f.x = F(x)) from Lambda1C(A1);
dom f = Valuations_in A & rng f c= BOOLEAN by FUNCT_2:def 1,RELSET_1:12;
then reconsider f as Element of Funcs(Valuations_in A,BOOLEAN) by FUNCT_2:
def 2;
take f;
let v be Element of Valuations_in A;
((ex v' being Element of Valuations_in A st v = v' &
v'*'ll in r) implies f.v = TRUE) &
(not (ex v' being Element of Valuations_in A st v = v' &
v'*'ll in r) implies f.v = FALSE) by A2;
hence thesis;
end;
uniqueness
proof let f1,f2 be Element of Funcs(Valuations_in A,BOOLEAN);
assume that
A3: for v being Element of Valuations_in A holds
(v*'ll in r implies f1.v = TRUE) &
(not v*'ll in r implies f1.v = FALSE) and
A4: for v being Element of Valuations_in A holds
(v*'ll in r implies f2.v = TRUE) &
(not v*'ll in r implies f2.v = FALSE);
for v being Element of Valuations_in A holds f1.v = f2.v
proof let v be Element of Valuations_in A;
per cases;
suppose v*'ll in r;
then f1.v = TRUE & f2.v = TRUE by A3,A4;
hence thesis;
suppose not v*'ll in r;
then f1.v = FALSE & f2.v = FALSE by A3,A4;
hence thesis;
end;
hence thesis by FUNCT_2:113;
end;
end;
definition
let A;
let F be Function of CQC-WFF,Funcs(Valuations_in A, BOOLEAN);
let p be Element of CQC-WFF;
redefine func F.p -> Element of Funcs(Valuations_in A, BOOLEAN);
coherence
proof
thus F.p is Element of Funcs(Valuations_in A, BOOLEAN);
end;
end;
definition
let D;
mode interpretation of D -> Function of QC-pred_symbols, relations_on D
means
for P being (Element of QC-pred_symbols),
r being Element of relations_on D st it.P = r holds
r = empty_rel(D) or the_arity_of P = the_arity_of r;
existence
proof
reconsider F1 = QC-pred_symbols --> empty_rel(D)
as Function of QC-pred_symbols, relations_on D;
take F1;
let P be Element of QC-pred_symbols;
thus thesis by FUNCOP_1:13;
end;
end;
reserve
p,q,s,t for Element of CQC-WFF,
J for interpretation of A,
P for QC-pred_symbol of k,
r for Element of relations_on A;
definition let A, k, J, P;
redefine func J.P -> Element of relations_on A;
coherence by FUNCT_2:7;
end;
definition let A, J, p;
func Valid(p,J) -> Element of Funcs(Valuations_in A, BOOLEAN) means
:Def11: ex F being Function of CQC-WFF,Funcs(Valuations_in A, BOOLEAN) st
it = F.p &
F.VERUM = (Valuations_in A --> TRUE) &
for p,q being Element of CQC-WFF,
x being bound_QC-variable, k being Nat,
ll being CQC-variable_list of k,
P being QC-pred_symbol of k holds
F.(P!ll) = (ll 'in' (J.P)) &
F.('not' p) = 'not'(F.p) &
(F.(p '&' q)) = ((F.p) '&' (F.q)) &
F.(All(x,p)) = (FOR_ALL(x,F.p));
correctness
proof
set D = Funcs(Valuations_in A, BOOLEAN);
set V = Valuations_in A --> TRUE;
deffunc A(Nat, QC-pred_symbol of $1, CQC-variable_list of $1)
= $3 'in' (J.$2);
deffunc N(Element of D) = 'not' $1;
deffunc C(Element of D, Element of D) = $1 '&' $2;
deffunc Q(bound_QC-variable, Element of D) = FOR_ALL($1,$2);
thus (ex d being Element of D st
ex F being Function of CQC-WFF, D st d = F.p &
F.VERUM = V &
for r,s being (Element of CQC-WFF),
x being bound_QC-variable, k being Nat
for l being CQC-variable_list of k
for P being QC-pred_symbol of k holds
F.(P!l) = A(k,P,l) &
F.('not' r) = N(F.r) &
F.(r '&' s) = C(F.r,F.s) &
F.All(x,r) = Q(x,F.r) )
& (for d1,d2 being Element of D st
(ex F being Function of CQC-WFF, D st d1 = F.p &
F.VERUM = V &
for r,s being (Element of CQC-WFF),
x being bound_QC-variable, k being Nat
for l being CQC-variable_list of k
for P being QC-pred_symbol of k holds
F.(P!l) = A(k,P,l) &
F.('not' r) = N(F.r) &
F.(r '&' s) = C(F.r,F.s) &
F.All(x,r) = Q(x,F.r) ) &
(ex F being Function of CQC-WFF, D st d2 = F.p &
F.VERUM = V &
for r,s being (Element of CQC-WFF),
x being bound_QC-variable, k being Nat
for l being CQC-variable_list of k
for P being QC-pred_symbol of k holds
F.(P!l) = A(k,P,l) &
F.('not' r) = N(F.r) &
F.(r '&' s) = C(F.r,F.s) &
F.All(x,r) = Q(x,F.r) )
holds d1 = d2) from CQC_Def_correctness;
end;
end;
Lm1:
for A, J holds
Valid(VERUM,J) = (Valuations_in A --> TRUE) &
(for k, ll, P holds Valid(P!ll,J) = ll 'in' (J.P)) &
(for p holds Valid('not' p,J) = 'not' Valid(p,J)) &
(for q holds Valid(p '&' q,J) = Valid(p,J) '&' Valid(q,J)) &
(for x holds Valid(All(x,p),J) = FOR_ALL(x,Valid(p,J)))
proof
let A, J;
set D = Funcs(Valuations_in A, BOOLEAN);
set V = Valuations_in A --> TRUE;
deffunc A(Nat, QC-pred_symbol of $1, CQC-variable_list of $1)
= $3 'in' (J.$2);
deffunc N(Element of D) = 'not' $1;
deffunc C(Element of D, Element of D) = $1 '&' $2;
deffunc Q(bound_QC-variable, Element of D) = FOR_ALL($1,$2);
deffunc X(Element of CQC-WFF) = Valid($1, J);
A1:for p holds for d be Element of D holds (
d = (X(p)) iff
ex F being Function of CQC-WFF, D st
d = F.p &
F.VERUM = V &
for p,q being Element of CQC-WFF,
x being bound_QC-variable, k being Nat,
ll being CQC-variable_list of k,
P being QC-pred_symbol of k holds
F.(P!ll) = A(k, P, ll) &
F.('not' p) = N(F.p) &
(F.(p '&' q)) = C(F.p,F.q) &
F.(All(x,p)) = Q(x,F.p)) by Def11;
thus X(VERUM) = V from CQC_Def_VERUM(A1);
hereby let k, ll, P;
thus X(P!ll) = A(k,P,ll) from CQC_Def_atomic(A1);
end;
hereby let p;
thus X('not' p) = N(X(p)) from CQC_Def_negative(A1);
end;
hereby let q;
thus X(p '&' q) = C(X(p), X(q)) from QC_Def_conjunctive(A1);
end;
let x;
thus X(All(x,p)) = Q(x,X(p)) from QC_Def_universal(A1);
end;
canceled 4;
theorem
Valid(VERUM,J) = Valuations_in A --> TRUE by Lm1;
theorem
Th14: Valid(VERUM,J).v = TRUE
proof
(Valuations_in A --> TRUE).v = TRUE by FUNCOP_1:13;
hence Valid(VERUM,J).v = TRUE by Lm1;
end;
theorem
Valid(P!ll,J) = ll 'in' (J.P) by Lm1;
theorem
Th16: p = P!ll & r = J.P implies (v*'ll in r iff Valid(p,J).v = TRUE)
proof assume
A1: p = P!ll & r = J.P;
A2: now assume v*'ll in r;
then (ll 'in' (J.P)).v = TRUE by A1,Def9;
hence Valid(p,J).v = TRUE by A1,Lm1;
end;
now assume Valid(p,J).v = TRUE;
then (ll 'in' (J.P)).v <> FALSE by A1,Lm1,MARGREL1:38;
hence v*'ll in r by A1,Def9;
end;
hence thesis by A2;
end;
theorem Th17:
p = P!ll & r = J.P implies (not (v*'ll in r) iff Valid(p,J).v = FALSE)
proof assume
A1: p = P!ll & r = J.P;
A2: now assume not (v*'ll in r);
then (ll 'in' (J.P)).v = FALSE by A1,Def9;
hence Valid(p,J).v = FALSE by A1,Lm1;
end;
now assume Valid(p,J).v = FALSE;
then (ll 'in' (J.P)).v <> TRUE by A1,Lm1,MARGREL1:38;
hence not (v*'ll in r) by A1,Def9;
end;
hence thesis by A2;
end;
canceled;
theorem
Valid('not' p,J) = 'not' Valid(p,J) by Lm1;
theorem
Th20: Valid('not' p,J).v = 'not'(Valid(p,J).v)
proof
Valid('not' p,J).v = ('not' Valid(p,J)).v by Lm1;
hence Valid('not' p,J).v = 'not' (Valid(p,J).v) by Def5;
end;
theorem
Valid(p '&'q ,J) = Valid(p,J) '&' Valid(q,J) by Lm1;
theorem
Th22: Valid(p '&'q ,J).v = (Valid(p,J).v) '&' (Valid(q,J).v)
proof
Valid(p '&'q ,J).v = (Valid(p,J) '&' Valid(q,J)).v by Lm1;
hence Valid(p '&'q ,J).v = (Valid(p,J).v) '&' (Valid(q,J).v) by Def6;
end;
theorem
Valid(All(x,p),J) = FOR_ALL(x,Valid(p,J)) by Lm1;
theorem
Th24: Valid(p '&' 'not' p,J).v = FALSE
proof
A1: Valid(p '&' 'not' p,J).v = (Valid(p,J).v) '&' (Valid('not' p,J).v)
by Th22
.= (Valid(p,J).v) '&' 'not'(Valid(p,J).v) by Th20;
A2: now assume (Valid(p,J)).v = TRUE;
then 'not'(Valid(p,J).v) = FALSE by MARGREL1:41;
hence (Valid(p,J).v) '&' 'not'(Valid(p,J).v) = FALSE by MARGREL1:45;
end;
Valid(p,J).v = FALSE implies (Valid(p,J).v) '&' 'not'
(Valid(p,J).v) = FALSE
by MARGREL1:45;
hence Valid(p '&' 'not' p,J).v = FALSE by A1,A2,MARGREL1:39;
end;
theorem
Valid('not'(p '&' 'not' p),J).v = TRUE
proof
Valid('not'(p '&' 'not' p),J).v = 'not'(Valid(p '&' 'not' p,J).v) by Th20
.= 'not' FALSE by Th24;
hence thesis by MARGREL1:41;
end;
definition
let A, p, J, v;
pred J,v |= p means
:Def12: Valid(p,J).v = TRUE;
end;
canceled;
theorem
J,v |= P!ll iff (ll 'in' (J.P)).v = TRUE
proof
A1:now assume J,v |= P!ll;
then Valid(P!ll,J).v = TRUE by Def12;
hence (ll 'in' (J.P)).v = TRUE by Lm1;
end;
now assume (ll 'in' (J.P)).v = TRUE;
then Valid(P!ll,J).v = TRUE by Lm1;
hence J,v |= P!ll by Def12;
end;
hence thesis by A1;
end;
theorem
J,v |= 'not' p iff not J,v |= p
proof
A1: now assume J,v |= 'not' p;
then Valid('not' p,J).v = TRUE by Def12;
then 'not' Valid(p,J).v = TRUE by Lm1;
then 'not'(Valid(p,J).v) = TRUE by Def5;
then Valid(p,J).v = FALSE by MARGREL1:41;
then not (Valid(p,J).v = TRUE) by MARGREL1:43;
hence not J,v |= p by Def12;
end;
now assume not J,v |= p;
then not (Valid(p,J).v = TRUE) by Def12;
then Valid(p,J).v = FALSE by MARGREL1:43;
then 'not'(Valid(p,J).v) = TRUE by MARGREL1:41;
then 'not' Valid(p,J).v = TRUE by Def5;
then Valid('not' p,J).v = TRUE by Lm1;
hence J,v |= 'not' p by Def12;
end;
hence thesis by A1;
end;
theorem
J,v |= (p '&' q) iff J,v |= p & J,v |= q
proof
A1: now assume J,v |= (p '&' q);
then Valid(p '&' q,J).v = TRUE by Def12;
then (Valid(p,J) '&' Valid(q,J)).v = TRUE by Lm1;
then (Valid(p,J).v) '&' (Valid(q,J).v) = TRUE by Def6;
then Valid(p,J).v = TRUE & Valid(q,J).v = TRUE by MARGREL1:45;
hence J,v |= p & J,v |= q by Def12;
end;
now assume J,v |= p & J,v |= q;
then Valid(p,J).v = TRUE & Valid(q,J).v = TRUE by Def12;
then (Valid(p,J).v) '&' (Valid(q,J).v) = TRUE by MARGREL1:45;
then (Valid(p,J) '&' Valid(q,J)).v = TRUE by Def6;
then Valid(p '&' q,J).v = TRUE by Lm1;
hence J,v |= (p '&' q) by Def12;
end;
hence thesis by A1;
end;
theorem
Th30: J,v |= All(x,p) iff FOR_ALL(x,Valid(p,J)).v = TRUE
proof
A1:now assume J,v |= All(x,p);
then Valid(All(x,p),J).v = TRUE by Def12;
hence FOR_ALL(x,Valid(p,J)).v = TRUE by Lm1;
end;
now assume FOR_ALL(x,Valid(p,J)).v = TRUE;
then Valid(All(x,p),J).v = TRUE by Lm1;
hence J,v |= All(x,p) by Def12;
end;
hence thesis by A1;
end;
theorem
Th31: J,v |= All(x,p) iff
for v1 st for y st x <> y holds v1.y = v.y holds Valid(p,J).v1 = TRUE
proof
A1:now assume J,v |= All(x,p);
then FOR_ALL(x,Valid(p,J)).v = TRUE by Th30;
hence
for v1 st for y st x <> y holds v1.y = v.y holds Valid(p,J).v1 = TRUE
by Th8;
end;
now assume
for v1 st for y st x <> y holds v1.y = v.y holds Valid(p,J).v1 = TRUE;
then FOR_ALL(x,Valid(p,J)).v = TRUE by Th8;
hence J,v |= All(x,p) by Th30;
end;
hence thesis by A1;
end;
theorem
Valid('not' 'not' p,J) = Valid(p,J)
proof
now let v;
thus Valid('not' 'not' p,J).v = 'not'(Valid('not' p,J).v) by Th20
.= 'not'('not'(Valid(p,J).v)) by Th20
.= Valid(p,J).v by MARGREL1:40;
end;
hence Valid('not' 'not' p,J) = Valid(p,J) by FUNCT_2:113;
end;
theorem
Th33: Valid(p '&' p,J) = Valid(p,J)
proof
now let v;
A1: Valid(p '&' p,J).v = (Valid(p,J).v) '&' (Valid(p,J).v) by Th22;
then A2: (Valid(p '&' p, J).v) = TRUE implies Valid(p, J).v = TRUE by
MARGREL1:45;
(Valid(p '&' p, J).v) = FALSE implies Valid(p, J).v = FALSE by A1,
MARGREL1:51;
hence Valid(p '&'p, J).v = Valid(p,J).v by A2,MARGREL1:39;
end;
hence Valid(p '&' p,J) = Valid(p,J) by FUNCT_2:113;
end;
canceled;
theorem
Th35: J,v |= p => q iff
Valid(p, J).v = FALSE or Valid(q, J).v = TRUE
proof
A1: now assume J,v |= p => q;
then Valid(p => q, J).v = TRUE by Def12;
then Valid('not'(p '&' 'not' q), J).v = TRUE by QC_LANG2:def 2;
then 'not'(Valid(p '&' 'not' q, J).v) = TRUE by Th20;
then Valid(p '&' 'not' q, J).v = FALSE by MARGREL1:41;
then (Valid(p, J).v) '&' (Valid('not' q, J).v) = FALSE by Th22;
then (Valid(p, J).v) '&' 'not'(Valid(q, J).v) = FALSE by Th20;
then Valid(p, J).v = FALSE or 'not' (Valid(q, J).v) = FALSE by MARGREL1:
45;
hence Valid(p, J).v = FALSE or Valid(q, J).v = TRUE by MARGREL1:41;
end;
now assume A2: Valid(p, J).v = FALSE or Valid(q, J).v = TRUE;
A3: now assume Valid(p, J).v = FALSE;
then (Valid(p, J).v) '&' (Valid('not' q, J).v) = FALSE by MARGREL1:45
;
then Valid(p '&' 'not' q, J).v = FALSE by Th22;
then 'not'(Valid(p '&' 'not' q, J).v) = TRUE by MARGREL1:41;
then Valid('not'(p '&' 'not' q), J).v = TRUE by Th20;
then Valid(p => q, J).v = TRUE by QC_LANG2:def 2;
hence J,v |= p => q by Def12;
end;
now assume A4: Valid(q, J).v = TRUE;
assume not J,v |= p => q;
then Valid(p => q, J).v <> TRUE by Def12;
then Valid(p => q, J).v = FALSE by MARGREL1:39;
then Valid('not'(p '&' 'not' q), J).v = FALSE by QC_LANG2:def 2;
then 'not'(Valid(p '&' 'not' q, J).v) = FALSE by Th20;
then Valid(p '&' 'not' q, J).v = TRUE by MARGREL1:41;
then (Valid(p, J).v) '&' (Valid('not' q, J).v) = TRUE by Th22;
then (Valid(p, J).v) '&' 'not'(Valid(q, J).v) = TRUE by Th20;
then Valid(p, J).v = TRUE & 'not' (Valid(q, J).v) = TRUE by MARGREL1:
45;
hence contradiction by A4,MARGREL1:38,41;
end;
hence J,v |= p => q by A2,A3;
end;
hence thesis by A1;
end;
theorem
Th36: J,v |= p => q iff (J,v |= p implies J,v |= q)
proof
A1: now assume J,v |= p => q;
then A2: Valid(p, J).v = FALSE or Valid(q, J).v = TRUE by Th35;
now assume J,v |= p;
then Valid(p, J).v = TRUE by Def12;
hence J,v |= q by A2,Def12,MARGREL1:43;
end;
hence J,v |= p implies J,v |= q;
end;
now assume J,v |= p implies J,v |= q;
then Valid(p, J).v = TRUE implies Valid(q, J).v = TRUE by Def12;
then Valid(p, J).v = FALSE or Valid(q, J).v = TRUE by MARGREL1:43;
hence J,v |= p => q by Th35;
end;
hence thesis by A1;
end;
theorem
Th37: for p being Element of Funcs(Valuations_in A,BOOLEAN) holds
FOR_ALL(x,p).v = TRUE implies p.v = TRUE
proof let p be Element of Funcs(Valuations_in A,BOOLEAN);
for y st x <> y holds v.y = v.y;
hence thesis by Th8;
end;
definition
let A, J, p;
pred J |= p means
:Def13: for v holds J,v |= p;
end;
reserve u,w,z for Element of BOOLEAN;
Lm2: 'not'('not'(u '&' 'not' w) '&' ('not'(w '&' z) '&' (u '&' z))) = TRUE
proof
per cases by MARGREL1:39;
suppose that
A1: z = TRUE and
A2: w = TRUE;
w '&' z = TRUE by A1,A2,MARGREL1:45;
then 'not'(w '&' z) = FALSE by MARGREL1:41;
then 'not'(w '&' z) '&' (u '&' z) = FALSE by MARGREL1:45;
then 'not'(u '&' 'not' w) '&' ('not'
(w '&' z) '&' (u '&' z)) = FALSE by MARGREL1:45;
hence thesis by MARGREL1:41;
suppose that
A3: w = FALSE and
A4: u = TRUE;
'not' w = TRUE by A3,MARGREL1:41;
then u '&' 'not' w = TRUE by A4,MARGREL1:45;
then 'not'(u '&' 'not' w) = FALSE by MARGREL1:41;
then 'not'(u '&' 'not' w) '&' ('not'
(w '&' z) '&' (u '&' z)) = FALSE by MARGREL1:45;
hence thesis by MARGREL1:41;
suppose u = FALSE;
then u '&' z = FALSE by MARGREL1:45;
then 'not'(w '&' z) '&' (u '&' z) = FALSE by MARGREL1:45;
then 'not'(u '&' 'not' w) '&' ('not'
(w '&' z) '&' (u '&' z)) = FALSE by MARGREL1:45;
hence thesis by MARGREL1:41;
suppose z = FALSE;
then u '&' z = FALSE by MARGREL1:45;
then 'not'(w '&' z) '&' (u '&' z) = FALSE by MARGREL1:45;
then 'not'(u '&' 'not' w) '&' ('not'
(w '&' z) '&' (u '&' z)) = FALSE by MARGREL1:45;
hence thesis by MARGREL1:41;
end;
reserve w,v2 for Element of Valuations_in A,
z for bound_QC-variable;
scheme Lambda_Val {A() -> non empty set, Y, Z() -> bound_QC-variable,
V1, V2() -> Element of Valuations_in A()}:
ex v being Element of Valuations_in A() st
(for x being bound_QC-variable st x <> Y() holds v.x = V1().x) &
v.Y() = V2().Z()
proof
defpred C[set] means for x1 st x1 = $1 holds x1 <> Y();
deffunc F(set) = V1().$1;
deffunc G(set) = V2().Z();
A1: for x being set st x in bound_QC-variables holds
(C[x] implies F(x) in A()) &
(not C[x] implies G(x) in A())
by FUNCT_2:7;
consider f being Function of bound_QC-variables, A() such that
A2: for x being set st x in bound_QC-variables holds
(C[x] implies f.x = F(x)) & (not C[x] implies f.x = G(x))
from Lambda1C(A1);
dom f = bound_QC-variables & rng f c= A() by FUNCT_2:def 1,RELSET_1:12;
then f is Element of Funcs(bound_QC-variables,A()) by FUNCT_2:def 2;
then reconsider f as Element of Valuations_in A() by Def1;
take f;
now let x be bound_QC-variable;
now assume A3: x <> Y();
(for x1 st x1 = x holds x1 <> Y()) implies f.x = V1().x by A2;
hence f.x = V1().x by A3;
end;
hence x <> Y() implies f.x = V1().x;
thus x = Y() implies f.Y() = V2().Z() by A2;
end;
hence thesis;
end;
canceled;
theorem
Th39:
not x in still_not-bound_in p implies
for v,w st for y st x<>y holds w.y = v.y holds Valid(p,J).v = Valid(p,J).w
proof
defpred PP[Element of CQC-WFF] means
not x in still_not-bound_in $1 implies
for v,w st for y st x<>y holds w.y = v.y holds
Valid($1,J).v = Valid($1,J).w;
A1: now
let s,t,y,k,ll,P;
A2: rng ll c= bound_QC-variables by CQC_LANG:def 5;
thus PP[VERUM]
proof assume not x in still_not-bound_in VERUM;
thus for v,w st for y st x<>y holds w.y = v.y holds
Valid(VERUM,J).v = Valid(VERUM,J).w
proof let v,w such that
for y st x <> y holds w.y = v.y;
Valid(VERUM,J).v = TRUE & Valid(VERUM,J).w = TRUE by Th14;
hence Valid(VERUM,J).v = Valid(VERUM,J).w;
end;
end;
thus PP[P!ll]
proof
assume A3: not x in still_not-bound_in (P!ll);
thus for v,w st for y st x<>y holds w.y = v.y holds
Valid(P!ll,J).v = Valid(P!ll,J).w
proof let v,w such that
A4: for y st x <> y holds w.y = v.y;
A5: now assume
A6: Valid(P!ll,J).v = TRUE;
then (ll 'in' (J.P)).v = TRUE by Lm1;
then not (ll 'in' (J.P)).v = FALSE by MARGREL1:43;
then A7: v*'ll in (J.P) by Def9;
A8: len (v*'ll) = k & len (w*'ll) = k by Def8;
now let i; assume
A9: 1 <= i & i <= len (v*'ll);
then A10: (v*'ll).i = v.(ll.i) by A8,Def8;
A11: len (v*'ll) = len ll by A8,QC_LANG1:def 8;
A12: ll.i in bound_QC-variables
proof
i in dom ll by A9,A11,FINSEQ_3:27;
then ll.i in rng ll by FUNCT_1:def 5;
hence ll.i in bound_QC-variables by A2;
end;
A13: ll.i <> x
proof
reconsider M = still_not-bound_in ll as set;
not x in M by A3,QC_LANG3:9;
then not x in variables_in(ll,bound_QC-variables) by
QC_LANG3:6;
then not x in {ll.i2 where i2 is Nat : 1 <= i2 & i2 <=
len ll &
ll.i2 in bound_QC-variables} by QC_LANG3:def
2;
hence ll.i <> x by A9,A11;
end;
reconsider z = ll.i as bound_QC-variable by A12;
w.z = v.z by A4,A13;
hence (v*'ll).i = (w*'ll).i by A8,A9,A10,Def8;
end;
then w*'ll in (J.P) by A7,A8,FINSEQ_1:18;
then (ll 'in' (J.P)).w = TRUE by Def9;
hence thesis by A6,Lm1;
end;
now assume
A14: Valid(P!ll,J).v = FALSE;
then (ll 'in' (J.P)).v = FALSE by Lm1;
then not (ll 'in' (J.P)).v = TRUE by MARGREL1:43;
then A15: not v*'ll in (J.P) by Def9;
A16: len (v*'ll) = k & len (w*'ll) = k by Def8;
now let i; assume
A17: 1 <= i & i <= len (v*'ll);
then A18: (v*'ll).i = v.(ll.i) by A16,Def8;
A19: len (v*'ll) = len ll by A16,QC_LANG1:def 8;
A20: ll.i in bound_QC-variables
proof
i in dom ll by A17,A19,FINSEQ_3:27;
then ll.i in rng ll by FUNCT_1:def 5;
hence ll.i in bound_QC-variables by A2;
end;
A21: ll.i <> x
proof
reconsider M = still_not-bound_in ll as set;
not x in M by A3,QC_LANG3:9;
then not x in variables_in(ll,bound_QC-variables) by
QC_LANG3:6;
then not x in {ll.i2 where i2 is Nat : 1 <= i2 & i2 <=
len ll &
ll.i2 in bound_QC-variables} by QC_LANG3:def
2;
hence ll.i <> x by A17,A19;
end;
reconsider z = ll.i as bound_QC-variable by A20;
w.z = v.z by A4,A21;
hence (v*'ll).i = (w*'ll).i by A16,A17,A18,Def8;
end;
then not w*'ll in (J.P) by A15,A16,FINSEQ_1:18;
then (ll 'in' (J.P)).w = FALSE by Def9;
hence thesis by A14,Lm1;
end;
hence thesis by A5,MARGREL1:39;
end;
end;
thus PP[s] implies PP['not' s]
proof
assume that
A22: not x in still_not-bound_in s implies
for v,w st for y st x<>y holds w.y = v.y holds
Valid(s,J).v = Valid(s,J).w
and
A23: not x in still_not-bound_in 'not' s;
thus for v,w st for y st x<>y holds w.y = v.y holds
Valid('not' s,J).v = Valid('not' s,J).w
proof let v,w such that
A24: for y st x<>y holds w.y = v.y;
A25: now assume
A26: Valid('not' s,J).v = TRUE;
then 'not'(Valid(s,J).v) = TRUE by Th20;
then Valid(s,J).v = FALSE by MARGREL1:41;
then Valid(s,J).w = FALSE by A22,A23,A24,QC_LANG3:11;
then 'not'(Valid(s,J).w) = TRUE by MARGREL1:41;
hence thesis by A26,Th20;
end;
now assume
A27: Valid('not' s,J).v = FALSE;
then 'not'(Valid(s,J).v) = FALSE by Th20;
then Valid(s,J).v = TRUE by MARGREL1:41;
then Valid(s,J).w = TRUE by A22,A23,A24,QC_LANG3:11;
then 'not'(Valid(s,J).w) = FALSE by MARGREL1:41;
hence thesis by A27,Th20;
end;
hence thesis by A25,MARGREL1:39;
end;
end;
thus PP[s] & PP[t] implies PP[s '&' t]
proof
assume that
A28: not x in still_not-bound_in s implies
for v,w st for y st x<>y holds w.y = v.y holds
Valid(s,J).v = Valid(s,J).w
and
A29: not x in still_not-bound_in t implies
for v,w st for y st x<>y holds w.y = v.y holds
Valid(t,J).v = Valid(t,J).w
and
A30: not x in still_not-bound_in s '&' t;
A31: not (x in (still_not-bound_in s) \/ (still_not-bound_in t))
by A30,QC_LANG3:14;
thus for v,w st for y st x<>y holds w.y = v.y holds
Valid(s '&' t ,J).v = Valid(s '&' t, J).w
proof let v,w such that
A32: for y st x<>y holds w.y = v.y;
A33: now assume
A34: Valid(s '&' t ,J).v = TRUE;
then (Valid(s,J).v) '&' (Valid(t,J).v) = TRUE by Th22;
then Valid(s,J).v = TRUE & Valid(t,J).v = TRUE by MARGREL1:45;
then Valid(s,J).w = TRUE & Valid(t,J).w = TRUE by A28,A29,A31,A32
,XBOOLE_0:def 2;
then (Valid(s,J).w) '&' (Valid(t,J).w) = TRUE by MARGREL1:45;
hence thesis by A34,Th22;
end;
now assume
A35: Valid(s '&' t ,J).v = FALSE;
then A36: (Valid(s,J).v) '&' (Valid(t,J).v) = FALSE by Th22;
A37: now assume Valid(s,J).v = FALSE;
then Valid(s,J).w = FALSE by A28,A31,A32,XBOOLE_0:def 2;
then (Valid(s,J).w) '&' (Valid(t,J).w) = FALSE by MARGREL1:45;
hence thesis by A35,Th22;
end;
now assume Valid(t,J).v = FALSE;
then Valid(t,J).w = FALSE by A29,A31,A32,XBOOLE_0:def 2;
then (Valid(s,J).w) '&' (Valid(t,J).w) = FALSE by MARGREL1:45;
hence thesis by A35,Th22;
end;
hence thesis by A36,A37,MARGREL1:45;
end;
hence thesis by A33,MARGREL1:39;
end;
end;
thus PP[s] implies PP[All(y,s)]
proof
assume that
A38: not x in still_not-bound_in s implies
for v,w st for y st x<>y holds w.y = v.y holds
Valid(s,J).v = Valid(s,J).w
and
A39: not x in still_not-bound_in All(y,s);
A40: not (x in (still_not-bound_in s) \ {y}) by A39,QC_LANG3:16;
thus for v,w st for z st x<>z holds w.z = v.z holds
Valid(All(y,s),J).v = Valid(All(y,s),J).w
proof let v,w such that
A41: for z st x<>z holds w.z = v.z;
A42: now assume
A43: Valid(All(y,s),J).v = TRUE;
then A44: FOR_ALL(y,Valid(s,J)).v = TRUE by Lm1;
for v1 st for z st y<>z holds v1.z = w.z holds
Valid(s,J).v1 = TRUE
proof let v1 such that
A45: for z st y<>z holds v1.z = w.z;
A46: now assume
A47: not x in (still_not-bound_in s);
consider v2 such that
A48: (for z st z <> y holds v2.z = v.z) &
v2.y = v1.y from Lambda_Val;
A49: for z st x <> z holds v2.z = v1.z
proof let z such that A50: x <> z;
now assume A51: z <> y; hence
v2.z = v.z by A48
.= w.z by A41,A50
.= v1.z by A45,A51;
end;
hence thesis by A48;
end;
Valid(s,J).v2 = TRUE by A44,A48,Th8;
hence Valid(s,J).v1 = TRUE by A38,A47,A49;
end;
now assume x in {y};
then A52: x = y by TARSKI:def 1;
for z st y <> z holds v1.z = v.z
proof let z; assume A53: y <> z;
hence v.z = w.z by A41,A52
.= v1.z by A45,A53;
end;
hence Valid(s,J).v1 = TRUE by A44,Th8;
end;
hence Valid(s,J).v1 = TRUE by A40,A46,XBOOLE_0:def 4;
end;
then FOR_ALL(y,Valid(s,J)).w = TRUE by Th8;
hence thesis by A43,Lm1;
end;
now assume
A54: Valid(All(y,s),J).v = FALSE;
then FOR_ALL(y,Valid(s,J)).v = FALSE by Lm1;
then consider v1 such that
A55: Valid(s,J).v1 = FALSE and
A56: for z st y <> z holds v1.z = v.z by Th7;
ex v2 st Valid(s,J).v2 = FALSE & for z st y<>z holds v2.z = w.z
proof
A57: now assume
A58: not x in (still_not-bound_in s);
consider v2 such that
A59: (for z st z <> y holds v2.z = w.z) &
v2.y = v1.y from Lambda_Val;
take v2;
for z st x <> z holds v2.z = v1.z
proof let z such that A60: x <> z;
now assume A61: z <> y; hence
v2.z = w.z by A59
.= v.z by A41,A60
.= v1.z by A56,A61;
end;
hence thesis by A59;
end;
hence Valid(s,J).v2 = FALSE by A38,A55,A58;
thus for z st y <> z holds v2.z = w.z by A59;
end;
now assume A62: x in {y};
take v2 = v1;
thus Valid(s,J).v2 = FALSE by A55;
for z st y <> z holds v1.z = w.z
proof let z; assume
A63: y <> z;
then A64: x <> z by A62,TARSKI:def 1;
thus v1.z = v.z by A56,A63
.= w.z by A41,A64;
end;
hence for z st y <> z holds v2.z = w.z;
end;
hence ex v2 st Valid(s,J).v2 = FALSE &
for z st y<>z holds v2.z = w.z by A40,A57,XBOOLE_0:def 4;
end;
then FOR_ALL(y,Valid(s,J)).w = FALSE by Th7;
hence thesis by A54,Lm1;
end;
hence thesis by A42,MARGREL1:39;
end;
end;
end;
for s holds PP[s] from CQC_Ind(A1);
hence thesis;
end;
theorem
Th40:
J,v |= p & not x in still_not-bound_in p implies
for w st for y st x<>y holds w.y = v.y holds J,w |= p
proof
assume that
A1: J,v |= p and
A2: not x in still_not-bound_in p;
now let w;
assume A3: for y st x<>y holds w.y = v.y;
Valid(p,J).v = TRUE by A1,Def12;
then Valid(p,J).w = TRUE by A2,A3,Th39;
hence J,w |= p by Def12;
end;
hence thesis;
end;
theorem
Th41:
J,v |= All(x,p) iff
for w st for y st x<>y holds w.y = v.y holds J,w |= p
proof
A1: now assume
A2: J,v |= All(x,p);
let w;
assume for y st x<>y holds w.y = v.y;
then Valid(p,J).w = TRUE by A2,Th31;
hence J,w |= p by Def12;
end;
now assume
A3: for w st for y st x<>y holds w.y = v.y holds J,w |= p;
for w st for y st x<>y holds w.y = v.y holds Valid(p,J).w = TRUE
proof let w;
assume for y st x<>y holds w.y = v.y;
then J,w |= p by A3;
hence Valid(p,J).w = TRUE by Def12;
end;
hence J,v |= All(x,p) by Th31;
end;
hence thesis by A1;
end;
reserve u,w for Element of Valuations_in A;
reserve s' for QC-formula;
theorem
Th42:
x <> y & p = s'.x & q = s'.y implies for v st v.x = v.y holds
Valid(p,J).v = Valid(q,J).v
proof
defpred PP[Element of QC-WFF] means
for x,y,p,q st x <> y & p = $1.x & q = $1.y holds
for v st v.x = v.y holds Valid(p,J).v = Valid(q,J).v;
A1: now
let s be Element of QC-WFF;
thus s is atomic implies PP[s]
proof assume
A2: s is atomic;
thus for x,y,p,q st x <> y & p = s.x & q = s.y holds
for v st v.x = v.y holds Valid(p,J).v = Valid(q,J).v
proof let x,y,p,q such that
A3: x <> y & p = s.x & q = s.y;
let v such that
A4: v.x = v.y;
consider k being Nat, P being (QC-pred_symbol of k),
l being QC-variable_list of k such that
A5: s = P!l by A2,QC_LANG1:def 17;
A6: p = P!Subst(l, a.0 .-->x) & q = P!Subst(l, a.0 .-->y)
by A3,A5,CQC_LANG:30;
set lx = Subst(l, a.0 .-->x),
ly = Subst(l, a.0 .-->y);
A7: {lx.i : 1 <= i & i <= len lx & lx.i in free_QC-variables} = {} &
{lx.j : 1 <= j & j <= len lx & lx.j in fixed_QC-variables} = {}
by A6,CQC_LANG:17;
{ly.i : 1 <= i & i <= len ly & ly.i in free_QC-variables} = {} &
{ly.j : 1 <= j & j <= len ly & ly.j in fixed_QC-variables} = {}
by A6,CQC_LANG:17;
then reconsider lx,ly as CQC-variable_list of k by A7,CQC_LANG:15;
A8: len (v*'lx) = k &
for i st 1 <= i & i <= k holds (v*'lx).i = v.(lx.i) by Def8;
A9: len (v*'ly) = k &
for i st 1 <= i & i <= k holds (v*'ly).i = v.(ly.i) by Def8;
A10: v*'lx = v*'ly
proof
now let i; assume
A11: 1 <= i & i <= len (v*'lx);
then A12: 1 <= i & i <= len l by A8,QC_LANG1:def 8;
A13: now assume l.i <> a.0;
then A14: lx.i = l.i & ly.i = l.i by A12,CQC_LANG:11;
v.(lx.i) = (v*'lx).i & v.(ly.i) = (v*'ly).i by A8,A11,Def8;
hence (v*'lx).i = (v*'ly).i by A14;
end;
now assume l.i = a.0;
then A15: lx.i = x & ly.i = y by A12,CQC_LANG:11;
v.(lx.i) = (v*'lx).i & v.(ly.i) = (v*'ly).i by A8,A11,Def8;
hence (v*'lx).i = (v*'ly).i by A4,A15;
end;
hence (v*'lx).i = (v*'ly).i by A13;
end;
hence thesis by A8,A9,FINSEQ_1:18;
end;
A16: now assume
Valid(p,J).v = TRUE;
then v*'lx in J.P by A6,Th16;
hence Valid(q,J).v = TRUE by A6,A10,Th16;
end;
now assume
Valid(p,J).v = FALSE;
then not (v*'lx in J.P) by A6,Th17;
hence Valid(q,J).v = FALSE by A6,A10,Th17;
end;
hence thesis by A16,MARGREL1:39;
end;
end;
thus PP[VERUM]
proof let x,y,p,q such that
A17: x <> y & p = VERUM.x & q = VERUM.y;
let v such that v.x = v.y;
p = VERUM & q = VERUM by A17,CQC_LANG:28;
hence thesis;
end;
thus s is negative & PP[the_argument_of s] implies PP[s]
proof assume that
A18: s is negative and
A19: for x,y,p,q st x <> y & p = (the_argument_of s).x &
q = (the_argument_of s).y
holds for v st v.x = v.y holds Valid(p,J).v = Valid(q,J).v;
thus for x,y,p,q st x <> y & p = s.x & q = s.y holds
for v st v.x = v.y holds Valid(p,J).v = Valid(q,J).v
proof let x,y,p,q such that
A20: x <> y & p = s.x & q = s.y;
let v such that
A21: v.x = v.y;
A22: s.x = 'not'((the_argument_of s).x) & s.y = 'not'
((the_argument_of s).y)
by A18,CQC_LANG:31;
then reconsider pa = (the_argument_of s).x as Element of CQC-WFF by
A20,CQC_LANG:18;
reconsider qa = (the_argument_of s).y as Element of CQC-WFF by A20,A22
,CQC_LANG:18;
A23: now assume
Valid(p,J).v = TRUE;
then 'not'(Valid(pa,J).v) = TRUE by A20,A22,Th20;
then Valid(pa,J).v = FALSE by MARGREL1:41;
then Valid(qa,J).v = FALSE by A19,A21;
then 'not'(Valid(qa,J).v) = TRUE by MARGREL1:41;
hence Valid(q,J).v = TRUE by A20,A22,Th20;
end;
now assume
Valid(p,J).v = FALSE;
then 'not'(Valid(pa,J).v) = FALSE by A20,A22,Th20;
then Valid(pa,J).v = TRUE by MARGREL1:41;
then Valid(qa,J).v = TRUE by A19,A21;
then 'not'(Valid(qa,J).v) = FALSE by MARGREL1:41;
hence Valid(q,J).v = FALSE by A20,A22,Th20;
end;
hence thesis by A23,MARGREL1:39;
end;
end;
thus (s is conjunctive & PP[the_left_argument_of s] &
PP[the_right_argument_of s]) implies PP[s]
proof assume that
A24: s is conjunctive and
A25: for x,y,p,q st x <> y & p = (the_left_argument_of s).x &
q = (the_left_argument_of s).y holds
for v st v.x = v.y holds Valid(p,J).v = Valid(q,J).v
and
A26: for x,y,p,q st x <> y & p = (the_right_argument_of s).x &
q = (the_right_argument_of s).y
holds for v st v.x = v.y holds Valid(p,J).v = Valid(q,J).v;
thus for x,y,p,q st x <> y & p = s.x & q = s.y holds
for v st v.x = v.y holds Valid(p,J).v = Valid(q,J).v
proof let x,y,p,q such that
A27: x <> y & p = s.x & q = s.y;
let v such that
A28: v.x = v.y;
A29: s.x=((the_left_argument_of s).x) '&' ((the_right_argument_of s).x) &
s.y=((the_left_argument_of s).y) '&' ((the_right_argument_of s).y)
by A24,CQC_LANG:33;
then reconsider pla = (the_left_argument_of s).x ,
pra = (the_right_argument_of s).x as Element of CQC-WFF
by A27,CQC_LANG:19;
reconsider qla = (the_left_argument_of s).y ,
qra = (the_right_argument_of s).y as Element of CQC-WFF
by A27,A29,CQC_LANG:19;
A30: now assume
Valid(p,J).v = TRUE;
then (Valid(pla,J).v) '&' (Valid(pra,J).v) = TRUE by A27,A29,Th22
;
then Valid(pla,J).v = TRUE & Valid(pra,J).v = TRUE by MARGREL1:45
;
then Valid(qla,J).v = TRUE & Valid(qra,J).v = TRUE by A25,A26,A28
;
then (Valid(qla,J).v) '&' (Valid(qra,J).v) = TRUE by MARGREL1:45;
hence Valid(q,J).v = TRUE by A27,A29,Th22;
end;
now assume
A31: Valid(p,J).v = FALSE;
then A32: (Valid(pla,J).v) '&' (Valid(pra,J).v) = FALSE by A27,A29,
Th22
;
A33: now assume Valid(pla,J).v = FALSE;
then Valid(qla,J).v = FALSE by A25,A28;
then (Valid(qla,J).v) '&' (Valid(qra,J).v) = FALSE by MARGREL1:
45;
hence thesis by A27,A29,A31,Th22;
end;
now assume Valid(pra,J).v = FALSE;
then Valid(qra,J).v = FALSE by A26,A28;
then (Valid(qla,J).v) '&' (Valid(qra,J).v) = FALSE by MARGREL1:
45;
hence thesis by A27,A29,A31,Th22;
end;
hence thesis by A32,A33,MARGREL1:45;
end;
hence thesis by A30,MARGREL1:39;
end;
end;
thus s is universal & PP[the_scope_of s] implies PP[s]
proof assume that
A34: s is universal and
A35: for x,y,p,q st x<>y & p = (the_scope_of s).x & q = (the_scope_of s).y
holds for v st v.x = v.y holds Valid(p,J).v = Valid(q,J).v;
consider xx being bound_QC-variable, pp being Element of QC-WFF such that
A36: s = All(xx,pp) by A34,QC_LANG1:def 20;
A37: xx = bound_in s by A34,A36,QC_LANG1:def 26;
thus for x,y,p,q st x <> y & p = s.x & q = s.y holds
for v st v.x = v.y holds Valid(p,J).v = Valid(q,J).v
proof let x,y,p,q such that
A38: x <> y & p = s.x & q = s.y;
let v such that
A39: v.x = v.y;
A40: now assume
A41: x <> bound_in s;
then s.x = All(bound_in s, (the_scope_of s).x) by A34,CQC_LANG:36;
then reconsider ps = (the_scope_of s).x as Element of CQC-WFF by A38,CQC_LANG:
23;
A42: All(bound_in s, ps) = p by A34,A38,A41,CQC_LANG:36;
A43: now assume
A44: y <> bound_in s;
then s.y = All(bound_in s, (the_scope_of s).y) by A34,CQC_LANG:36;
then reconsider qs = (the_scope_of s).y as Element of CQC-WFF by A38
,CQC_LANG:23;
A45: All(bound_in s, qs) = q by A34,A38,A44,CQC_LANG:36;
A46: Valid(All(bound_in s, ps),J) = FOR_ALL(bound_in s, Valid(ps,J)) &
Valid(All(bound_in s, qs),J) = FOR_ALL(bound_in s, Valid(qs,J))
by Lm1;
A47: now assume
A48: Valid(p,J).v = TRUE;
for v1 st for y st (bound_in s) <> y holds v1.y = v.y holds
Valid(qs,J).v1 = TRUE
proof let v1; assume
A49: for y st (bound_in s) <> y holds v1.y = v.y;
then A50: v1.x = v.x & v1.y = v.y by A41,A44;
Valid(ps,J).v1 = TRUE by A42,A46,A48,A49,Th8;
hence Valid(qs,J).v1 = TRUE by A35,A39,A50;
end;
hence Valid(q,J).v = TRUE by A45,A46,Th8;
end;
now assume
A51: Valid(p,J).v = FALSE;
ex v1 st Valid(qs,J).v1 = FALSE &
for y st (bound_in s) <> y holds v1.y = v.y
proof
consider v1 such that
A52: Valid(ps,J).v1 = FALSE and
A53: for y st (bound_in s) <> y holds v1.y = v.y by A42,A46,A51,
Th7;
v1.x = v.x & v1.y = v.y by A41,A44,A53;
then Valid(qs,J).v1 = FALSE by A35,A39,A52;
hence thesis by A53;
end;
hence Valid(q,J).v = FALSE by A45,A46,Th7;
end;
hence thesis by A47,MARGREL1:39;
end;
now assume
A54: y = bound_in s;
then q = All(y,pp) by A36,A37,A38,CQC_LANG:37;
hence thesis by A36,A37,A38,A54,CQC_LANG:40;
end;
hence thesis by A43;
end;
now assume
A55: x = bound_in s;
then p = All(x,pp) by A36,A37,A38,CQC_LANG:37;
hence thesis by A36,A37,A38,A55,CQC_LANG:40;
end;
hence thesis by A40;
end;
end;
end;
for s being Element of QC-WFF holds PP[s] from QC_Ind2 (A1);
hence thesis;
end;
theorem
Th43:
x <> y & not x in still_not-bound_in s' implies
not x in still_not-bound_in (s'.y)
proof
defpred PP[Element of QC-WFF] means
x <> y & not x in still_not-bound_in ($1) implies
not x in still_not-bound_in ($1.y);
A1: now
let s be Element of QC-WFF;
thus s is atomic implies PP[s]
proof assume that
A2: s is atomic and
A3: x <> y & not x in still_not-bound_in s;
thus not x in still_not-bound_in (s.y)
proof
set l = the_arguments_of s;
A4: still_not-bound_in s = still_not-bound_in l by A2,QC_LANG3:8
.= variables_in(l, bound_QC-variables) by QC_LANG3:6
.={l.k : 1<=k & k<=len l & l.k in bound_QC-variables} by QC_LANG3:
def 2;
A5: s.y = (the_pred_symbol_of s)!Subst(l,a.0 .-->y) by A2,CQC_LANG:29;
set ll = Subst(l,a.0 .-->y);
A6: s.y is atomic & the_arguments_of s.y = ll
proof
consider k being Nat, p being (QC-pred_symbol of k),
l2 being QC-variable_list of k such that
A7: s = p!l2 by A2,QC_LANG1:def 17;
l2 = l by A2,A7,QC_LANG1:def 22;
then len l = k by QC_LANG1:def 8;
then len (Subst(l,a.0 .-->y)) = k by CQC_LANG:def 3;
then reconsider l3 = Subst(l,a.0 .-->y)
as QC-variable_list of k by QC_LANG1:def 8;
A8: s.y = p!l3 by A2,A5,A7,QC_LANG1:def 21;
hence
s.y is atomic by QC_LANG1:def 17;
hence ll = the_arguments_of s.y by A8,QC_LANG1:def 22;
end;
then A9: still_not-bound_in the_arguments_of s.y =
variables_in(ll, bound_QC-variables) by QC_LANG3:6
.={ll.k : 1<=k & k<=
len ll & ll.k in bound_QC-variables} by QC_LANG3:def 2;
x in {ll.k : 1 <= k & k <= len ll & ll.k in bound_QC-variables}
implies
x in {l.i : 1 <= i & i <= len l & l.i in bound_QC-variables}
proof assume
x in {ll.k : 1 <= k & k <= len ll & ll.k in bound_QC-variables};
then consider k such that
A10: x = ll.k & 1 <= k & k <= len ll & ll.k in bound_QC-variables;
A11: 1 <= k & k <= len l by A10,CQC_LANG:def 3;
then l.k <> a.0 by A3,A10,CQC_LANG:11;
then x = l.k & l.k in bound_QC-variables by A10,A11,CQC_LANG:11;
hence x in {l.i : 1 <= i & i <=
len l & l.i in bound_QC-variables} by A11
;
end;
hence thesis by A3,A4,A6,A9,QC_LANG3:8;
end;
end;
thus PP[VERUM] by CQC_LANG:28;
thus s is negative & PP[the_argument_of s] implies PP[s]
proof assume that
A12: s is negative and
A13: x <> y & not x in still_not-bound_in (the_argument_of s)
implies not x in still_not-bound_in ((the_argument_of s).y)
and
A14: x <> y & not x in still_not-bound_in s;
not x in
still_not-bound_in 'not'((the_argument_of s).y) by A12,A13,A14,QC_LANG3:10,11;
hence not x in still_not-bound_in (s.y) by A12,CQC_LANG:31;
end;
thus (s is conjunctive & PP[the_left_argument_of s] &
PP[the_right_argument_of s]) implies PP[s]
proof assume that
A15: s is conjunctive and
A16: x <> y & not x in still_not-bound_in (the_left_argument_of s)
implies not x in still_not-bound_in ((the_left_argument_of s).y)
and
A17: x <> y & not x in still_not-bound_in (the_right_argument_of s)
implies not x in still_not-bound_in ((the_right_argument_of s).y)
and
A18: x <> y & not x in still_not-bound_in s;
still_not-bound_in s = (still_not-bound_in (the_left_argument_of s)) \/
(still_not-bound_in (the_right_argument_of s)) by A15,QC_LANG3:13;
then not x in still_not-bound_in ((the_left_argument_of s).y) \/
still_not-bound_in ((the_right_argument_of s).y) by A16,A17,A18,
XBOOLE_0:def 2;
then not x in (still_not-bound_in ((the_left_argument_of s).y) '&'
((the_right_argument_of s).y)) by QC_LANG3:14;
hence not x in still_not-bound_in (s.y) by A15,CQC_LANG:33;
end;
thus s is universal & PP[the_scope_of s] implies PP[s]
proof assume that
A19: s is universal and
A20: x <> y & not x in still_not-bound_in (the_scope_of s)
implies not x in still_not-bound_in ((the_scope_of s).y)
and
A21: x <> y & not x in still_not-bound_in s;
A22: still_not-bound_in s =
still_not-bound_in (the_scope_of s) \ {bound_in s} by A19,QC_LANG3:15;
thus not x in still_not-bound_in (s.y)
proof
A23: now assume not x in still_not-bound_in (the_scope_of s);
then not x in still_not-bound_in ((the_scope_of s).y) \ {bound_in s}
by A20,A21,XBOOLE_0:
def 4
;
then not x in still_not-bound_in All(bound_in s,(the_scope_of s).y)
by QC_LANG3:16;
then y <> bound_in s implies not x in still_not-bound_in (s.y) by A19,
CQC_LANG:36;
hence thesis by A19,A21,CQC_LANG:35;
end;
now assume x in {bound_in s};
then A24: x = bound_in s by TARSKI:def 1;
still_not-bound_in All(x,(the_scope_of s).y) =
still_not-bound_in ((the_scope_of s).y) \ {x} by QC_LANG3:16;
then not x in still_not-bound_in All(x,(the_scope_of s).y) iff
not x in still_not-bound_in ((the_scope_of s).y) or x in {x}
by XBOOLE_0:def 4;
hence not x in still_not-bound_in (s.y)
by A19,A21,A24,CQC_LANG:36,TARSKI:def 1;
end;
hence thesis by A21,A22,A23,XBOOLE_0:def 4;
end;
end;
end;
for s being Element of QC-WFF holds PP[s] from QC_Ind2 (A1);
hence thesis;
end;
theorem
Th44: J,v |= VERUM
proof
(Valuations_in A --> TRUE).v = TRUE by FUNCOP_1:13;
then (Valid(VERUM,J)).v = TRUE by Lm1;
hence J,v |= VERUM by Def12;
end;
theorem
Th45: J,v |= p '&' q => q '&' p
proof
thus Valid(p '&' q => q '&' p, J).v = TRUE
proof assume
not (Valid(p '&' q => q '&' p, J).v = TRUE);
then A1: Valid(p '&' q => q '&' p, J).v = FALSE by MARGREL1:43;
Valid(p '&' q => q '&' p, J).v = Valid('not'((p '&' q) '&' 'not'
(q '&' p)), J).v
by QC_LANG2:def 2
.= 'not'(Valid(((p '&' q) '&' 'not'(q '&' p)), J).v) by Th20
.= 'not'((Valid(p '&' q, J).v) '&' (Valid('not'
(q '&' p), J).v)) by Th22
.= 'not'((Valid(p '&' q, J).v) '&' 'not'
(Valid(q '&' p, J).v)) by Th20
;
then (Valid(p '&' q, J).v) '&' 'not'(Valid(q '&' p, J).v) = TRUE by A1,
MARGREL1:41;
then Valid(p '&' q, J).v=TRUE & 'not'
(Valid(q '&' p, J).v) = TRUE by MARGREL1:45;
then Valid(p '&' q, J).v = TRUE & Valid(q '&' p, J).v = FALSE by MARGREL1
:41;
then (Valid(p, J).v) '&' (Valid(q, J).v) = TRUE &
(Valid(q, J).v) '&' (Valid(p, J).v) = FALSE by Th22;
hence thesis by MARGREL1:38;
end;
end;
theorem
Th46: J,v |= ('not' p => p) => p
proof
thus Valid(('not' p => p) => p, J).v = TRUE
proof
'not' p => p = 'not'('not' p '&' 'not' p) by QC_LANG2:def 2;
then A1: Valid(('not' p => p) => p, J).v =
Valid('not'('not'('not' p '&' 'not'
p) '&' 'not' p), J).v by QC_LANG2:def 2
.= 'not'(Valid('not'('not' p '&' 'not' p) '&' 'not' p, J).v) by Th20
.= 'not'((Valid('not'('not' p '&' 'not' p), J).v) '&' (Valid('not'
p, J).v)) by Th22;
Valid('not'('not' p '&' 'not' p), J).v = 'not'(Valid('not' p '&' 'not'
p, J).v) by Th20
.= 'not'(Valid('not' p, J).v) by Th33
.= 'not' 'not'(Valid(p, J).v) by Th20
.= Valid(p, J).v by MARGREL1:40;
hence
Valid(('not' p => p) => p, J).v='not'((Valid(p, J).v) '&' 'not'
(Valid(p, J).v)) by A1,Th20
.= TRUE by MARGREL1:47;
end;
end;
theorem
Th47: J,v |= p => ('not' p => q)
proof
thus Valid(p => ('not' p => q), J).v = TRUE
proof
'not' p => q = 'not'('not' p '&' 'not' q) by QC_LANG2:def 2;
then A1: Valid(p => ('not' p => q), J).v =
Valid('not'(p '&' 'not'('not'('not' p '&'
'not' q))), J).v by QC_LANG2:def 2
.= 'not'(Valid((p '&' 'not'('not'('not' p '&' 'not' q))), J).v) by Th20
.= 'not'((Valid(p,J).v) '&' (Valid('not'('not'('not' p '&' 'not'
q)), J).v)) by Th22;
Valid('not'('not'('not' p '&' 'not' q)), J).v =
'not'(Valid('not'('not'
p '&' 'not' q), J).v) by Th20
.= 'not' 'not'(Valid('not' p '&' 'not' q, J).v) by Th20
.= (Valid('not' p '&' 'not' q, J).v) by MARGREL1:40
.= (Valid('not' p, J).v) '&' (Valid('not' q, J).v) by Th22
.= 'not'(Valid(p, J).v) '&' (Valid('not' q, J).v) by Th20
.= 'not'(Valid(p, J).v) '&' 'not'(Valid(q, J).v) by Th20;
then A2: Valid(p => ('not' p => q), J).v =
'not'(((Valid(p,J).v) '&' 'not'(Valid(p, J).v)) '&' 'not'(Valid(q, J).v))
by A1,MARGREL1:52
.= 'not'(FALSE '&' 'not'(Valid(q, J).v)) by MARGREL1:46;
FALSE '&' 'not'(Valid(q, J).v) = FALSE by MARGREL1:49;
hence Valid(p => ('not' p => q), J).v = TRUE by A2,MARGREL1:41;
end;
end;
theorem
Th48: J,v |= (p => q) => ('not'(q '&' t) => 'not'(p '&' t))
proof
thus Valid((p => q) => ('not'(q '&' t) => 'not'(p '&' t)), J).v = TRUE
proof
A1: p => q = 'not'(p '&' 'not' q) by QC_LANG2:def 2;
'not'(q '&' t) => 'not'(p '&' t) = 'not'('not'(q '&' t) '&'
'not' 'not' (p '&' t)) by QC_LANG2:def 2;
then A2: Valid((p => q) => ('not'(q '&' t) => 'not'(p '&' t)), J).v =
Valid('not'('not'(p '&' 'not' q) '&' 'not'('not'('not'(q '&' t) '&'
'not' 'not'(p '&' t)))), J).v by A1,QC_LANG2:def 2
.= 'not'(Valid('not'(p '&' 'not' q) '&' 'not'('not'('not'(q '&' t) '&'
'not' 'not'(p '&' t))), J).v)
by Th20
.= 'not'((Valid('not'(p '&' 'not' q), J).v) '&'
(Valid('not'('not'('not'(q '&' t) '&' 'not' 'not'
(p '&' t))), J).v)) by Th22;
A3: Valid('not'(p '&' 'not' q), J).v = 'not'(Valid(p '&' 'not' q, J).v)
by Th20
.= 'not'((Valid(p, J).v) '&' (Valid('not' q, J).v)) by Th22
.= 'not'((Valid(p, J).v) '&'('not'(Valid(q, J).v))) by Th20;
Valid('not'('not'('not'(q '&' t) '&' 'not' 'not'(p '&' t))), J).v =
'not'(Valid('not'('not'(q '&' t) '&' 'not' 'not'
(p '&' t)), J).v) by Th20
.= 'not' 'not'(Valid('not'(q '&' t) '&' 'not' 'not'
(p '&' t), J).v) by Th20
.= Valid('not'(q '&' t) '&' 'not' 'not'(p '&' t), J).v
by MARGREL1:40
.= (Valid('not'(q '&' t),J).v) '&' (Valid('not' 'not'
(p '&' t), J).v) by Th22
.= 'not'(Valid(q '&' t,J).v) '&' (Valid('not' 'not'
(p '&' t), J).v) by Th20
.= 'not'(Valid(q '&' t,J).v) '&'('not'(Valid('not'
(p '&' t), J).v)) by Th20
.= 'not'(Valid(q '&' t,J).v) '&'('not' 'not'
(Valid(p '&' t, J).v)) by Th20
.= 'not'(Valid(q '&' t,J).v) '&'(Valid(p '&' t, J).v) by MARGREL1:40
.= 'not'((Valid(q,J).v) '&' (Valid(t,J).v)) '&'
(Valid(p '&' t, J).v) by Th22
.= 'not'((Valid(q,J).v) '&' (Valid(t,J).v)) '&'
((Valid(p,J).v) '&' (Valid(t,J).v)) by Th22;
hence Valid((p => q) => ('not'(q '&' t) => 'not'
(p '&' t)), J).v =TRUE by A2,A3,Lm2;
end;
end;
theorem
J,v |= p & J,v |= (p => q) implies J,v |= q by Th36;
theorem
Th50: J,v |= All(x,p) => p
proof
thus Valid(All(x,p) => p, J).v = TRUE
proof assume
not (Valid(All(x,p) => p, J).v = TRUE);
then A1: Valid(All(x,p) => p, J).v = FALSE by MARGREL1:43;
Valid(All(x,p) => p , J).v = Valid('not'(All(x,p) '&' 'not'
p), J).v by QC_LANG2:def 2
.= 'not'(Valid(All(x,p) '&' 'not' p, J).v) by Th20
.= 'not'((Valid(All(x,p), J).v) '&' (Valid('not' p, J).v)) by Th22
.= 'not'((Valid(All(x,p), J).v) '&' 'not'
(Valid(p, J).v)) by Th20;
then (Valid(All(x,p), J).v) '&' 'not'(Valid(p, J).v) = TRUE by A1,
MARGREL1:41;
then A2: Valid(All(x,p), J).v=TRUE & 'not'
(Valid(p, J).v) = TRUE by MARGREL1:45;
then A3: Valid(All(x,p), J).v = TRUE & Valid(p, J).v = FALSE by MARGREL1:41;
FOR_ALL(x, Valid(p,J)).v = TRUE by A2,Lm1;
hence thesis by A3,Th37,MARGREL1:38;
end;
end;
theorem
J |= VERUM
proof let v;
thus thesis by Th44;
end;
theorem
J |= p '&' q => q '&' p
proof let v;
thus thesis by Th45;
end;
theorem
J |= ('not' p => p) => p
proof let v;
thus thesis by Th46;
end;
theorem
J |= p => ('not' p => q)
proof let v;
thus thesis by Th47;
end;
theorem
J |= (p => q) => ('not'(q '&' t) => 'not'(p '&' t))
proof let v;
thus thesis by Th48;
end;
theorem
J |= p & J |= (p => q) implies J |= q
proof
assume that
A1: J |= p and A2: J |= p => q;
now let v;
J,v |= p & J,v |= p => q by A1,A2,Def13;
hence J,v |= q by Th36;
end;
hence J |= q by Def13;
end;
theorem
J |= All(x,p) => p
proof let v;
thus thesis by Th50;
end;
theorem
(J |= p => q) & not x in still_not-bound_in p implies J |= p => All(x,q)
proof
assume that
A1:for v holds J,v |= p => q and
A2: not x in still_not-bound_in p;
let u;
now assume A3: J,u |= p;
now let w; assume
for y st x<>y holds w.y = u.y;
then A4: J,w |= p by A2,A3,Th40;
J,w |= p => q by A1;
hence J,w |= q by A4,Th36;
end;
hence J,u |= All(x,q) by Th41;
end;
hence J,u |= p => All(x,q) by Th36;
end;
theorem
for s being QC-formula st p = s.x & q = s.y & not x in still_not-bound_in s
&
J |= p holds J |= q
proof let s be QC-formula;
assume that
A1: p = s.x & q = s.y and
A2: not x in still_not-bound_in s and
A3: J |= p;
now assume
A4: x <> y;
A5: now let u;
consider w being Element of Valuations_in A such that
A6: (for z being bound_QC-variable st z <> x holds w.z = u.z) &
w.x = u.y from Lambda_Val;
w.x = w.y by A6;
then A7: Valid(p,J).w = Valid(q,J).w by A1,Th42;
J,w |= p by A3,Def13;
then A8: Valid(p,J).w = TRUE by Def12;
not x in still_not-bound_in q by A1,A2,A4,Th43;
hence Valid(q,J).u = TRUE by A6,A7,A8,Th39;
end;
now let v;
Valid(q,J).v = TRUE by A5;
hence J,v |= q by Def12;
end;
hence J |= q by Def13;
end;
hence thesis by A1,A3;
end;