let Al be QC-alphabet ; for p being Element of CQC-WFF Al
for A being non empty set
for J being interpretation of Al,A holds
( Valid ((VERUM Al),J) = (Valuations_in (Al,A)) --> TRUE & ( for k being Nat
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds Valid ((P ! ll),J) = ll 'in' (J . P) ) & ( for p being Element of CQC-WFF Al holds Valid (('not' p),J) = 'not' (Valid (p,J)) ) & ( for q being Element of CQC-WFF Al holds Valid ((p '&' q),J) = (Valid (p,J)) '&' (Valid (q,J)) ) & ( for x being bound_QC-variable of Al holds Valid ((All (x,p)),J) = FOR_ALL (x,(Valid (p,J))) ) )
let p be Element of CQC-WFF Al; for A being non empty set
for J being interpretation of Al,A holds
( Valid ((VERUM Al),J) = (Valuations_in (Al,A)) --> TRUE & ( for k being Nat
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds Valid ((P ! ll),J) = ll 'in' (J . P) ) & ( for p being Element of CQC-WFF Al holds Valid (('not' p),J) = 'not' (Valid (p,J)) ) & ( for q being Element of CQC-WFF Al holds Valid ((p '&' q),J) = (Valid (p,J)) '&' (Valid (q,J)) ) & ( for x being bound_QC-variable of Al holds Valid ((All (x,p)),J) = FOR_ALL (x,(Valid (p,J))) ) )
let A be non empty set ; for J being interpretation of Al,A holds
( Valid ((VERUM Al),J) = (Valuations_in (Al,A)) --> TRUE & ( for k being Nat
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds Valid ((P ! ll),J) = ll 'in' (J . P) ) & ( for p being Element of CQC-WFF Al holds Valid (('not' p),J) = 'not' (Valid (p,J)) ) & ( for q being Element of CQC-WFF Al holds Valid ((p '&' q),J) = (Valid (p,J)) '&' (Valid (q,J)) ) & ( for x being bound_QC-variable of Al holds Valid ((All (x,p)),J) = FOR_ALL (x,(Valid (p,J))) ) )
let J be interpretation of Al,A; ( Valid ((VERUM Al),J) = (Valuations_in (Al,A)) --> TRUE & ( for k being Nat
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds Valid ((P ! ll),J) = ll 'in' (J . P) ) & ( for p being Element of CQC-WFF Al holds Valid (('not' p),J) = 'not' (Valid (p,J)) ) & ( for q being Element of CQC-WFF Al holds Valid ((p '&' q),J) = (Valid (p,J)) '&' (Valid (q,J)) ) & ( for x being bound_QC-variable of Al holds Valid ((All (x,p)),J) = FOR_ALL (x,(Valid (p,J))) ) )
set D = Funcs ((Valuations_in (Al,A)),BOOLEAN);
set V = In (((Valuations_in (Al,A)) --> TRUE),(Funcs ((Valuations_in (Al,A)),BOOLEAN)));
deffunc H1( Nat, QC-pred_symbol of $1,Al, CQC-variable_list of $1,Al) -> Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) = $3 'in' (J . $2);
deffunc H2( Element of Funcs ((Valuations_in (Al,A)),BOOLEAN)) -> Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) = In (('not' $1),(Funcs ((Valuations_in (Al,A)),BOOLEAN)));
deffunc H3( Element of Funcs ((Valuations_in (Al,A)),BOOLEAN), Element of Funcs ((Valuations_in (Al,A)),BOOLEAN)) -> Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) = In (($1 '&' $2),(Funcs ((Valuations_in (Al,A)),BOOLEAN)));
deffunc H4( bound_QC-variable of Al, Element of Funcs ((Valuations_in (Al,A)),BOOLEAN)) -> Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) = In ((FOR_ALL ($1,$2)),(Funcs ((Valuations_in (Al,A)),BOOLEAN)));
deffunc H5( Element of CQC-WFF Al) -> Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) = Valid ($1,J);
A1:
for p being Element of CQC-WFF Al
for d being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) holds
( d = H5(p) iff ex F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) st
( d = F . p & F . (VERUM Al) = In (((Valuations_in (Al,A)) --> TRUE),(Funcs ((Valuations_in (Al,A)),BOOLEAN))) & ( for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Nat
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = H2(F . p) & F . (p '&' q) = H3(F . p,F . q) & F . (All (x,p)) = H4(x,F . p) ) ) ) )
proof
let p be
Element of
CQC-WFF Al;
for d being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) holds
( d = H5(p) iff ex F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) st
( d = F . p & F . (VERUM Al) = In (((Valuations_in (Al,A)) --> TRUE),(Funcs ((Valuations_in (Al,A)),BOOLEAN))) & ( for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Nat
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = H2(F . p) & F . (p '&' q) = H3(F . p,F . q) & F . (All (x,p)) = H4(x,F . p) ) ) ) )let d be
Element of
Funcs (
(Valuations_in (Al,A)),
BOOLEAN);
( d = H5(p) iff ex F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) st
( d = F . p & F . (VERUM Al) = In (((Valuations_in (Al,A)) --> TRUE),(Funcs ((Valuations_in (Al,A)),BOOLEAN))) & ( for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Nat
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = H2(F . p) & F . (p '&' q) = H3(F . p,F . q) & F . (All (x,p)) = H4(x,F . p) ) ) ) )
thus
(
d = H5(
p) implies ex
F being
Function of
(CQC-WFF Al),
(Funcs ((Valuations_in (Al,A)),BOOLEAN)) st
(
d = F . p &
F . (VERUM Al) = In (
((Valuations_in (Al,A)) --> TRUE),
(Funcs ((Valuations_in (Al,A)),BOOLEAN))) & ( for
p,
q being
Element of
CQC-WFF Al for
x being
bound_QC-variable of
Al for
k being
Nat for
ll being
CQC-variable_list of
k,
Al for
P being
QC-pred_symbol of
k,
Al holds
(
F . (P ! ll) = H1(
k,
P,
ll) &
F . ('not' p) = H2(
F . p) &
F . (p '&' q) = H3(
F . p,
F . q) &
F . (All (x,p)) = H4(
x,
F . p) ) ) ) )
( ex F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) st
( d = F . p & F . (VERUM Al) = In (((Valuations_in (Al,A)) --> TRUE),(Funcs ((Valuations_in (Al,A)),BOOLEAN))) & ( for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Nat
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = H2(F . p) & F . (p '&' q) = H3(F . p,F . q) & F . (All (x,p)) = H4(x,F . p) ) ) ) implies d = H5(p) )proof
assume
d = H5(
p)
;
ex F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) st
( d = F . p & F . (VERUM Al) = In (((Valuations_in (Al,A)) --> TRUE),(Funcs ((Valuations_in (Al,A)),BOOLEAN))) & ( for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Nat
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = H2(F . p) & F . (p '&' q) = H3(F . p,F . q) & F . (All (x,p)) = H4(x,F . p) ) ) )
then consider F being
Function of
(CQC-WFF Al),
(Funcs ((Valuations_in (Al,A)),BOOLEAN)) such that A2:
d = F . p
and A3:
F . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE
and A4:
for
p,
q being
Element of
CQC-WFF Al for
x being
bound_QC-variable of
Al for
k being
Nat for
ll being
CQC-variable_list of
k,
Al for
P being
QC-pred_symbol of
k,
Al 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)) )
by Def6;
take
F
;
( d = F . p & F . (VERUM Al) = In (((Valuations_in (Al,A)) --> TRUE),(Funcs ((Valuations_in (Al,A)),BOOLEAN))) & ( for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Nat
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = H2(F . p) & F . (p '&' q) = H3(F . p,F . q) & F . (All (x,p)) = H4(x,F . p) ) ) )
thus
d = F . p
by A2;
( F . (VERUM Al) = In (((Valuations_in (Al,A)) --> TRUE),(Funcs ((Valuations_in (Al,A)),BOOLEAN))) & ( for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Nat
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = H2(F . p) & F . (p '&' q) = H3(F . p,F . q) & F . (All (x,p)) = H4(x,F . p) ) ) )
thus
F . (VERUM Al) = In (
((Valuations_in (Al,A)) --> TRUE),
(Funcs ((Valuations_in (Al,A)),BOOLEAN)))
by A3, SUBSET_1:def 8;
for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Nat
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = H2(F . p) & F . (p '&' q) = H3(F . p,F . q) & F . (All (x,p)) = H4(x,F . p) )
let p,
q be
Element of
CQC-WFF Al;
for x being bound_QC-variable of Al
for k being Nat
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = H2(F . p) & F . (p '&' q) = H3(F . p,F . q) & F . (All (x,p)) = H4(x,F . p) )let x be
bound_QC-variable of
Al;
for k being Nat
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = H2(F . p) & F . (p '&' q) = H3(F . p,F . q) & F . (All (x,p)) = H4(x,F . p) )let k be
Nat;
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = H2(F . p) & F . (p '&' q) = H3(F . p,F . q) & F . (All (x,p)) = H4(x,F . p) )let ll be
CQC-variable_list of
k,
Al;
for P being QC-pred_symbol of k,Al holds
( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = H2(F . p) & F . (p '&' q) = H3(F . p,F . q) & F . (All (x,p)) = H4(x,F . p) )let P be
QC-pred_symbol of
k,
Al;
( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = H2(F . p) & F . (p '&' q) = H3(F . p,F . q) & F . (All (x,p)) = H4(x,F . p) )
thus
F . (P ! ll) = H1(
k,
P,
ll)
by A4;
( F . ('not' p) = H2(F . p) & F . (p '&' q) = H3(F . p,F . q) & F . (All (x,p)) = H4(x,F . p) )
A5:
'not' (F . p) in Funcs (
(Valuations_in (Al,A)),
BOOLEAN)
by FUNCT_2:8;
thus F . ('not' p) =
'not' (F . p)
by A4
.=
H2(
F . p)
by A5, SUBSET_1:def 8
;
( F . (p '&' q) = H3(F . p,F . q) & F . (All (x,p)) = H4(x,F . p) )
A6:
(F . p) '&' (F . q) in Funcs (
(Valuations_in (Al,A)),
BOOLEAN)
by FUNCT_2:8;
thus F . (p '&' q) =
(F . p) '&' (F . q)
by A4
.=
H3(
F . p,
F . q)
by A6, SUBSET_1:def 8
;
F . (All (x,p)) = H4(x,F . p)
thus F . (All (x,p)) =
FOR_ALL (
x,
(F . p))
by A4
.=
H4(
x,
F . p)
by SUBSET_1:def 8
;
verum
end;
given F being
Function of
(CQC-WFF Al),
(Funcs ((Valuations_in (Al,A)),BOOLEAN)) such that A7:
d = F . p
and A8:
F . (VERUM Al) = In (
((Valuations_in (Al,A)) --> TRUE),
(Funcs ((Valuations_in (Al,A)),BOOLEAN)))
and A9:
for
p,
q being
Element of
CQC-WFF Al for
x being
bound_QC-variable of
Al for
k being
Nat for
ll being
CQC-variable_list of
k,
Al for
P being
QC-pred_symbol of
k,
Al holds
(
F . (P ! ll) = H1(
k,
P,
ll) &
F . ('not' p) = H2(
F . p) &
F . (p '&' q) = H3(
F . p,
F . q) &
F . (All (x,p)) = H4(
x,
F . p) )
;
d = H5(p)
(Valuations_in (Al,A)) --> TRUE in Funcs (
(Valuations_in (Al,A)),
BOOLEAN)
by FUNCT_2:8;
then A10:
F . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE
by A8, SUBSET_1:def 8;
for
p,
q being
Element of
CQC-WFF Al for
x being
bound_QC-variable of
Al for
k being
Nat for
ll being
CQC-variable_list of
k,
Al for
P being
QC-pred_symbol of
k,
Al holds
(
F . (P ! ll) = H1(
k,
P,
ll) &
F . ('not' p) = 'not' (F . p) &
F . (p '&' q) = (F . p) '&' (F . q) &
F . (All (x,p)) = FOR_ALL (
x,
(F . p)) )
proof
let p,
q be
Element of
CQC-WFF Al;
for x being bound_QC-variable of Al
for k being Nat
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) )let x be
bound_QC-variable of
Al;
for k being Nat
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) )let k be
Nat;
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) )let ll be
CQC-variable_list of
k,
Al;
for P being QC-pred_symbol of k,Al holds
( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) )let P be
QC-pred_symbol of
k,
Al;
( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) )
thus
F . (P ! ll) = H1(
k,
P,
ll)
by A9;
( F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) )
A11:
'not' (F . p) in Funcs (
(Valuations_in (Al,A)),
BOOLEAN)
by FUNCT_2:8;
thus F . ('not' p) =
H2(
F . p)
by A9
.=
'not' (F . p)
by A11, SUBSET_1:def 8
;
( F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) )
A12:
(F . p) '&' (F . q) in Funcs (
(Valuations_in (Al,A)),
BOOLEAN)
by FUNCT_2:8;
thus F . (p '&' q) =
H3(
F . p,
F . q)
by A9
.=
(F . p) '&' (F . q)
by A12, SUBSET_1:def 8
;
F . (All (x,p)) = FOR_ALL (x,(F . p))
thus F . (All (x,p)) =
H4(
x,
F . p)
by A9
.=
FOR_ALL (
x,
(F . p))
by SUBSET_1:def 8
;
verum
end;
hence
d = H5(
p)
by A7, A10, Def6;
verum
end;
A13:
(Valuations_in (Al,A)) --> TRUE in Funcs ((Valuations_in (Al,A)),BOOLEAN)
by FUNCT_2:8;
H5( VERUM Al) = In (((Valuations_in (Al,A)) --> TRUE),(Funcs ((Valuations_in (Al,A)),BOOLEAN)))
from CQC_LANG:sch 5(A1);
hence
H5( VERUM Al) = (Valuations_in (Al,A)) --> TRUE
by A13, SUBSET_1:def 8; ( ( for k being Nat
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds Valid ((P ! ll),J) = ll 'in' (J . P) ) & ( for p being Element of CQC-WFF Al holds Valid (('not' p),J) = 'not' (Valid (p,J)) ) & ( for q being Element of CQC-WFF Al holds Valid ((p '&' q),J) = (Valid (p,J)) '&' (Valid (q,J)) ) & ( for x being bound_QC-variable of Al holds Valid ((All (x,p)),J) = FOR_ALL (x,(Valid (p,J))) ) )
hereby ( ( for p being Element of CQC-WFF Al holds Valid (('not' p),J) = 'not' (Valid (p,J)) ) & ( for q being Element of CQC-WFF Al holds Valid ((p '&' q),J) = (Valid (p,J)) '&' (Valid (q,J)) ) & ( for x being bound_QC-variable of Al holds Valid ((All (x,p)),J) = FOR_ALL (x,(Valid (p,J))) ) )
let k be
Nat;
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds H5(P ! ll) = H1(k,P,ll)let ll be
CQC-variable_list of
k,
Al;
for P being QC-pred_symbol of k,Al holds H5(P ! ll) = H1(k,P,ll)let P be
QC-pred_symbol of
k,
Al;
H5(P ! ll) = H1(k,P,ll)thus
H5(
P ! ll)
= H1(
k,
P,
ll)
from CQC_LANG:sch 6(A1); verum
end;
let x be bound_QC-variable of Al; Valid ((All (x,p)),J) = FOR_ALL (x,(Valid (p,J)))
H5( All (x,p)) = H4(x,H5(p))
from CQC_LANG:sch 9(A1);
hence
H5( All (x,p)) = FOR_ALL (x,H5(p))
by SUBSET_1:def 8; verum