begin
scheme
QCFuncUniq{
F1()
-> QC-alphabet ,
F2()
-> non
empty set ,
F3()
-> Function of
(QC-WFF F1()),
F2(),
F4()
-> Function of
(QC-WFF F1()),
F2(),
F5()
-> Element of
F2(),
F6(
set )
-> Element of
F2(),
F7(
set )
-> Element of
F2(),
F8(
set ,
set )
-> Element of
F2(),
F9(
set ,
set )
-> Element of
F2() } :
provided
scheme
QCDefD{
F1()
-> QC-alphabet ,
F2()
-> non
empty set ,
F3()
-> Element of
F2(),
F4()
-> Element of
QC-WFF F1(),
F5(
Element of
QC-WFF F1())
-> Element of
F2(),
F6(
Element of
F2())
-> Element of
F2(),
F7(
Element of
F2(),
Element of
F2())
-> Element of
F2(),
F8(
Element of
QC-WFF F1(),
Element of
F2())
-> Element of
F2() } :
( ex
d being
Element of
F2() ex
F being
Function of
(QC-WFF F1()),
F2() st
(
d = F . F4() & ( for
p being
Element of
QC-WFF F1()
for
d1,
d2 being
Element of
F2() holds
( (
p = VERUM F1() implies
F . p = F3() ) & (
p is
atomic implies
F . p = F5(
p) ) & (
p is
negative &
d1 = F . (the_argument_of p) implies
F . p = F6(
d1) ) & (
p is
conjunctive &
d1 = F . (the_left_argument_of p) &
d2 = F . (the_right_argument_of p) implies
F . p = F7(
d1,
d2) ) & (
p is
universal &
d1 = F . (the_scope_of p) implies
F . p = F8(
p,
d1) ) ) ) ) & ( for
x1,
x2 being
Element of
F2() st ex
F being
Function of
(QC-WFF F1()),
F2() st
(
x1 = F . F4() & ( for
p being
Element of
QC-WFF F1()
for
d1,
d2 being
Element of
F2() holds
( (
p = VERUM F1() implies
F . p = F3() ) & (
p is
atomic implies
F . p = F5(
p) ) & (
p is
negative &
d1 = F . (the_argument_of p) implies
F . p = F6(
d1) ) & (
p is
conjunctive &
d1 = F . (the_left_argument_of p) &
d2 = F . (the_right_argument_of p) implies
F . p = F7(
d1,
d2) ) & (
p is
universal &
d1 = F . (the_scope_of p) implies
F . p = F8(
p,
d1) ) ) ) ) & ex
F being
Function of
(QC-WFF F1()),
F2() st
(
x2 = F . F4() & ( for
p being
Element of
QC-WFF F1()
for
d1,
d2 being
Element of
F2() holds
( (
p = VERUM F1() implies
F . p = F3() ) & (
p is
atomic implies
F . p = F5(
p) ) & (
p is
negative &
d1 = F . (the_argument_of p) implies
F . p = F6(
d1) ) & (
p is
conjunctive &
d1 = F . (the_left_argument_of p) &
d2 = F . (the_right_argument_of p) implies
F . p = F7(
d1,
d2) ) & (
p is
universal &
d1 = F . (the_scope_of p) implies
F . p = F8(
p,
d1) ) ) ) ) holds
x1 = x2 ) )
scheme
QCDResult9atomic{
F1()
-> QC-alphabet ,
F2()
-> non
empty set ,
F3()
-> Element of
F2(),
F4(
Element of
QC-WFF F1())
-> Element of
F2(),
F5()
-> QC-formula of
F1(),
F6(
Element of
QC-WFF F1())
-> Element of
F2(),
F7(
Element of
F2())
-> Element of
F2(),
F8(
Element of
F2(),
Element of
F2())
-> Element of
F2(),
F9(
Element of
QC-WFF F1(),
Element of
F2())
-> Element of
F2() } :
provided
scheme
QCDResult9negative{
F1()
-> QC-alphabet ,
F2()
-> non
empty set ,
F3()
-> Element of
F2(),
F4()
-> QC-formula of
F1(),
F5(
Element of
QC-WFF F1())
-> Element of
F2(),
F6(
Element of
F2())
-> Element of
F2(),
F7(
Element of
F2(),
Element of
F2())
-> Element of
F2(),
F8(
Element of
QC-WFF F1(),
Element of
F2())
-> Element of
F2(),
F9(
Element of
QC-WFF F1())
-> Element of
F2() } :
provided
scheme
QCDResult9conjunctive{
F1()
-> QC-alphabet ,
F2()
-> non
empty set ,
F3()
-> Element of
F2(),
F4(
Element of
QC-WFF F1())
-> Element of
F2(),
F5(
Element of
F2())
-> Element of
F2(),
F6(
Element of
F2(),
Element of
F2())
-> Element of
F2(),
F7(
Element of
QC-WFF F1(),
Element of
F2())
-> Element of
F2(),
F8(
Element of
QC-WFF F1())
-> Element of
F2(),
F9()
-> QC-formula of
F1() } :
provided
scheme
QCDResult9universal{
F1()
-> QC-alphabet ,
F2()
-> non
empty set ,
F3()
-> Element of
F2(),
F4()
-> QC-formula of
F1(),
F5(
Element of
QC-WFF F1())
-> Element of
F2(),
F6(
Element of
F2())
-> Element of
F2(),
F7(
Element of
F2(),
Element of
F2())
-> Element of
F2(),
F8(
Element of
QC-WFF F1(),
Element of
F2())
-> Element of
F2(),
F9(
Element of
QC-WFF F1())
-> Element of
F2() } :
provided
Lm1:
now for A being QC-alphabet
for p being QC-formula of A
for d being Subset of (bound_QC-variables A) holds
( d = H1(p) iff ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st
( d = F . p & ( for p being Element of QC-WFF A
for d1, d2 being Subset of (bound_QC-variables A) holds
( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = H2(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H4(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H5(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H3(p,d1) ) ) ) ) )
let A be
QC-alphabet ;
for p being QC-formula of A
for d being Subset of (bound_QC-variables A) holds
( d = H1(p) iff ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st
( d = F . p & ( for p being Element of QC-WFF A
for d1, d2 being Subset of (bound_QC-variables A) holds
( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = H2(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H4(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H5(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H3(p,d1) ) ) ) ) )deffunc H1(
Element of
QC-WFF A)
-> Element of
bool (bound_QC-variables A) =
still_not-bound_in $1;
deffunc H2(
Element of
QC-WFF A)
-> Element of
bool (bound_QC-variables A) =
still_not-bound_in (the_arguments_of $1);
deffunc H3(
Element of
QC-WFF A,
Subset of
(bound_QC-variables A))
-> Element of
bool (bound_QC-variables A) = $2
\ {(bound_in $1)};
deffunc H4(
Subset of
(bound_QC-variables A))
-> Subset of
(bound_QC-variables A) = $1;
deffunc H5(
Subset of
(bound_QC-variables A),
Subset of
(bound_QC-variables A))
-> Element of
bool (bound_QC-variables A) = $1
\/ $2;
thus
for
p being
QC-formula of
A for
d being
Subset of
(bound_QC-variables A) holds
(
d = H1(
p) iff ex
F being
Function of
(QC-WFF A),
(bool (bound_QC-variables A)) st
(
d = F . p & ( for
p being
Element of
QC-WFF A for
d1,
d2 being
Subset of
(bound_QC-variables A) holds
( (
p = VERUM A implies
F . p = {} (bound_QC-variables A) ) & (
p is
atomic implies
F . p = H2(
p) ) & (
p is
negative &
d1 = F . (the_argument_of p) implies
F . p = H4(
d1) ) & (
p is
conjunctive &
d1 = F . (the_left_argument_of p) &
d2 = F . (the_right_argument_of p) implies
F . p = H5(
d1,
d2) ) & (
p is
universal &
d1 = F . (the_scope_of p) implies
F . p = H3(
p,
d1) ) ) ) ) )
verum
proof
let p be
QC-formula of
A;
for d being Subset of (bound_QC-variables A) holds
( d = H1(p) iff ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st
( d = F . p & ( for p being Element of QC-WFF A
for d1, d2 being Subset of (bound_QC-variables A) holds
( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = H2(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H4(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H5(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H3(p,d1) ) ) ) ) )let d be
Subset of
(bound_QC-variables A);
( d = H1(p) iff ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st
( d = F . p & ( for p being Element of QC-WFF A
for d1, d2 being Subset of (bound_QC-variables A) holds
( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = H2(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H4(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H5(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H3(p,d1) ) ) ) ) )
thus
(
d = still_not-bound_in p implies ex
F being
Function of
(QC-WFF A),
(bool (bound_QC-variables A)) st
(
d = F . p & ( for
p being
Element of
QC-WFF A for
d1,
d2 being
Subset of
(bound_QC-variables A) holds
( (
p = VERUM A implies
F . p = {} (bound_QC-variables A) ) & (
p is
atomic implies
F . p = still_not-bound_in (the_arguments_of p) ) & (
p is
negative &
d1 = F . (the_argument_of p) implies
F . p = d1 ) & (
p is
conjunctive &
d1 = F . (the_left_argument_of p) &
d2 = F . (the_right_argument_of p) implies
F . p = d1 \/ d2 ) & (
p is
universal &
d1 = F . (the_scope_of p) implies
F . p = d1 \ {(bound_in p)} ) ) ) ) )
( ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st
( d = F . p & ( for p being Element of QC-WFF A
for d1, d2 being Subset of (bound_QC-variables A) holds
( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = H2(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H4(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H5(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H3(p,d1) ) ) ) ) implies d = H1(p) )
given F being
Function of
(QC-WFF A),
(bool (bound_QC-variables A)) such that A2:
d = F . p
and A3:
for
p being
Element of
QC-WFF A for
d1,
d2 being
Subset of
(bound_QC-variables A) holds
( (
p = VERUM A implies
F . p = {} (bound_QC-variables A) ) & (
p is
atomic implies
F . p = still_not-bound_in (the_arguments_of p) ) & (
p is
negative &
d1 = F . (the_argument_of p) implies
F . p = d1 ) & (
p is
conjunctive &
d1 = F . (the_left_argument_of p) &
d2 = F . (the_right_argument_of p) implies
F . p = d1 \/ d2 ) & (
p is
universal &
d1 = F . (the_scope_of p) implies
F . p = d1 \ {(bound_in p)} ) )
;
d = H1(p)
hence
d = H1(
p)
by A2, QC_LANG1:def 30;
verum
end;
end;
definition
let A be
QC-alphabet ;
let V be non
empty Subset of
(QC-variables A);
let p be
Element of
QC-WFF A;
correctness
existence
ex b1 being Subset of V ex F being Function of (QC-WFF A),(bool V) st
( b1 = F . p & ( for p being Element of QC-WFF A
for d1, d2 being Subset of V holds
( ( p = VERUM A implies F . p = {} V ) & ( p is atomic implies F . p = variables_in ((the_arguments_of p),V) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 ) ) ) );
uniqueness
for b1, b2 being Subset of V st ex F being Function of (QC-WFF A),(bool V) st
( b1 = F . p & ( for p being Element of QC-WFF A
for d1, d2 being Subset of V holds
( ( p = VERUM A implies F . p = {} V ) & ( p is atomic implies F . p = variables_in ((the_arguments_of p),V) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 ) ) ) ) & ex F being Function of (QC-WFF A),(bool V) st
( b2 = F . p & ( for p being Element of QC-WFF A
for d1, d2 being Subset of V holds
( ( p = VERUM A implies F . p = {} V ) & ( p is atomic implies F . p = variables_in ((the_arguments_of p),V) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 ) ) ) ) holds
b1 = b2;
end;
Lm2:
now for A being QC-alphabet
for V being non empty Subset of (QC-variables A) holds
( H1( VERUM A) = {} & ( for p being Element of QC-WFF A st p is atomic holds
Vars (p,V) = variables_in ((the_arguments_of p),V) ) & ( for p being Element of QC-WFF A st p is negative holds
Vars (p,V) = Vars ((the_argument_of p),V) ) & ( for p being Element of QC-WFF A st p is conjunctive holds
Vars (p,V) = (Vars ((the_left_argument_of p),V)) \/ (Vars ((the_right_argument_of p),V)) ) & ( for p being Element of QC-WFF A st p is universal holds
Vars (p,V) = Vars ((the_scope_of p),V) ) )
let A be
QC-alphabet ;
for V being non empty Subset of (QC-variables A) holds
( H1( VERUM A) = {} & ( for p being Element of QC-WFF A st p is atomic holds
Vars (p,V) = variables_in ((the_arguments_of p),V) ) & ( for p being Element of QC-WFF A st p is negative holds
Vars (p,V) = Vars ((the_argument_of p),V) ) & ( for p being Element of QC-WFF A st p is conjunctive holds
Vars (p,V) = (Vars ((the_left_argument_of p),V)) \/ (Vars ((the_right_argument_of p),V)) ) & ( for p being Element of QC-WFF A st p is universal holds
Vars (p,V) = Vars ((the_scope_of p),V) ) )let V be non
empty Subset of
(QC-variables A);
( H1( VERUM A) = {} & ( for p being Element of QC-WFF A st p is atomic holds
Vars (p,V) = variables_in ((the_arguments_of p),V) ) & ( for p being Element of QC-WFF A st p is negative holds
Vars (p,V) = Vars ((the_argument_of p),V) ) & ( for p being Element of QC-WFF A st p is conjunctive holds
Vars (p,V) = (Vars ((the_left_argument_of p),V)) \/ (Vars ((the_right_argument_of p),V)) ) & ( for p being Element of QC-WFF A st p is universal holds
Vars (p,V) = Vars ((the_scope_of p),V) ) )deffunc H1(
Element of
QC-WFF A)
-> Subset of
V =
Vars ($1,
V);
deffunc H2(
Element of
QC-WFF A)
-> Subset of
V =
variables_in (
(the_arguments_of $1),
V);
deffunc H3(
Subset of
V)
-> Subset of
V = $1;
deffunc H4(
Subset of
V,
Subset of
V)
-> Element of
bool V = $1
\/ $2;
deffunc H5(
Element of
QC-WFF A,
Subset of
V)
-> Subset of
V = $2;
A1:
for
p being
Element of
QC-WFF A for
X being
Subset of
V holds
(
X = H1(
p) iff ex
F being
Function of
(QC-WFF A),
(bool V) st
(
X = F . p & ( for
p being
Element of
QC-WFF A for
d1,
d2 being
Subset of
V holds
( (
p = VERUM A implies
F . p = {} V ) & (
p is
atomic implies
F . p = H2(
p) ) & (
p is
negative &
d1 = F . (the_argument_of p) implies
F . p = H3(
d1) ) & (
p is
conjunctive &
d1 = F . (the_left_argument_of p) &
d2 = F . (the_right_argument_of p) implies
F . p = H4(
d1,
d2) ) & (
p is
universal &
d1 = F . (the_scope_of p) implies
F . p = H5(
p,
d1) ) ) ) ) )
by Def4;
thus H1(
VERUM A) =
{} V
from QC_LANG3:sch 3(A1)
.=
{}
;
( ( for p being Element of QC-WFF A st p is atomic holds
Vars (p,V) = variables_in ((the_arguments_of p),V) ) & ( for p being Element of QC-WFF A st p is negative holds
Vars (p,V) = Vars ((the_argument_of p),V) ) & ( for p being Element of QC-WFF A st p is conjunctive holds
Vars (p,V) = (Vars ((the_left_argument_of p),V)) \/ (Vars ((the_right_argument_of p),V)) ) & ( for p being Element of QC-WFF A st p is universal holds
Vars (p,V) = Vars ((the_scope_of p),V) ) )thus
for
p being
Element of
QC-WFF A st
p is
atomic holds
Vars (
p,
V)
= variables_in (
(the_arguments_of p),
V)
( ( for p being Element of QC-WFF A st p is negative holds
Vars (p,V) = Vars ((the_argument_of p),V) ) & ( for p being Element of QC-WFF A st p is conjunctive holds
Vars (p,V) = (Vars ((the_left_argument_of p),V)) \/ (Vars ((the_right_argument_of p),V)) ) & ( for p being Element of QC-WFF A st p is universal holds
Vars (p,V) = Vars ((the_scope_of p),V) ) )
thus
for
p being
Element of
QC-WFF A st
p is
negative holds
Vars (
p,
V)
= Vars (
(the_argument_of p),
V)
( ( for p being Element of QC-WFF A st p is conjunctive holds
Vars (p,V) = (Vars ((the_left_argument_of p),V)) \/ (Vars ((the_right_argument_of p),V)) ) & ( for p being Element of QC-WFF A st p is universal holds
Vars (p,V) = Vars ((the_scope_of p),V) ) )
thus
for
p being
Element of
QC-WFF A st
p is
conjunctive holds
Vars (
p,
V)
= (Vars ((the_left_argument_of p),V)) \/ (Vars ((the_right_argument_of p),V))
for p being Element of QC-WFF A st p is universal holds
Vars (p,V) = Vars ((the_scope_of p),V)
proof
let p be
Element of
QC-WFF A;
( p is conjunctive implies Vars (p,V) = (Vars ((the_left_argument_of p),V)) \/ (Vars ((the_right_argument_of p),V)) )
assume A4:
p is
conjunctive
;
Vars (p,V) = (Vars ((the_left_argument_of p),V)) \/ (Vars ((the_right_argument_of p),V))
for
d1,
d2 being
Subset of
V st
d1 = H1(
the_left_argument_of p) &
d2 = H1(
the_right_argument_of p) holds
H1(
p)
= H4(
d1,
d2)
from QC_LANG3:sch 6(A1, A4);
hence
Vars (
p,
V)
= (Vars ((the_left_argument_of p),V)) \/ (Vars ((the_right_argument_of p),V))
;
verum
end;
thus
for
p being
Element of
QC-WFF A st
p is
universal holds
Vars (
p,
V)
= Vars (
(the_scope_of p),
V)
verum
end;