:: VALUAT_1 semantic presentation
begin
definition
let Al be QC-alphabet ;
let A be set ;
func Valuations_in (Al,A) -> set equals :: VALUAT_1:def 1
Funcs ((bound_QC-variables Al),A);
coherence
Funcs ((bound_QC-variables Al),A) is set ;
end;
:: deftheorem defines Valuations_in VALUAT_1:def_1_:_
for Al being QC-alphabet
for A being set holds Valuations_in (Al,A) = Funcs ((bound_QC-variables Al),A);
registration
let Al be QC-alphabet ;
let A be non empty set ;
cluster Valuations_in (Al,A) -> functional non empty ;
coherence
( not Valuations_in (Al,A) is empty & Valuations_in (Al,A) is functional ) ;
end;
theorem Th1: :: VALUAT_1:1
for Al being QC-alphabet
for A being non empty set
for x being set st x is Element of Valuations_in (Al,A) holds
x is Function of (bound_QC-variables Al),A
proof
let Al be QC-alphabet ; ::_thesis: for A being non empty set
for x being set st x is Element of Valuations_in (Al,A) holds
x is Function of (bound_QC-variables Al),A
let A be non empty set ; ::_thesis: for x being set st x is Element of Valuations_in (Al,A) holds
x is Function of (bound_QC-variables Al),A
let x be set ; ::_thesis: ( x is Element of Valuations_in (Al,A) implies x is Function of (bound_QC-variables Al),A )
assume x is Element of Valuations_in (Al,A) ; ::_thesis: x is Function of (bound_QC-variables Al),A
then ex f being Function st
( x = f & dom f = bound_QC-variables Al & rng f c= A ) by FUNCT_2:def_2;
hence x is Function of (bound_QC-variables Al),A by FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum
end;
definition
let Al be QC-alphabet ;
let A be non empty set ;
:: original: Valuations_in
redefine func Valuations_in (Al,A) -> FUNCTION_DOMAIN of bound_QC-variables Al,A;
coherence
Valuations_in (Al,A) is FUNCTION_DOMAIN of bound_QC-variables Al,A
proof
for x being Element of Valuations_in (Al,A) holds x is Function of (bound_QC-variables Al),A by Th1;
hence Valuations_in (Al,A) is FUNCTION_DOMAIN of bound_QC-variables Al,A by FUNCT_2:def_12; ::_thesis: verum
end;
end;
definition
let Al be QC-alphabet ;
let A be non empty set ;
let x be bound_QC-variable of Al;
let p be Element of Funcs ((Valuations_in (Al,A)),BOOLEAN);
func FOR_ALL (x,p) -> Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) means :Def2: :: VALUAT_1:def 2
for v being Element of Valuations_in (Al,A) holds it . v = ALL { (p . v9) where v9 is Element of Valuations_in (Al,A) : for y being bound_QC-variable of Al st x <> y holds
v9 . y = v . y } ;
existence
ex b1 being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) st
for v being Element of Valuations_in (Al,A) holds b1 . v = ALL { (p . v9) where v9 is Element of Valuations_in (Al,A) : for y being bound_QC-variable of Al st x <> y holds
v9 . y = v . y }
proof
deffunc H1( Function) -> Element of BOOLEAN = ALL { (p . v9) where v9 is Element of Valuations_in (Al,A) : for y being bound_QC-variable of Al st x <> y holds
v9 . y = $1 . y } ;
consider f being Function of (Valuations_in (Al,A)),BOOLEAN such that
A1: for v being Element of Valuations_in (Al,A) holds f . v = H1(v) from FUNCT_2:sch_4();
( dom f = Valuations_in (Al,A) & rng f c= BOOLEAN ) by FUNCT_2:def_1, RELAT_1:def_19;
then reconsider f = f as Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) by FUNCT_2:def_2;
take f ; ::_thesis: for v being Element of Valuations_in (Al,A) holds f . v = ALL { (p . v9) where v9 is Element of Valuations_in (Al,A) : for y being bound_QC-variable of Al st x <> y holds
v9 . y = v . y }
thus for v being Element of Valuations_in (Al,A) holds f . v = ALL { (p . v9) where v9 is Element of Valuations_in (Al,A) : for y being bound_QC-variable of Al st x <> y holds
v9 . y = v . y } by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) st ( for v being Element of Valuations_in (Al,A) holds b1 . v = ALL { (p . v9) where v9 is Element of Valuations_in (Al,A) : for y being bound_QC-variable of Al st x <> y holds
v9 . y = v . y } ) & ( for v being Element of Valuations_in (Al,A) holds b2 . v = ALL { (p . v9) where v9 is Element of Valuations_in (Al,A) : for y being bound_QC-variable of Al st x <> y holds
v9 . y = v . y } ) holds
b1 = b2
proof
let f1, f2 be Element of Funcs ((Valuations_in (Al,A)),BOOLEAN); ::_thesis: ( ( for v being Element of Valuations_in (Al,A) holds f1 . v = ALL { (p . v9) where v9 is Element of Valuations_in (Al,A) : for y being bound_QC-variable of Al st x <> y holds
v9 . y = v . y } ) & ( for v being Element of Valuations_in (Al,A) holds f2 . v = ALL { (p . v9) where v9 is Element of Valuations_in (Al,A) : for y being bound_QC-variable of Al st x <> y holds
v9 . y = v . y } ) implies f1 = f2 )
assume that
A2: for v being Element of Valuations_in (Al,A) holds f1 . v = ALL { (p . v9) where v9 is Element of Valuations_in (Al,A) : for y being bound_QC-variable of Al st x <> y holds
v9 . y = v . y } and
A3: for v being Element of Valuations_in (Al,A) holds f2 . v = ALL { (p . v9) where v9 is Element of Valuations_in (Al,A) : for y being bound_QC-variable of Al st x <> y holds
v9 . y = v . y } ; ::_thesis: f1 = f2
for v being Element of Valuations_in (Al,A) holds f1 . v = f2 . v
proof
let v be Element of Valuations_in (Al,A); ::_thesis: f1 . v = f2 . v
f1 . v = ALL { (p . v9) where v9 is Element of Valuations_in (Al,A) : for y being bound_QC-variable of Al st x <> y holds
v9 . y = v . y } by A2;
hence f1 . v = f2 . v by A3; ::_thesis: verum
end;
hence f1 = f2 by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines FOR_ALL VALUAT_1:def_2_:_
for Al being QC-alphabet
for A being non empty set
for x being bound_QC-variable of Al
for p, b5 being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) holds
( b5 = FOR_ALL (x,p) iff for v being Element of Valuations_in (Al,A) holds b5 . v = ALL { (p . v9) where v9 is Element of Valuations_in (Al,A) : for y being bound_QC-variable of Al st x <> y holds
v9 . y = v . y } );
theorem Th2: :: VALUAT_1:2
for Al being QC-alphabet
for A being non empty set
for x being bound_QC-variable of Al
for v being Element of Valuations_in (Al,A)
for p being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) holds
( (FOR_ALL (x,p)) . v = FALSE iff ex v1 being Element of Valuations_in (Al,A) st
( p . v1 = FALSE & ( for y being bound_QC-variable of Al st x <> y holds
v1 . y = v . y ) ) )
proof
let Al be QC-alphabet ; ::_thesis: for A being non empty set
for x being bound_QC-variable of Al
for v being Element of Valuations_in (Al,A)
for p being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) holds
( (FOR_ALL (x,p)) . v = FALSE iff ex v1 being Element of Valuations_in (Al,A) st
( p . v1 = FALSE & ( for y being bound_QC-variable of Al st x <> y holds
v1 . y = v . y ) ) )
let A be non empty set ; ::_thesis: for x being bound_QC-variable of Al
for v being Element of Valuations_in (Al,A)
for p being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) holds
( (FOR_ALL (x,p)) . v = FALSE iff ex v1 being Element of Valuations_in (Al,A) st
( p . v1 = FALSE & ( for y being bound_QC-variable of Al st x <> y holds
v1 . y = v . y ) ) )
let x be bound_QC-variable of Al; ::_thesis: for v being Element of Valuations_in (Al,A)
for p being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) holds
( (FOR_ALL (x,p)) . v = FALSE iff ex v1 being Element of Valuations_in (Al,A) st
( p . v1 = FALSE & ( for y being bound_QC-variable of Al st x <> y holds
v1 . y = v . y ) ) )
let v be Element of Valuations_in (Al,A); ::_thesis: for p being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) holds
( (FOR_ALL (x,p)) . v = FALSE iff ex v1 being Element of Valuations_in (Al,A) st
( p . v1 = FALSE & ( for y being bound_QC-variable of Al st x <> y holds
v1 . y = v . y ) ) )
let p be Element of Funcs ((Valuations_in (Al,A)),BOOLEAN); ::_thesis: ( (FOR_ALL (x,p)) . v = FALSE iff ex v1 being Element of Valuations_in (Al,A) st
( p . v1 = FALSE & ( for y being bound_QC-variable of Al st x <> y holds
v1 . y = v . y ) ) )
A1: now__::_thesis:_(_ex_v1_being_Element_of_Valuations_in_(Al,A)_st_
(_p_._v1_=_FALSE_&_(_for_y_being_bound_QC-variable_of_Al_st_x_<>_y_holds_
v1_._y_=_v_._y_)_)_implies_(FOR_ALL_(x,p))_._v_=_FALSE_)
assume ex v1 being Element of Valuations_in (Al,A) st
( p . v1 = FALSE & ( for y being bound_QC-variable of Al st x <> y holds
v1 . y = v . y ) ) ; ::_thesis: (FOR_ALL (x,p)) . v = FALSE
then FALSE in { (p . v99) where v99 is Element of Valuations_in (Al,A) : for y being bound_QC-variable of Al st x <> y holds
v99 . y = v . y } ;
then ALL { (p . v99) where v99 is Element of Valuations_in (Al,A) : for y being bound_QC-variable of Al st x <> y holds
v99 . y = v . y } = FALSE by MARGREL1:17;
hence (FOR_ALL (x,p)) . v = FALSE by Def2; ::_thesis: verum
end;
now__::_thesis:_(_(FOR_ALL_(x,p))_._v_=_FALSE_implies_ex_v1_being_Element_of_Valuations_in_(Al,A)_st_
(_p_._v1_=_FALSE_&_(_for_y_being_bound_QC-variable_of_Al_st_x_<>_y_holds_
v1_._y_=_v_._y_)_)_)
assume (FOR_ALL (x,p)) . v = FALSE ; ::_thesis: ex v1 being Element of Valuations_in (Al,A) st
( p . v1 = FALSE & ( for y being bound_QC-variable of Al st x <> y holds
v1 . y = v . y ) )
then ALL { (p . v99) where v99 is Element of Valuations_in (Al,A) : for y being bound_QC-variable of Al st x <> y holds
v99 . y = v . y } = FALSE by Def2;
then FALSE in { (p . v99) where v99 is Element of Valuations_in (Al,A) : for y being bound_QC-variable of Al st x <> y holds
v99 . y = v . y } by MARGREL1:17;
hence ex v1 being Element of Valuations_in (Al,A) st
( p . v1 = FALSE & ( for y being bound_QC-variable of Al st x <> y holds
v1 . y = v . y ) ) ; ::_thesis: verum
end;
hence ( (FOR_ALL (x,p)) . v = FALSE iff ex v1 being Element of Valuations_in (Al,A) st
( p . v1 = FALSE & ( for y being bound_QC-variable of Al st x <> y holds
v1 . y = v . y ) ) ) by A1; ::_thesis: verum
end;
theorem Th3: :: VALUAT_1:3
for Al being QC-alphabet
for A being non empty set
for x being bound_QC-variable of Al
for v being Element of Valuations_in (Al,A)
for p being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) holds
( (FOR_ALL (x,p)) . v = TRUE iff for v1 being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
v1 . y = v . y ) holds
p . v1 = TRUE )
proof
let Al be QC-alphabet ; ::_thesis: for A being non empty set
for x being bound_QC-variable of Al
for v being Element of Valuations_in (Al,A)
for p being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) holds
( (FOR_ALL (x,p)) . v = TRUE iff for v1 being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
v1 . y = v . y ) holds
p . v1 = TRUE )
let A be non empty set ; ::_thesis: for x being bound_QC-variable of Al
for v being Element of Valuations_in (Al,A)
for p being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) holds
( (FOR_ALL (x,p)) . v = TRUE iff for v1 being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
v1 . y = v . y ) holds
p . v1 = TRUE )
let x be bound_QC-variable of Al; ::_thesis: for v being Element of Valuations_in (Al,A)
for p being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) holds
( (FOR_ALL (x,p)) . v = TRUE iff for v1 being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
v1 . y = v . y ) holds
p . v1 = TRUE )
let v be Element of Valuations_in (Al,A); ::_thesis: for p being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) holds
( (FOR_ALL (x,p)) . v = TRUE iff for v1 being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
v1 . y = v . y ) holds
p . v1 = TRUE )
let p be Element of Funcs ((Valuations_in (Al,A)),BOOLEAN); ::_thesis: ( (FOR_ALL (x,p)) . v = TRUE iff for v1 being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
v1 . y = v . y ) holds
p . v1 = TRUE )
A1: now__::_thesis:_(_(FOR_ALL_(x,p))_._v_=_TRUE_implies_for_v1_being_Element_of_Valuations_in_(Al,A)_st_(_for_y_being_bound_QC-variable_of_Al_st_x_<>_y_holds_
v1_._y_=_v_._y_)_holds_
p_._v1_=_TRUE_)
assume (FOR_ALL (x,p)) . v = TRUE ; ::_thesis: for v1 being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
v1 . y = v . y ) holds
p . v1 = TRUE
then ALL { (p . v99) where v99 is Element of Valuations_in (Al,A) : for y being bound_QC-variable of Al st x <> y holds
v99 . y = v . y } = TRUE by Def2;
then A2: not FALSE in { (p . v99) where v99 is Element of Valuations_in (Al,A) : for y being bound_QC-variable of Al st x <> y holds
v99 . y = v . y } by MARGREL1:17;
thus for v1 being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
v1 . y = v . y ) holds
p . v1 = TRUE ::_thesis: verum
proof
let v1 be Element of Valuations_in (Al,A); ::_thesis: ( ( for y being bound_QC-variable of Al st x <> y holds
v1 . y = v . y ) implies p . v1 = TRUE )
assume for y being bound_QC-variable of Al st x <> y holds
v1 . y = v . y ; ::_thesis: p . v1 = TRUE
then not p . v1 = FALSE by A2;
hence p . v1 = TRUE by XBOOLEAN:def_3; ::_thesis: verum
end;
end;
now__::_thesis:_(_(_for_v1_being_Element_of_Valuations_in_(Al,A)_st_(_for_y_being_bound_QC-variable_of_Al_st_x_<>_y_holds_
v1_._y_=_v_._y_)_holds_
p_._v1_=_TRUE_)_implies_(FOR_ALL_(x,p))_._v_=_TRUE_)
assume for v1 being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
v1 . y = v . y ) holds
p . v1 = TRUE ; ::_thesis: (FOR_ALL (x,p)) . v = TRUE
then for v1 being Element of Valuations_in (Al,A) holds
( not p . v1 = FALSE or ex y being bound_QC-variable of Al st
( x <> y & not v1 . y = v . y ) ) ;
then not FALSE in { (p . v99) where v99 is Element of Valuations_in (Al,A) : for y being bound_QC-variable of Al st x <> y holds
v99 . y = v . y } ;
then ALL { (p . v99) where v99 is Element of Valuations_in (Al,A) : for y being bound_QC-variable of Al st x <> y holds
v99 . y = v . y } = TRUE by MARGREL1:17;
hence (FOR_ALL (x,p)) . v = TRUE by Def2; ::_thesis: verum
end;
hence ( (FOR_ALL (x,p)) . v = TRUE iff for v1 being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
v1 . y = v . y ) holds
p . v1 = TRUE ) by A1; ::_thesis: verum
end;
notation
let Al be QC-alphabet ;
let A be non empty set ;
let k be Element of NAT ;
let ll be CQC-variable_list of k,Al;
let v be Element of Valuations_in (Al,A);
synonym v *' ll for A * Al;
end;
definition
let Al be QC-alphabet ;
let A be non empty set ;
let k be Element of NAT ;
let ll be CQC-variable_list of k,Al;
let v be Element of Valuations_in (Al,A);
:: original: *'
redefine funcv *' ll -> FinSequence of A means :Def3: :: VALUAT_1:def 3
( len it = k & ( for i being natural number st 1 <= i & i <= k holds
it . i = v . (ll . i) ) );
coherence
*' is FinSequence of A
proof
( rng v c= A & rng (v * ll) c= rng v ) by RELAT_1:26, RELAT_1:def_19;
then A1: rng (v * ll) c= A by XBOOLE_1:1;
A2: len ll = k by CARD_1:def_7;
dom v = bound_QC-variables Al by FUNCT_2:def_1;
then rng ll c= dom v by RELAT_1:def_19;
then dom (v * ll) = dom ll by RELAT_1:27
.= Seg k by A2, FINSEQ_1:def_3 ;
then v * ll is FinSequence-like by FINSEQ_1:def_2;
hence *' is FinSequence of A by A1, FINSEQ_1:def_4; ::_thesis: verum
end;
compatibility
for b1 being FinSequence of A holds
( b1 = *' iff ( len b1 = k & ( for i being natural number st 1 <= i & i <= k holds
b1 . i = v . (ll . i) ) ) )
proof
let IT be FinSequence of A; ::_thesis: ( IT = *' iff ( len IT = k & ( for i being natural number st 1 <= i & i <= k holds
IT . i = v . (ll . i) ) ) )
A3: len ll = k by CARD_1:def_7;
dom v = bound_QC-variables Al by FUNCT_2:def_1;
then A4: rng ll c= dom v by RELAT_1:def_19;
thus ( IT = v * ll implies ( len IT = k & ( for i being natural number st 1 <= i & i <= k holds
IT . i = v . (ll . i) ) ) ) ::_thesis: ( len IT = k & ( for i being natural number st 1 <= i & i <= k holds
IT . i = v . (ll . i) ) implies IT = *' )
proof
assume A5: IT = v * ll ; ::_thesis: ( len IT = k & ( for i being natural number st 1 <= i & i <= k holds
IT . i = v . (ll . i) ) )
then A6: dom ll = dom IT by A4, RELAT_1:27;
hence len IT = k by A3, FINSEQ_3:29; ::_thesis: for i being natural number st 1 <= i & i <= k holds
IT . i = v . (ll . i)
let i be natural number ; ::_thesis: ( 1 <= i & i <= k implies IT . i = v . (ll . i) )
assume ( 1 <= i & i <= k ) ; ::_thesis: IT . i = v . (ll . i)
then i in dom IT by A3, A6, FINSEQ_3:25;
hence IT . i = v . (ll . i) by A5, FUNCT_1:12; ::_thesis: verum
end;
assume that
A7: len IT = k and
A8: for i being Nat st 1 <= i & i <= k holds
IT . i = v . (ll . i) ; ::_thesis: IT = *'
A9: for x being set holds
( x in dom IT iff ( x in dom ll & ll . x in dom v ) )
proof
let x be set ; ::_thesis: ( x in dom IT iff ( x in dom ll & ll . x in dom v ) )
thus ( x in dom IT implies ( x in dom ll & ll . x in dom v ) ) ::_thesis: ( x in dom ll & ll . x in dom v implies x in dom IT )
proof
assume x in dom IT ; ::_thesis: ( x in dom ll & ll . x in dom v )
hence x in dom ll by A3, A7, FINSEQ_3:29; ::_thesis: ll . x in dom v
then ll . x in rng ll by FUNCT_1:def_3;
hence ll . x in dom v by A4; ::_thesis: verum
end;
assume that
A10: x in dom ll and
ll . x in dom v ; ::_thesis: x in dom IT
thus x in dom IT by A3, A7, A10, FINSEQ_3:29; ::_thesis: verum
end;
for x being set st x in dom IT holds
IT . x = v . (ll . x)
proof
let x be set ; ::_thesis: ( x in dom IT implies IT . x = v . (ll . x) )
assume A11: x in dom IT ; ::_thesis: IT . x = v . (ll . x)
then reconsider i = x as Element of NAT ;
( 1 <= i & i <= k ) by A7, A11, FINSEQ_3:25;
hence IT . x = v . (ll . x) by A8; ::_thesis: verum
end;
hence IT = *' by A9, FUNCT_1:10; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines *' VALUAT_1:def_3_:_
for Al being QC-alphabet
for A being non empty set
for k being Element of NAT
for ll being CQC-variable_list of k,Al
for v being Element of Valuations_in (Al,A)
for b6 being FinSequence of A holds
( b6 = v *' ll iff ( len b6 = k & ( for i being natural number st 1 <= i & i <= k holds
b6 . i = v . (ll . i) ) ) );
definition
let Al be QC-alphabet ;
let A be non empty set ;
let k be Element of NAT ;
let ll be CQC-variable_list of k,Al;
let r be Element of relations_on A;
funcll 'in' r -> Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) means :Def4: :: VALUAT_1:def 4
for v being Element of Valuations_in (Al,A) holds
( ( v *' ll in r implies it . v = TRUE ) & ( it . v = TRUE implies v *' ll in r ) & ( not v *' ll in r implies it . v = FALSE ) & ( it . v = FALSE implies not v *' ll in r ) );
existence
ex b1 being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) st
for v being Element of Valuations_in (Al,A) holds
( ( v *' ll in r implies b1 . v = TRUE ) & ( b1 . v = TRUE implies v *' ll in r ) & ( not v *' ll in r implies b1 . v = FALSE ) & ( b1 . v = FALSE implies not v *' ll in r ) )
proof
defpred S1[ set ] means ex v being Element of Valuations_in (Al,A) st
( $1 = v & v *' ll in r );
deffunc H1( set ) -> Element of BOOLEAN = TRUE ;
deffunc H2( set ) -> Element of BOOLEAN = FALSE ;
A1: for x being set st x in Valuations_in (Al,A) holds
( ( S1[x] implies H1(x) in BOOLEAN ) & ( not S1[x] implies H2(x) in BOOLEAN ) ) ;
consider f being Function of (Valuations_in (Al,A)),BOOLEAN such that
A2: for x being set st x in Valuations_in (Al,A) holds
( ( S1[x] implies f . x = H1(x) ) & ( not S1[x] implies f . x = H2(x) ) ) from FUNCT_2:sch_5(A1);
( dom f = Valuations_in (Al,A) & rng f c= BOOLEAN ) by FUNCT_2:def_1, RELAT_1:def_19;
then reconsider f = f as Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) by FUNCT_2:def_2;
take f ; ::_thesis: for v being Element of Valuations_in (Al,A) holds
( ( v *' ll in r implies f . v = TRUE ) & ( f . v = TRUE implies v *' ll in r ) & ( not v *' ll in r implies f . v = FALSE ) & ( f . v = FALSE implies not v *' ll in r ) )
let v be Element of Valuations_in (Al,A); ::_thesis: ( ( v *' ll in r implies f . v = TRUE ) & ( f . v = TRUE implies v *' ll in r ) & ( not v *' ll in r implies f . v = FALSE ) & ( f . v = FALSE implies not v *' ll in r ) )
( ( for v9 being Element of Valuations_in (Al,A) holds
( not v = v9 or not v9 *' ll in r ) ) implies f . v = FALSE ) by A2;
hence ( ( v *' ll in r implies f . v = TRUE ) & ( f . v = TRUE implies v *' ll in r ) & ( not v *' ll in r implies f . v = FALSE ) & ( f . v = FALSE implies not v *' ll in r ) ) by A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) st ( for v being Element of Valuations_in (Al,A) holds
( ( v *' ll in r implies b1 . v = TRUE ) & ( b1 . v = TRUE implies v *' ll in r ) & ( not v *' ll in r implies b1 . v = FALSE ) & ( b1 . v = FALSE implies not v *' ll in r ) ) ) & ( for v being Element of Valuations_in (Al,A) holds
( ( v *' ll in r implies b2 . v = TRUE ) & ( b2 . v = TRUE implies v *' ll in r ) & ( not v *' ll in r implies b2 . v = FALSE ) & ( b2 . v = FALSE implies not v *' ll in r ) ) ) holds
b1 = b2
proof
let f1, f2 be Element of Funcs ((Valuations_in (Al,A)),BOOLEAN); ::_thesis: ( ( for v being Element of Valuations_in (Al,A) holds
( ( v *' ll in r implies f1 . v = TRUE ) & ( f1 . v = TRUE implies v *' ll in r ) & ( not v *' ll in r implies f1 . v = FALSE ) & ( f1 . v = FALSE implies not v *' ll in r ) ) ) & ( for v being Element of Valuations_in (Al,A) holds
( ( v *' ll in r implies f2 . v = TRUE ) & ( f2 . v = TRUE implies v *' ll in r ) & ( not v *' ll in r implies f2 . v = FALSE ) & ( f2 . v = FALSE implies not v *' ll in r ) ) ) implies f1 = f2 )
assume that
A3: for v being Element of Valuations_in (Al,A) holds
( ( v *' ll in r implies f1 . v = TRUE ) & ( f1 . v = TRUE implies v *' ll in r ) & ( not v *' ll in r implies f1 . v = FALSE ) & ( f1 . v = FALSE implies not v *' ll in r ) ) and
A4: for v being Element of Valuations_in (Al,A) holds
( ( v *' ll in r implies f2 . v = TRUE ) & ( f2 . v = TRUE implies v *' ll in r ) & ( not v *' ll in r implies f2 . v = FALSE ) & ( f2 . v = FALSE implies not v *' ll in r ) ) ; ::_thesis: f1 = f2
for v being Element of Valuations_in (Al,A) holds f1 . v = f2 . v
proof
let v be Element of Valuations_in (Al,A); ::_thesis: f1 . v = f2 . v
percases ( v *' ll in r or not v *' ll in r ) ;
supposeA5: v *' ll in r ; ::_thesis: f1 . v = f2 . v
then f1 . v = TRUE by A3;
hence f1 . v = f2 . v by A4, A5; ::_thesis: verum
end;
supposeA6: not v *' ll in r ; ::_thesis: f1 . v = f2 . v
then f1 . v = FALSE by A3;
hence f1 . v = f2 . v by A4, A6; ::_thesis: verum
end;
end;
end;
hence f1 = f2 by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines 'in' VALUAT_1:def_4_:_
for Al being QC-alphabet
for A being non empty set
for k being Element of NAT
for ll being CQC-variable_list of k,Al
for r being Element of relations_on A
for b6 being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) holds
( b6 = ll 'in' r iff for v being Element of Valuations_in (Al,A) holds
( ( v *' ll in r implies b6 . v = TRUE ) & ( b6 . v = TRUE implies v *' ll in r ) & ( not v *' ll in r implies b6 . v = FALSE ) & ( b6 . v = FALSE implies not v *' ll in r ) ) );
definition
let Al be QC-alphabet ;
let A be non empty set ;
let F be Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN));
let p be Element of CQC-WFF Al;
:: original: .
redefine funcF . p -> Element of Funcs ((Valuations_in (Al,A)),BOOLEAN);
coherence
F . p is Element of Funcs ((Valuations_in (Al,A)),BOOLEAN)
proof
thus F . p is Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) ; ::_thesis: verum
end;
end;
definition
let Al be QC-alphabet ;
let D be non empty set ;
mode interpretation of Al,D -> Function of (QC-pred_symbols Al),(relations_on D) means :: VALUAT_1:def 5
for P being Element of QC-pred_symbols Al
for r being Element of relations_on D holds
( not it . P = r or r = empty_rel D or the_arity_of P = the_arity_of r );
existence
ex b1 being Function of (QC-pred_symbols Al),(relations_on D) st
for P being Element of QC-pred_symbols Al
for r being Element of relations_on D holds
( not b1 . P = r or r = empty_rel D or the_arity_of P = the_arity_of r )
proof
reconsider F1 = (QC-pred_symbols Al) --> (empty_rel D) as Function of (QC-pred_symbols Al),(relations_on D) ;
take F1 ; ::_thesis: for P being Element of QC-pred_symbols Al
for r being Element of relations_on D holds
( not F1 . P = r or r = empty_rel D or the_arity_of P = the_arity_of r )
let P be Element of QC-pred_symbols Al; ::_thesis: for r being Element of relations_on D holds
( not F1 . P = r or r = empty_rel D or the_arity_of P = the_arity_of r )
thus for r being Element of relations_on D holds
( not F1 . P = r or r = empty_rel D or the_arity_of P = the_arity_of r ) by FUNCOP_1:7; ::_thesis: verum
end;
end;
:: deftheorem defines interpretation VALUAT_1:def_5_:_
for Al being QC-alphabet
for D being non empty set
for b3 being Function of (QC-pred_symbols Al),(relations_on D) holds
( b3 is interpretation of Al,D iff for P being Element of QC-pred_symbols Al
for r being Element of relations_on D holds
( not b3 . P = r or r = empty_rel D or the_arity_of P = the_arity_of r ) );
definition
let Al be QC-alphabet ;
let A be non empty set ;
let k be Element of NAT ;
let J be interpretation of Al,A;
let P be QC-pred_symbol of k,Al;
:: original: .
redefine funcJ . P -> Element of relations_on A;
coherence
J . P is Element of relations_on A by FUNCT_2:5;
end;
definition
let Al be QC-alphabet ;
let A be non empty set ;
let J be interpretation of Al,A;
let p be Element of CQC-WFF Al;
func Valid (p,J) -> Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) means :Def6: :: VALUAT_1:def 6
ex F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) st
( it = F . p & F . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE & ( for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Element of 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)) ) ) );
existence
ex b1 being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) ex F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) st
( b1 = F . p & F . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE & ( for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Element of 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)) ) ) )
proof
deffunc H1( Element of 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);
set D = Funcs ((Valuations_in (Al,A)),BOOLEAN);
set V = In (((Valuations_in (Al,A)) --> TRUE),(Funcs ((Valuations_in (Al,A)),BOOLEAN)));
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)));
consider F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) such that
W1: F . (VERUM Al) = In (((Valuations_in (Al,A)) --> TRUE),(Funcs ((Valuations_in (Al,A)),BOOLEAN))) and
W2: for r, s being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Element of NAT
for l being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F . (P ! l) = H1(k,P,l) & F . ('not' r) = H2(F . r) & F . (r '&' s) = H3(F . r,F . s) & F . (All (x,r)) = H4(x,F . r) ) from CQC_LANG:sch_2();
take F . p ; ::_thesis: ex F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) st
( F . p = F . p & F . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE & ( for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Element of 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)) ) ) )
take F ; ::_thesis: ( F . p = F . p & F . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE & ( for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Element of 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)) ) ) )
thus F . p = F . p ; ::_thesis: ( F . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE & ( for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Element of 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)) ) ) )
(Valuations_in (Al,A)) --> TRUE in Funcs ((Valuations_in (Al,A)),BOOLEAN) by FUNCT_2:8;
hence F . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE by W1, FUNCT_7:def_1; ::_thesis: for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Element of 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)) )
let p, q be Element of CQC-WFF Al; ::_thesis: for x being bound_QC-variable of Al
for k being Element of 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)) )
let x be bound_QC-variable of Al; ::_thesis: for k being Element of 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)) )
let k be Element of NAT ; ::_thesis: 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)) )
let ll be CQC-variable_list of k,Al; ::_thesis: 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)) )
let P be QC-pred_symbol of k,Al; ::_thesis: ( 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)) )
thus F . (P ! ll) = ll 'in' (J . P) by W2; ::_thesis: ( F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) )
X1: 'not' (F . p) in Funcs ((Valuations_in (Al,A)),BOOLEAN) by FUNCT_2:8;
thus F . ('not' p) = H2(F . p) by W2
.= 'not' (F . p) by X1, FUNCT_7:def_1 ; ::_thesis: ( F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) )
X1: (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 W2
.= (F . p) '&' (F . q) by X1, FUNCT_7:def_1 ; ::_thesis: F . (All (x,p)) = FOR_ALL (x,(F . p))
thus F . (All (x,p)) = H4(x,F . p) by W2
.= FOR_ALL (x,(F . p)) by FUNCT_7:def_1 ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) st ex F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) st
( b1 = F . p & F . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE & ( for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Element of 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)) ) ) ) & ex F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) st
( b2 = F . p & F . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE & ( for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Element of 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)) ) ) ) holds
b1 = b2
proof
deffunc H1( Element of 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);
set D = Funcs ((Valuations_in (Al,A)),BOOLEAN);
set V = In (((Valuations_in (Al,A)) --> TRUE),(Funcs ((Valuations_in (Al,A)),BOOLEAN)));
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)));
let d1, d2 be Element of Funcs ((Valuations_in (Al,A)),BOOLEAN); ::_thesis: ( ex F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) st
( d1 = F . p & F . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE & ( for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Element of 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)) ) ) ) & ex F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) st
( d2 = F . p & F . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE & ( for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Element of 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)) ) ) ) implies d1 = d2 )
given F1 being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) such that Z1: d1 = F1 . p and
Z2: F1 . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE and
Z3: for r, s being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Element of NAT
for l being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F1 . (P ! l) = H1(k,P,l) & F1 . ('not' r) = 'not' (F1 . r) & F1 . (r '&' s) = (F1 . r) '&' (F1 . s) & F1 . (All (x,r)) = FOR_ALL (x,(F1 . r)) ) ; ::_thesis: ( for F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) holds
( not d2 = F . p or not F . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE or ex p, q being Element of CQC-WFF Al ex x being bound_QC-variable of Al ex k being Element of NAT ex ll being CQC-variable_list of k,Al ex P being QC-pred_symbol of k,Al st
( F . (P ! ll) = ll 'in' (J . P) & F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) implies not F . (All (x,p)) = FOR_ALL (x,(F . p)) ) ) or d1 = d2 )
Y2: now__::_thesis:_(_F1_._(VERUM_Al)_=_In_(((Valuations_in_(Al,A))_-->_TRUE),(Funcs_((Valuations_in_(Al,A)),BOOLEAN)))_&_(_for_r,_s_being_Element_of_CQC-WFF_Al
for_x_being_bound_QC-variable_of_Al
for_k_being_Element_of_NAT_
for_l_being_CQC-variable_list_of_k,Al
for_P_being_QC-pred_symbol_of_k,Al_holds_
(_F1_._(P_!_l)_=_H1(k,P,l)_&_F1_._('not'_r)_=_H2(F1_._r)_&_F1_._(r_'&'_s)_=_H3(F1_._r,F1_._s)_&_F1_._(All_(x,r))_=_H4(x,F1_._r)_)_)_)
thus F1 . (VERUM Al) = In (((Valuations_in (Al,A)) --> TRUE),(Funcs ((Valuations_in (Al,A)),BOOLEAN))) by Z2, FUNCT_7:def_1; ::_thesis: for r, s being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Element of NAT
for l being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F1 . (P ! l) = H1(k,P,l) & F1 . ('not' r) = H2(F1 . r) & F1 . (r '&' s) = H3(F1 . r,F1 . s) & F1 . (All (x,r)) = H4(x,F1 . r) )
let r, s be Element of CQC-WFF Al; ::_thesis: for x being bound_QC-variable of Al
for k being Element of NAT
for l being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F1 . (P ! l) = H1(k,P,l) & F1 . ('not' r) = H2(F1 . r) & F1 . (r '&' s) = H3(F1 . r,F1 . s) & F1 . (All (x,r)) = H4(x,F1 . r) )
let x be bound_QC-variable of Al; ::_thesis: for k being Element of NAT
for l being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F1 . (P ! l) = H1(k,P,l) & F1 . ('not' r) = H2(F1 . r) & F1 . (r '&' s) = H3(F1 . r,F1 . s) & F1 . (All (x,r)) = H4(x,F1 . r) )
let k be Element of NAT ; ::_thesis: for l being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F1 . (P ! l) = H1(k,P,l) & F1 . ('not' r) = H2(F1 . r) & F1 . (r '&' s) = H3(F1 . r,F1 . s) & F1 . (All (x,r)) = H4(x,F1 . r) )
let l be CQC-variable_list of k,Al; ::_thesis: for P being QC-pred_symbol of k,Al holds
( F1 . (P ! l) = H1(k,P,l) & F1 . ('not' r) = H2(F1 . r) & F1 . (r '&' s) = H3(F1 . r,F1 . s) & F1 . (All (x,r)) = H4(x,F1 . r) )
let P be QC-pred_symbol of k,Al; ::_thesis: ( F1 . (P ! l) = H1(k,P,l) & F1 . ('not' r) = H2(F1 . r) & F1 . (r '&' s) = H3(F1 . r,F1 . s) & F1 . (All (x,r)) = H4(x,F1 . r) )
thus F1 . (P ! l) = H1(k,P,l) by Z3; ::_thesis: ( F1 . ('not' r) = H2(F1 . r) & F1 . (r '&' s) = H3(F1 . r,F1 . s) & F1 . (All (x,r)) = H4(x,F1 . r) )
X1: 'not' (F1 . r) in Funcs ((Valuations_in (Al,A)),BOOLEAN) by FUNCT_2:8;
thus F1 . ('not' r) = 'not' (F1 . r) by Z3
.= H2(F1 . r) by X1, FUNCT_7:def_1 ; ::_thesis: ( F1 . (r '&' s) = H3(F1 . r,F1 . s) & F1 . (All (x,r)) = H4(x,F1 . r) )
X1: (F1 . r) '&' (F1 . s) in Funcs ((Valuations_in (Al,A)),BOOLEAN) by FUNCT_2:8;
thus F1 . (r '&' s) = (F1 . r) '&' (F1 . s) by Z3
.= H3(F1 . r,F1 . s) by X1, FUNCT_7:def_1 ; ::_thesis: F1 . (All (x,r)) = H4(x,F1 . r)
thus F1 . (All (x,r)) = FOR_ALL (x,(F1 . r)) by Z3
.= H4(x,F1 . r) by FUNCT_7:def_1 ; ::_thesis: verum
end;
given F2 being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) such that Z4: d2 = F2 . p and
Z5: F2 . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE and
Z6: for r, s being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Element of NAT
for l being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F2 . (P ! l) = H1(k,P,l) & F2 . ('not' r) = 'not' (F2 . r) & F2 . (r '&' s) = (F2 . r) '&' (F2 . s) & F2 . (All (x,r)) = FOR_ALL (x,(F2 . r)) ) ; ::_thesis: d1 = d2
Y5: now__::_thesis:_(_F2_._(VERUM_Al)_=_In_(((Valuations_in_(Al,A))_-->_TRUE),(Funcs_((Valuations_in_(Al,A)),BOOLEAN)))_&_(_for_r,_s_being_Element_of_CQC-WFF_Al
for_x_being_bound_QC-variable_of_Al
for_k_being_Element_of_NAT_
for_l_being_CQC-variable_list_of_k,Al
for_P_being_QC-pred_symbol_of_k,Al_holds_
(_F2_._(P_!_l)_=_H1(k,P,l)_&_F2_._('not'_r)_=_H2(F2_._r)_&_F2_._(r_'&'_s)_=_H3(F2_._r,F2_._s)_&_F2_._(All_(x,r))_=_H4(x,F2_._r)_)_)_)
thus F2 . (VERUM Al) = In (((Valuations_in (Al,A)) --> TRUE),(Funcs ((Valuations_in (Al,A)),BOOLEAN))) by Z5, FUNCT_7:def_1; ::_thesis: for r, s being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Element of NAT
for l being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F2 . (P ! l) = H1(k,P,l) & F2 . ('not' r) = H2(F2 . r) & F2 . (r '&' s) = H3(F2 . r,F2 . s) & F2 . (All (x,r)) = H4(x,F2 . r) )
let r, s be Element of CQC-WFF Al; ::_thesis: for x being bound_QC-variable of Al
for k being Element of NAT
for l being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F2 . (P ! l) = H1(k,P,l) & F2 . ('not' r) = H2(F2 . r) & F2 . (r '&' s) = H3(F2 . r,F2 . s) & F2 . (All (x,r)) = H4(x,F2 . r) )
let x be bound_QC-variable of Al; ::_thesis: for k being Element of NAT
for l being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F2 . (P ! l) = H1(k,P,l) & F2 . ('not' r) = H2(F2 . r) & F2 . (r '&' s) = H3(F2 . r,F2 . s) & F2 . (All (x,r)) = H4(x,F2 . r) )
let k be Element of NAT ; ::_thesis: for l being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F2 . (P ! l) = H1(k,P,l) & F2 . ('not' r) = H2(F2 . r) & F2 . (r '&' s) = H3(F2 . r,F2 . s) & F2 . (All (x,r)) = H4(x,F2 . r) )
let l be CQC-variable_list of k,Al; ::_thesis: for P being QC-pred_symbol of k,Al holds
( F2 . (P ! l) = H1(k,P,l) & F2 . ('not' r) = H2(F2 . r) & F2 . (r '&' s) = H3(F2 . r,F2 . s) & F2 . (All (x,r)) = H4(x,F2 . r) )
let P be QC-pred_symbol of k,Al; ::_thesis: ( F2 . (P ! l) = H1(k,P,l) & F2 . ('not' r) = H2(F2 . r) & F2 . (r '&' s) = H3(F2 . r,F2 . s) & F2 . (All (x,r)) = H4(x,F2 . r) )
thus F2 . (P ! l) = H1(k,P,l) by Z6; ::_thesis: ( F2 . ('not' r) = H2(F2 . r) & F2 . (r '&' s) = H3(F2 . r,F2 . s) & F2 . (All (x,r)) = H4(x,F2 . r) )
X1: 'not' (F2 . r) in Funcs ((Valuations_in (Al,A)),BOOLEAN) by FUNCT_2:8;
thus F2 . ('not' r) = 'not' (F2 . r) by Z6
.= H2(F2 . r) by X1, FUNCT_7:def_1 ; ::_thesis: ( F2 . (r '&' s) = H3(F2 . r,F2 . s) & F2 . (All (x,r)) = H4(x,F2 . r) )
X1: (F2 . r) '&' (F2 . s) in Funcs ((Valuations_in (Al,A)),BOOLEAN) by FUNCT_2:8;
thus F2 . (r '&' s) = (F2 . r) '&' (F2 . s) by Z6
.= H3(F2 . r,F2 . s) by X1, FUNCT_7:def_1 ; ::_thesis: F2 . (All (x,r)) = H4(x,F2 . r)
thus F2 . (All (x,r)) = FOR_ALL (x,(F2 . r)) by Z6
.= H4(x,F2 . r) by FUNCT_7:def_1 ; ::_thesis: verum
end;
F1 = F2 from CQC_LANG:sch_3(Y2, Y5);
hence d1 = d2 by Z1, Z4; ::_thesis: verum
end;
end;
:: deftheorem Def6 defines Valid VALUAT_1:def_6_:_
for Al being QC-alphabet
for A being non empty set
for J being interpretation of Al,A
for p being Element of CQC-WFF Al
for b5 being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) holds
( b5 = Valid (p,J) iff ex F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) st
( b5 = F . p & F . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE & ( for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Element of 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)) ) ) ) );
Lm1: for Al being 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 Element of 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))) ) )
proof
let Al be QC-alphabet ; ::_thesis: 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 Element of 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; ::_thesis: 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 Element of 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 ; ::_thesis: for J being interpretation of Al,A holds
( Valid ((VERUM Al),J) = (Valuations_in (Al,A)) --> TRUE & ( for k being Element of 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; ::_thesis: ( Valid ((VERUM Al),J) = (Valuations_in (Al,A)) --> TRUE & ( for k being Element of 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( Element of 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 Element of 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; ::_thesis: 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 Element of 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); ::_thesis: ( 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 Element of 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 Element of 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) ) ) ) ) ::_thesis: ( 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 Element of 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) ; ::_thesis: 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 Element of 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
W1: d = F . p and
W2: F . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE and
W3: for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Element of 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 ; ::_thesis: ( 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 Element of 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 W1; ::_thesis: ( 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 Element of 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 W2, FUNCT_7:def_1; ::_thesis: for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Element of 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; ::_thesis: for x being bound_QC-variable of Al
for k being Element of 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; ::_thesis: for k being Element of 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 Element of NAT ; ::_thesis: 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; ::_thesis: 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; ::_thesis: ( 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 W3; ::_thesis: ( F . ('not' p) = H2(F . p) & F . (p '&' q) = H3(F . p,F . q) & F . (All (x,p)) = H4(x,F . p) )
X1: 'not' (F . p) in Funcs ((Valuations_in (Al,A)),BOOLEAN) by FUNCT_2:8;
thus F . ('not' p) = 'not' (F . p) by W3
.= H2(F . p) by X1, FUNCT_7:def_1 ; ::_thesis: ( F . (p '&' q) = H3(F . p,F . q) & F . (All (x,p)) = H4(x,F . p) )
X1: (F . p) '&' (F . q) in Funcs ((Valuations_in (Al,A)),BOOLEAN) by FUNCT_2:8;
thus F . (p '&' q) = (F . p) '&' (F . q) by W3
.= H3(F . p,F . q) by X1, FUNCT_7:def_1 ; ::_thesis: F . (All (x,p)) = H4(x,F . p)
thus F . (All (x,p)) = FOR_ALL (x,(F . p)) by W3
.= H4(x,F . p) by FUNCT_7:def_1 ; ::_thesis: verum
end;
given F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) such that G1: d = F . p and
G2: F . (VERUM Al) = In (((Valuations_in (Al,A)) --> TRUE),(Funcs ((Valuations_in (Al,A)),BOOLEAN))) and
G3: for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Element of 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) ) ; ::_thesis: d = H5(p)
(Valuations_in (Al,A)) --> TRUE in Funcs ((Valuations_in (Al,A)),BOOLEAN) by FUNCT_2:8;
then H2: F . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE by G2, FUNCT_7:def_1;
for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Element of 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; ::_thesis: for x being bound_QC-variable of Al
for k being Element of 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; ::_thesis: for k being Element of 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 Element of NAT ; ::_thesis: 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; ::_thesis: 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; ::_thesis: ( 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 G3; ::_thesis: ( F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) )
X1: 'not' (F . p) in Funcs ((Valuations_in (Al,A)),BOOLEAN) by FUNCT_2:8;
thus F . ('not' p) = H2(F . p) by G3
.= 'not' (F . p) by X1, FUNCT_7:def_1 ; ::_thesis: ( F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) )
X1: (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 G3
.= (F . p) '&' (F . q) by X1, FUNCT_7:def_1 ; ::_thesis: F . (All (x,p)) = FOR_ALL (x,(F . p))
thus F . (All (x,p)) = H4(x,F . p) by G3
.= FOR_ALL (x,(F . p)) by FUNCT_7:def_1 ; ::_thesis: verum
end;
hence d = H5(p) by G1, H2, Def6; ::_thesis: verum
end;
X1: (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 X1, FUNCT_7:def_1; ::_thesis: ( ( for k being Element of 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 ::_thesis: ( ( 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 Element of NAT ; ::_thesis: 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; ::_thesis: 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; ::_thesis: H5(P ! ll) = H1(k,P,ll)
thus H5(P ! ll) = H1(k,P,ll) from CQC_LANG:sch_6(A1); ::_thesis: verum
end;
hereby ::_thesis: ( ( 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; ::_thesis: H5( 'not' p) = 'not' H5(p)
X1: 'not' H5(p) in Funcs ((Valuations_in (Al,A)),BOOLEAN) by FUNCT_2:8;
H5( 'not' p) = H2(H5(p)) from CQC_LANG:sch_7(A1);
hence H5( 'not' p) = 'not' H5(p) by X1, FUNCT_7:def_1; ::_thesis: verum
end;
hereby ::_thesis: for x being bound_QC-variable of Al holds Valid ((All (x,p)),J) = FOR_ALL (x,(Valid (p,J)))
let q be Element of CQC-WFF Al; ::_thesis: H5(p '&' q) = H5(p) '&' H5(q)
X1: H5(p) '&' H5(q) in Funcs ((Valuations_in (Al,A)),BOOLEAN) by FUNCT_2:8;
H5(p '&' q) = H3(H5(p),H5(q)) from CQC_LANG:sch_8(A1);
hence H5(p '&' q) = H5(p) '&' H5(q) by X1, FUNCT_7:def_1; ::_thesis: verum
end;
let x be bound_QC-variable of Al; ::_thesis: 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 FUNCT_7:def_1; ::_thesis: verum
end;
theorem :: VALUAT_1:4
for Al being QC-alphabet
for A being non empty set
for J being interpretation of Al,A holds Valid ((VERUM Al),J) = (Valuations_in (Al,A)) --> TRUE by Lm1;
theorem Th5: :: VALUAT_1:5
for Al being QC-alphabet
for A being non empty set
for v being Element of Valuations_in (Al,A)
for J being interpretation of Al,A holds (Valid ((VERUM Al),J)) . v = TRUE
proof
let Al be QC-alphabet ; ::_thesis: for A being non empty set
for v being Element of Valuations_in (Al,A)
for J being interpretation of Al,A holds (Valid ((VERUM Al),J)) . v = TRUE
let A be non empty set ; ::_thesis: for v being Element of Valuations_in (Al,A)
for J being interpretation of Al,A holds (Valid ((VERUM Al),J)) . v = TRUE
let v be Element of Valuations_in (Al,A); ::_thesis: for J being interpretation of Al,A holds (Valid ((VERUM Al),J)) . v = TRUE
let J be interpretation of Al,A; ::_thesis: (Valid ((VERUM Al),J)) . v = TRUE
((Valuations_in (Al,A)) --> TRUE) . v = TRUE by FUNCOP_1:7;
hence (Valid ((VERUM Al),J)) . v = TRUE by Lm1; ::_thesis: verum
end;
theorem :: VALUAT_1:6
for Al being QC-alphabet
for k being Element of NAT
for A being non empty set
for ll being CQC-variable_list of k,Al
for J being interpretation of Al,A
for P being QC-pred_symbol of k,Al holds Valid ((P ! ll),J) = ll 'in' (J . P) by Lm1;
theorem Th7: :: VALUAT_1:7
for Al being QC-alphabet
for k being Element of NAT
for A being non empty set
for v being Element of Valuations_in (Al,A)
for ll being CQC-variable_list of k,Al
for p being Element of CQC-WFF Al
for J being interpretation of Al,A
for P being QC-pred_symbol of k,Al
for r being Element of relations_on A st p = P ! ll & r = J . P holds
( v *' ll in r iff (Valid (p,J)) . v = TRUE )
proof
let Al be QC-alphabet ; ::_thesis: for k being Element of NAT
for A being non empty set
for v being Element of Valuations_in (Al,A)
for ll being CQC-variable_list of k,Al
for p being Element of CQC-WFF Al
for J being interpretation of Al,A
for P being QC-pred_symbol of k,Al
for r being Element of relations_on A st p = P ! ll & r = J . P holds
( v *' ll in r iff (Valid (p,J)) . v = TRUE )
let k be Element of NAT ; ::_thesis: for A being non empty set
for v being Element of Valuations_in (Al,A)
for ll being CQC-variable_list of k,Al
for p being Element of CQC-WFF Al
for J being interpretation of Al,A
for P being QC-pred_symbol of k,Al
for r being Element of relations_on A st p = P ! ll & r = J . P holds
( v *' ll in r iff (Valid (p,J)) . v = TRUE )
let A be non empty set ; ::_thesis: for v being Element of Valuations_in (Al,A)
for ll being CQC-variable_list of k,Al
for p being Element of CQC-WFF Al
for J being interpretation of Al,A
for P being QC-pred_symbol of k,Al
for r being Element of relations_on A st p = P ! ll & r = J . P holds
( v *' ll in r iff (Valid (p,J)) . v = TRUE )
let v be Element of Valuations_in (Al,A); ::_thesis: for ll being CQC-variable_list of k,Al
for p being Element of CQC-WFF Al
for J being interpretation of Al,A
for P being QC-pred_symbol of k,Al
for r being Element of relations_on A st p = P ! ll & r = J . P holds
( v *' ll in r iff (Valid (p,J)) . v = TRUE )
let ll be CQC-variable_list of k,Al; ::_thesis: for p being Element of CQC-WFF Al
for J being interpretation of Al,A
for P being QC-pred_symbol of k,Al
for r being Element of relations_on A st p = P ! ll & r = J . P holds
( v *' ll in r iff (Valid (p,J)) . v = TRUE )
let p be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A
for P being QC-pred_symbol of k,Al
for r being Element of relations_on A st p = P ! ll & r = J . P holds
( v *' ll in r iff (Valid (p,J)) . v = TRUE )
let J be interpretation of Al,A; ::_thesis: for P being QC-pred_symbol of k,Al
for r being Element of relations_on A st p = P ! ll & r = J . P holds
( v *' ll in r iff (Valid (p,J)) . v = TRUE )
let P be QC-pred_symbol of k,Al; ::_thesis: for r being Element of relations_on A st p = P ! ll & r = J . P holds
( v *' ll in r iff (Valid (p,J)) . v = TRUE )
let r be Element of relations_on A; ::_thesis: ( p = P ! ll & r = J . P implies ( v *' ll in r iff (Valid (p,J)) . v = TRUE ) )
assume that
A1: p = P ! ll and
A2: r = J . P ; ::_thesis: ( v *' ll in r iff (Valid (p,J)) . v = TRUE )
A3: now__::_thesis:_(_(Valid_(p,J))_._v_=_TRUE_implies_v_*'_ll_in_r_)
assume (Valid (p,J)) . v = TRUE ; ::_thesis: v *' ll in r
then (ll 'in' (J . P)) . v <> FALSE by A1, Lm1;
hence v *' ll in r by A2, Def4; ::_thesis: verum
end;
now__::_thesis:_(_v_*'_ll_in_r_implies_(Valid_(p,J))_._v_=_TRUE_)
assume v *' ll in r ; ::_thesis: (Valid (p,J)) . v = TRUE
then (ll 'in' (J . P)) . v = TRUE by A2, Def4;
hence (Valid (p,J)) . v = TRUE by A1, Lm1; ::_thesis: verum
end;
hence ( v *' ll in r iff (Valid (p,J)) . v = TRUE ) by A3; ::_thesis: verum
end;
theorem Th8: :: VALUAT_1:8
for Al being QC-alphabet
for k being Element of NAT
for A being non empty set
for v being Element of Valuations_in (Al,A)
for ll being CQC-variable_list of k,Al
for p being Element of CQC-WFF Al
for J being interpretation of Al,A
for P being QC-pred_symbol of k,Al
for r being Element of relations_on A st p = P ! ll & r = J . P holds
( not v *' ll in r iff (Valid (p,J)) . v = FALSE )
proof
let Al be QC-alphabet ; ::_thesis: for k being Element of NAT
for A being non empty set
for v being Element of Valuations_in (Al,A)
for ll being CQC-variable_list of k,Al
for p being Element of CQC-WFF Al
for J being interpretation of Al,A
for P being QC-pred_symbol of k,Al
for r being Element of relations_on A st p = P ! ll & r = J . P holds
( not v *' ll in r iff (Valid (p,J)) . v = FALSE )
let k be Element of NAT ; ::_thesis: for A being non empty set
for v being Element of Valuations_in (Al,A)
for ll being CQC-variable_list of k,Al
for p being Element of CQC-WFF Al
for J being interpretation of Al,A
for P being QC-pred_symbol of k,Al
for r being Element of relations_on A st p = P ! ll & r = J . P holds
( not v *' ll in r iff (Valid (p,J)) . v = FALSE )
let A be non empty set ; ::_thesis: for v being Element of Valuations_in (Al,A)
for ll being CQC-variable_list of k,Al
for p being Element of CQC-WFF Al
for J being interpretation of Al,A
for P being QC-pred_symbol of k,Al
for r being Element of relations_on A st p = P ! ll & r = J . P holds
( not v *' ll in r iff (Valid (p,J)) . v = FALSE )
let v be Element of Valuations_in (Al,A); ::_thesis: for ll being CQC-variable_list of k,Al
for p being Element of CQC-WFF Al
for J being interpretation of Al,A
for P being QC-pred_symbol of k,Al
for r being Element of relations_on A st p = P ! ll & r = J . P holds
( not v *' ll in r iff (Valid (p,J)) . v = FALSE )
let ll be CQC-variable_list of k,Al; ::_thesis: for p being Element of CQC-WFF Al
for J being interpretation of Al,A
for P being QC-pred_symbol of k,Al
for r being Element of relations_on A st p = P ! ll & r = J . P holds
( not v *' ll in r iff (Valid (p,J)) . v = FALSE )
let p be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A
for P being QC-pred_symbol of k,Al
for r being Element of relations_on A st p = P ! ll & r = J . P holds
( not v *' ll in r iff (Valid (p,J)) . v = FALSE )
let J be interpretation of Al,A; ::_thesis: for P being QC-pred_symbol of k,Al
for r being Element of relations_on A st p = P ! ll & r = J . P holds
( not v *' ll in r iff (Valid (p,J)) . v = FALSE )
let P be QC-pred_symbol of k,Al; ::_thesis: for r being Element of relations_on A st p = P ! ll & r = J . P holds
( not v *' ll in r iff (Valid (p,J)) . v = FALSE )
let r be Element of relations_on A; ::_thesis: ( p = P ! ll & r = J . P implies ( not v *' ll in r iff (Valid (p,J)) . v = FALSE ) )
assume that
A1: p = P ! ll and
A2: r = J . P ; ::_thesis: ( not v *' ll in r iff (Valid (p,J)) . v = FALSE )
A3: now__::_thesis:_(_(Valid_(p,J))_._v_=_FALSE_implies_not_v_*'_ll_in_r_)
assume (Valid (p,J)) . v = FALSE ; ::_thesis: not v *' ll in r
then (ll 'in' (J . P)) . v <> TRUE by A1, Lm1;
hence not v *' ll in r by A2, Def4; ::_thesis: verum
end;
now__::_thesis:_(_not_v_*'_ll_in_r_implies_(Valid_(p,J))_._v_=_FALSE_)
assume not v *' ll in r ; ::_thesis: (Valid (p,J)) . v = FALSE
then (ll 'in' (J . P)) . v = FALSE by A2, Def4;
hence (Valid (p,J)) . v = FALSE by A1, Lm1; ::_thesis: verum
end;
hence ( not v *' ll in r iff (Valid (p,J)) . v = FALSE ) by A3; ::_thesis: verum
end;
theorem :: VALUAT_1:9
for Al being QC-alphabet
for A being non empty set
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds Valid (('not' p),J) = 'not' (Valid (p,J)) by Lm1;
theorem Th10: :: VALUAT_1:10
for Al being QC-alphabet
for A being non empty set
for v being Element of Valuations_in (Al,A)
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds (Valid (('not' p),J)) . v = 'not' ((Valid (p,J)) . v)
proof
let Al be QC-alphabet ; ::_thesis: for A being non empty set
for v being Element of Valuations_in (Al,A)
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds (Valid (('not' p),J)) . v = 'not' ((Valid (p,J)) . v)
let A be non empty set ; ::_thesis: for v being Element of Valuations_in (Al,A)
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds (Valid (('not' p),J)) . v = 'not' ((Valid (p,J)) . v)
let v be Element of Valuations_in (Al,A); ::_thesis: for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds (Valid (('not' p),J)) . v = 'not' ((Valid (p,J)) . v)
let p be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A holds (Valid (('not' p),J)) . v = 'not' ((Valid (p,J)) . v)
let J be interpretation of Al,A; ::_thesis: (Valid (('not' p),J)) . v = 'not' ((Valid (p,J)) . v)
(Valid (('not' p),J)) . v = ('not' (Valid (p,J))) . v by Lm1;
hence (Valid (('not' p),J)) . v = 'not' ((Valid (p,J)) . v) by MARGREL1:def_19; ::_thesis: verum
end;
theorem :: VALUAT_1:11
for Al being QC-alphabet
for A being non empty set
for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A holds Valid ((p '&' q),J) = (Valid (p,J)) '&' (Valid (q,J)) by Lm1;
theorem Th12: :: VALUAT_1:12
for Al being QC-alphabet
for A being non empty set
for v being Element of Valuations_in (Al,A)
for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A holds (Valid ((p '&' q),J)) . v = ((Valid (p,J)) . v) '&' ((Valid (q,J)) . v)
proof
let Al be QC-alphabet ; ::_thesis: for A being non empty set
for v being Element of Valuations_in (Al,A)
for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A holds (Valid ((p '&' q),J)) . v = ((Valid (p,J)) . v) '&' ((Valid (q,J)) . v)
let A be non empty set ; ::_thesis: for v being Element of Valuations_in (Al,A)
for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A holds (Valid ((p '&' q),J)) . v = ((Valid (p,J)) . v) '&' ((Valid (q,J)) . v)
let v be Element of Valuations_in (Al,A); ::_thesis: for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A holds (Valid ((p '&' q),J)) . v = ((Valid (p,J)) . v) '&' ((Valid (q,J)) . v)
let p, q be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A holds (Valid ((p '&' q),J)) . v = ((Valid (p,J)) . v) '&' ((Valid (q,J)) . v)
let J be interpretation of Al,A; ::_thesis: (Valid ((p '&' q),J)) . v = ((Valid (p,J)) . v) '&' ((Valid (q,J)) . v)
(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 MARGREL1:def_20; ::_thesis: verum
end;
theorem :: VALUAT_1:13
for Al being QC-alphabet
for A being non empty set
for x being bound_QC-variable of Al
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds Valid ((All (x,p)),J) = FOR_ALL (x,(Valid (p,J))) by Lm1;
theorem Th14: :: VALUAT_1:14
for Al being QC-alphabet
for A being non empty set
for v being Element of Valuations_in (Al,A)
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds (Valid ((p '&' ('not' p)),J)) . v = FALSE
proof
let Al be QC-alphabet ; ::_thesis: for A being non empty set
for v being Element of Valuations_in (Al,A)
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds (Valid ((p '&' ('not' p)),J)) . v = FALSE
let A be non empty set ; ::_thesis: for v being Element of Valuations_in (Al,A)
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds (Valid ((p '&' ('not' p)),J)) . v = FALSE
let v be Element of Valuations_in (Al,A); ::_thesis: for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds (Valid ((p '&' ('not' p)),J)) . v = FALSE
let p be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A holds (Valid ((p '&' ('not' p)),J)) . v = FALSE
let J be interpretation of Al,A; ::_thesis: (Valid ((p '&' ('not' p)),J)) . v = FALSE
A1: now__::_thesis:_(_(Valid_(p,J))_._v_=_TRUE_implies_((Valid_(p,J))_._v)_'&'_('not'_((Valid_(p,J))_._v))_=_FALSE_)
assume (Valid (p,J)) . v = TRUE ; ::_thesis: ((Valid (p,J)) . v) '&' ('not' ((Valid (p,J)) . v)) = FALSE
then 'not' ((Valid (p,J)) . v) = FALSE by MARGREL1:11;
hence ((Valid (p,J)) . v) '&' ('not' ((Valid (p,J)) . v)) = FALSE by MARGREL1:12; ::_thesis: verum
end;
A2: ( (Valid (p,J)) . v = FALSE implies ((Valid (p,J)) . v) '&' ('not' ((Valid (p,J)) . v)) = FALSE ) by MARGREL1:12;
(Valid ((p '&' ('not' p)),J)) . v = ((Valid (p,J)) . v) '&' ((Valid (('not' p),J)) . v) by Th12
.= ((Valid (p,J)) . v) '&' ('not' ((Valid (p,J)) . v)) by Th10 ;
hence (Valid ((p '&' ('not' p)),J)) . v = FALSE by A1, A2, XBOOLEAN:def_3; ::_thesis: verum
end;
theorem :: VALUAT_1:15
for Al being QC-alphabet
for A being non empty set
for v being Element of Valuations_in (Al,A)
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds (Valid (('not' (p '&' ('not' p))),J)) . v = TRUE
proof
let Al be QC-alphabet ; ::_thesis: for A being non empty set
for v being Element of Valuations_in (Al,A)
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds (Valid (('not' (p '&' ('not' p))),J)) . v = TRUE
let A be non empty set ; ::_thesis: for v being Element of Valuations_in (Al,A)
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds (Valid (('not' (p '&' ('not' p))),J)) . v = TRUE
let v be Element of Valuations_in (Al,A); ::_thesis: for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds (Valid (('not' (p '&' ('not' p))),J)) . v = TRUE
let p be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A holds (Valid (('not' (p '&' ('not' p))),J)) . v = TRUE
let J be interpretation of Al,A; ::_thesis: (Valid (('not' (p '&' ('not' p))),J)) . v = TRUE
(Valid (('not' (p '&' ('not' p))),J)) . v = 'not' ((Valid ((p '&' ('not' p)),J)) . v) by Th10
.= 'not' FALSE by Th14 ;
hence (Valid (('not' (p '&' ('not' p))),J)) . v = TRUE by MARGREL1:11; ::_thesis: verum
end;
definition
let Al be QC-alphabet ;
let A be non empty set ;
let p be Element of CQC-WFF Al;
let J be interpretation of Al,A;
let v be Element of Valuations_in (Al,A);
predJ,v |= p means :Def7: :: VALUAT_1:def 7
(Valid (p,J)) . v = TRUE ;
end;
:: deftheorem Def7 defines |= VALUAT_1:def_7_:_
for Al being QC-alphabet
for A being non empty set
for p being Element of CQC-WFF Al
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) holds
( J,v |= p iff (Valid (p,J)) . v = TRUE );
theorem :: VALUAT_1:16
for Al being QC-alphabet
for k being Element of NAT
for A being non empty set
for v being Element of Valuations_in (Al,A)
for ll being CQC-variable_list of k,Al
for J being interpretation of Al,A
for P being QC-pred_symbol of k,Al holds
( J,v |= P ! ll iff (ll 'in' (J . P)) . v = TRUE )
proof
let Al be QC-alphabet ; ::_thesis: for k being Element of NAT
for A being non empty set
for v being Element of Valuations_in (Al,A)
for ll being CQC-variable_list of k,Al
for J being interpretation of Al,A
for P being QC-pred_symbol of k,Al holds
( J,v |= P ! ll iff (ll 'in' (J . P)) . v = TRUE )
let k be Element of NAT ; ::_thesis: for A being non empty set
for v being Element of Valuations_in (Al,A)
for ll being CQC-variable_list of k,Al
for J being interpretation of Al,A
for P being QC-pred_symbol of k,Al holds
( J,v |= P ! ll iff (ll 'in' (J . P)) . v = TRUE )
let A be non empty set ; ::_thesis: for v being Element of Valuations_in (Al,A)
for ll being CQC-variable_list of k,Al
for J being interpretation of Al,A
for P being QC-pred_symbol of k,Al holds
( J,v |= P ! ll iff (ll 'in' (J . P)) . v = TRUE )
let v be Element of Valuations_in (Al,A); ::_thesis: for ll being CQC-variable_list of k,Al
for J being interpretation of Al,A
for P being QC-pred_symbol of k,Al holds
( J,v |= P ! ll iff (ll 'in' (J . P)) . v = TRUE )
let ll be CQC-variable_list of k,Al; ::_thesis: for J being interpretation of Al,A
for P being QC-pred_symbol of k,Al holds
( J,v |= P ! ll iff (ll 'in' (J . P)) . v = TRUE )
let J be interpretation of Al,A; ::_thesis: for P being QC-pred_symbol of k,Al holds
( J,v |= P ! ll iff (ll 'in' (J . P)) . v = TRUE )
let P be QC-pred_symbol of k,Al; ::_thesis: ( J,v |= P ! ll iff (ll 'in' (J . P)) . v = TRUE )
A1: now__::_thesis:_(_(ll_'in'_(J_._P))_._v_=_TRUE_implies_J,v_|=_P_!_ll_)
assume (ll 'in' (J . P)) . v = TRUE ; ::_thesis: J,v |= P ! ll
then (Valid ((P ! ll),J)) . v = TRUE by Lm1;
hence J,v |= P ! ll by Def7; ::_thesis: verum
end;
now__::_thesis:_(_J,v_|=_P_!_ll_implies_(ll_'in'_(J_._P))_._v_=_TRUE_)
assume J,v |= P ! ll ; ::_thesis: (ll 'in' (J . P)) . v = TRUE
then (Valid ((P ! ll),J)) . v = TRUE by Def7;
hence (ll 'in' (J . P)) . v = TRUE by Lm1; ::_thesis: verum
end;
hence ( J,v |= P ! ll iff (ll 'in' (J . P)) . v = TRUE ) by A1; ::_thesis: verum
end;
theorem :: VALUAT_1:17
for Al being QC-alphabet
for A being non empty set
for v being Element of Valuations_in (Al,A)
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds
( J,v |= 'not' p iff not J,v |= p )
proof
let Al be QC-alphabet ; ::_thesis: for A being non empty set
for v being Element of Valuations_in (Al,A)
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds
( J,v |= 'not' p iff not J,v |= p )
let A be non empty set ; ::_thesis: for v being Element of Valuations_in (Al,A)
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds
( J,v |= 'not' p iff not J,v |= p )
let v be Element of Valuations_in (Al,A); ::_thesis: for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds
( J,v |= 'not' p iff not J,v |= p )
let p be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A holds
( J,v |= 'not' p iff not J,v |= p )
let J be interpretation of Al,A; ::_thesis: ( J,v |= 'not' p iff not J,v |= p )
A1: now__::_thesis:_(_not_J,v_|=_p_implies_J,v_|=_'not'_p_)
assume not J,v |= p ; ::_thesis: J,v |= 'not' p
then not (Valid (p,J)) . v = TRUE by Def7;
then (Valid (p,J)) . v = FALSE by XBOOLEAN:def_3;
then 'not' ((Valid (p,J)) . v) = TRUE by MARGREL1:11;
then ('not' (Valid (p,J))) . v = TRUE by MARGREL1:def_19;
then (Valid (('not' p),J)) . v = TRUE by Lm1;
hence J,v |= 'not' p by Def7; ::_thesis: verum
end;
now__::_thesis:_(_J,v_|=_'not'_p_implies_not_J,v_|=_p_)
assume J,v |= 'not' p ; ::_thesis: not J,v |= p
then (Valid (('not' p),J)) . v = TRUE by Def7;
then ('not' (Valid (p,J))) . v = TRUE by Lm1;
then 'not' ((Valid (p,J)) . v) = TRUE by MARGREL1:def_19;
then (Valid (p,J)) . v = FALSE by MARGREL1:11;
hence not J,v |= p by Def7; ::_thesis: verum
end;
hence ( J,v |= 'not' p iff not J,v |= p ) by A1; ::_thesis: verum
end;
theorem :: VALUAT_1:18
for Al being QC-alphabet
for A being non empty set
for v being Element of Valuations_in (Al,A)
for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A holds
( J,v |= p '&' q iff ( J,v |= p & J,v |= q ) )
proof
let Al be QC-alphabet ; ::_thesis: for A being non empty set
for v being Element of Valuations_in (Al,A)
for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A holds
( J,v |= p '&' q iff ( J,v |= p & J,v |= q ) )
let A be non empty set ; ::_thesis: for v being Element of Valuations_in (Al,A)
for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A holds
( J,v |= p '&' q iff ( J,v |= p & J,v |= q ) )
let v be Element of Valuations_in (Al,A); ::_thesis: for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A holds
( J,v |= p '&' q iff ( J,v |= p & J,v |= q ) )
let p, q be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A holds
( J,v |= p '&' q iff ( J,v |= p & J,v |= q ) )
let J be interpretation of Al,A; ::_thesis: ( J,v |= p '&' q iff ( J,v |= p & J,v |= q ) )
A1: now__::_thesis:_(_J,v_|=_p_&_J,v_|=_q_implies_J,v_|=_p_'&'_q_)
assume ( J,v |= p & J,v |= q ) ; ::_thesis: J,v |= p '&' q
then ( (Valid (p,J)) . v = TRUE & (Valid (q,J)) . v = TRUE ) by Def7;
then ((Valid (p,J)) . v) '&' ((Valid (q,J)) . v) = TRUE ;
then ((Valid (p,J)) '&' (Valid (q,J))) . v = TRUE by MARGREL1:def_20;
then (Valid ((p '&' q),J)) . v = TRUE by Lm1;
hence J,v |= p '&' q by Def7; ::_thesis: verum
end;
now__::_thesis:_(_J,v_|=_p_'&'_q_implies_(_J,v_|=_p_&_J,v_|=_q_)_)
assume J,v |= p '&' q ; ::_thesis: ( J,v |= p & J,v |= q )
then (Valid ((p '&' q),J)) . v = TRUE by Def7;
then ((Valid (p,J)) '&' (Valid (q,J))) . v = TRUE by Lm1;
then ((Valid (p,J)) . v) '&' ((Valid (q,J)) . v) = TRUE by MARGREL1:def_20;
then ( (Valid (p,J)) . v = TRUE & (Valid (q,J)) . v = TRUE ) by MARGREL1:12;
hence ( J,v |= p & J,v |= q ) by Def7; ::_thesis: verum
end;
hence ( J,v |= p '&' q iff ( J,v |= p & J,v |= q ) ) by A1; ::_thesis: verum
end;
theorem Th19: :: VALUAT_1:19
for Al being QC-alphabet
for A being non empty set
for x being bound_QC-variable of Al
for v being Element of Valuations_in (Al,A)
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds
( J,v |= All (x,p) iff (FOR_ALL (x,(Valid (p,J)))) . v = TRUE )
proof
let Al be QC-alphabet ; ::_thesis: for A being non empty set
for x being bound_QC-variable of Al
for v being Element of Valuations_in (Al,A)
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds
( J,v |= All (x,p) iff (FOR_ALL (x,(Valid (p,J)))) . v = TRUE )
let A be non empty set ; ::_thesis: for x being bound_QC-variable of Al
for v being Element of Valuations_in (Al,A)
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds
( J,v |= All (x,p) iff (FOR_ALL (x,(Valid (p,J)))) . v = TRUE )
let x be bound_QC-variable of Al; ::_thesis: for v being Element of Valuations_in (Al,A)
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds
( J,v |= All (x,p) iff (FOR_ALL (x,(Valid (p,J)))) . v = TRUE )
let v be Element of Valuations_in (Al,A); ::_thesis: for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds
( J,v |= All (x,p) iff (FOR_ALL (x,(Valid (p,J)))) . v = TRUE )
let p be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A holds
( J,v |= All (x,p) iff (FOR_ALL (x,(Valid (p,J)))) . v = TRUE )
let J be interpretation of Al,A; ::_thesis: ( J,v |= All (x,p) iff (FOR_ALL (x,(Valid (p,J)))) . v = TRUE )
A1: now__::_thesis:_(_(FOR_ALL_(x,(Valid_(p,J))))_._v_=_TRUE_implies_J,v_|=_All_(x,p)_)
assume (FOR_ALL (x,(Valid (p,J)))) . v = TRUE ; ::_thesis: J,v |= All (x,p)
then (Valid ((All (x,p)),J)) . v = TRUE by Lm1;
hence J,v |= All (x,p) by Def7; ::_thesis: verum
end;
now__::_thesis:_(_J,v_|=_All_(x,p)_implies_(FOR_ALL_(x,(Valid_(p,J))))_._v_=_TRUE_)
assume J,v |= All (x,p) ; ::_thesis: (FOR_ALL (x,(Valid (p,J)))) . v = TRUE
then (Valid ((All (x,p)),J)) . v = TRUE by Def7;
hence (FOR_ALL (x,(Valid (p,J)))) . v = TRUE by Lm1; ::_thesis: verum
end;
hence ( J,v |= All (x,p) iff (FOR_ALL (x,(Valid (p,J)))) . v = TRUE ) by A1; ::_thesis: verum
end;
theorem Th20: :: VALUAT_1:20
for Al being QC-alphabet
for A being non empty set
for x being bound_QC-variable of Al
for v being Element of Valuations_in (Al,A)
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds
( J,v |= All (x,p) iff for v1 being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
v1 . y = v . y ) holds
(Valid (p,J)) . v1 = TRUE )
proof
let Al be QC-alphabet ; ::_thesis: for A being non empty set
for x being bound_QC-variable of Al
for v being Element of Valuations_in (Al,A)
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds
( J,v |= All (x,p) iff for v1 being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
v1 . y = v . y ) holds
(Valid (p,J)) . v1 = TRUE )
let A be non empty set ; ::_thesis: for x being bound_QC-variable of Al
for v being Element of Valuations_in (Al,A)
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds
( J,v |= All (x,p) iff for v1 being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
v1 . y = v . y ) holds
(Valid (p,J)) . v1 = TRUE )
let x be bound_QC-variable of Al; ::_thesis: for v being Element of Valuations_in (Al,A)
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds
( J,v |= All (x,p) iff for v1 being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
v1 . y = v . y ) holds
(Valid (p,J)) . v1 = TRUE )
let v be Element of Valuations_in (Al,A); ::_thesis: for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds
( J,v |= All (x,p) iff for v1 being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
v1 . y = v . y ) holds
(Valid (p,J)) . v1 = TRUE )
let p be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A holds
( J,v |= All (x,p) iff for v1 being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
v1 . y = v . y ) holds
(Valid (p,J)) . v1 = TRUE )
let J be interpretation of Al,A; ::_thesis: ( J,v |= All (x,p) iff for v1 being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
v1 . y = v . y ) holds
(Valid (p,J)) . v1 = TRUE )
hereby ::_thesis: ( ( for v1 being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
v1 . y = v . y ) holds
(Valid (p,J)) . v1 = TRUE ) implies J,v |= All (x,p) )
assume J,v |= All (x,p) ; ::_thesis: for v1 being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
v1 . y = v . y ) holds
(Valid (p,J)) . v1 = TRUE
then (FOR_ALL (x,(Valid (p,J)))) . v = TRUE by Th19;
hence for v1 being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
v1 . y = v . y ) holds
(Valid (p,J)) . v1 = TRUE by Th3; ::_thesis: verum
end;
assume for v1 being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
v1 . y = v . y ) holds
(Valid (p,J)) . v1 = TRUE ; ::_thesis: J,v |= All (x,p)
then (FOR_ALL (x,(Valid (p,J)))) . v = TRUE by Th3;
hence J,v |= All (x,p) by Th19; ::_thesis: verum
end;
theorem :: VALUAT_1:21
for Al being QC-alphabet
for A being non empty set
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds Valid (('not' ('not' p)),J) = Valid (p,J)
proof
let Al be QC-alphabet ; ::_thesis: for A being non empty set
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds Valid (('not' ('not' p)),J) = Valid (p,J)
let A be non empty set ; ::_thesis: for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds Valid (('not' ('not' p)),J) = Valid (p,J)
let p be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A holds Valid (('not' ('not' p)),J) = Valid (p,J)
let J be interpretation of Al,A; ::_thesis: Valid (('not' ('not' p)),J) = Valid (p,J)
now__::_thesis:_for_v_being_Element_of_Valuations_in_(Al,A)_holds_(Valid_(('not'_('not'_p)),J))_._v_=_(Valid_(p,J))_._v
let v be Element of Valuations_in (Al,A); ::_thesis: (Valid (('not' ('not' p)),J)) . v = (Valid (p,J)) . v
thus (Valid (('not' ('not' p)),J)) . v = 'not' ((Valid (('not' p),J)) . v) by Th10
.= 'not' ('not' ((Valid (p,J)) . v)) by Th10
.= (Valid (p,J)) . v ; ::_thesis: verum
end;
hence Valid (('not' ('not' p)),J) = Valid (p,J) by FUNCT_2:63; ::_thesis: verum
end;
theorem Th22: :: VALUAT_1:22
for Al being QC-alphabet
for A being non empty set
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds Valid ((p '&' p),J) = Valid (p,J)
proof
let Al be QC-alphabet ; ::_thesis: for A being non empty set
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds Valid ((p '&' p),J) = Valid (p,J)
let A be non empty set ; ::_thesis: for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds Valid ((p '&' p),J) = Valid (p,J)
let p be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A holds Valid ((p '&' p),J) = Valid (p,J)
let J be interpretation of Al,A; ::_thesis: Valid ((p '&' p),J) = Valid (p,J)
now__::_thesis:_for_v_being_Element_of_Valuations_in_(Al,A)_holds_(Valid_((p_'&'_p),J))_._v_=_(Valid_(p,J))_._v
let v be Element of Valuations_in (Al,A); ::_thesis: (Valid ((p '&' p),J)) . v = (Valid (p,J)) . v
thus (Valid ((p '&' p),J)) . v = ((Valid (p,J)) . v) '&' ((Valid (p,J)) . v) by Th12
.= (Valid (p,J)) . v ; ::_thesis: verum
end;
hence Valid ((p '&' p),J) = Valid (p,J) by FUNCT_2:63; ::_thesis: verum
end;
theorem Th23: :: VALUAT_1:23
for Al being QC-alphabet
for A being non empty set
for v being Element of Valuations_in (Al,A)
for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A holds
( J,v |= p => q iff ( (Valid (p,J)) . v = FALSE or (Valid (q,J)) . v = TRUE ) )
proof
let Al be QC-alphabet ; ::_thesis: for A being non empty set
for v being Element of Valuations_in (Al,A)
for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A holds
( J,v |= p => q iff ( (Valid (p,J)) . v = FALSE or (Valid (q,J)) . v = TRUE ) )
let A be non empty set ; ::_thesis: for v being Element of Valuations_in (Al,A)
for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A holds
( J,v |= p => q iff ( (Valid (p,J)) . v = FALSE or (Valid (q,J)) . v = TRUE ) )
let v be Element of Valuations_in (Al,A); ::_thesis: for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A holds
( J,v |= p => q iff ( (Valid (p,J)) . v = FALSE or (Valid (q,J)) . v = TRUE ) )
let p, q be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A holds
( J,v |= p => q iff ( (Valid (p,J)) . v = FALSE or (Valid (q,J)) . v = TRUE ) )
let J be interpretation of Al,A; ::_thesis: ( J,v |= p => q iff ( (Valid (p,J)) . v = FALSE or (Valid (q,J)) . v = TRUE ) )
A1: now__::_thesis:_(_(_(Valid_(p,J))_._v_=_FALSE_or_(Valid_(q,J))_._v_=_TRUE_)_implies_J,v_|=_p_=>_q_)
A2: now__::_thesis:_(_(Valid_(q,J))_._v_=_TRUE_implies_J,v_|=_p_=>_q_)
assume A3: (Valid (q,J)) . v = TRUE ; ::_thesis: J,v |= p => q
assume not J,v |= p => q ; ::_thesis: contradiction
then (Valid ((p => q),J)) . v <> TRUE by Def7;
then (Valid ((p => q),J)) . v = FALSE by XBOOLEAN:def_3;
then (Valid (('not' (p '&' ('not' q))),J)) . v = FALSE by QC_LANG2:def_2;
then 'not' ((Valid ((p '&' ('not' q)),J)) . v) = FALSE by Th10;
then (Valid ((p '&' ('not' q)),J)) . v = TRUE by MARGREL1:11;
then ((Valid (p,J)) . v) '&' ((Valid (('not' q),J)) . v) = TRUE by Th12;
then ((Valid (p,J)) . v) '&' ('not' ((Valid (q,J)) . v)) = TRUE by Th10;
then 'not' ((Valid (q,J)) . v) = TRUE by MARGREL1:12;
hence contradiction by A3, MARGREL1:11; ::_thesis: verum
end;
A4: now__::_thesis:_(_(Valid_(p,J))_._v_=_FALSE_implies_J,v_|=_p_=>_q_)
assume (Valid (p,J)) . v = FALSE ; ::_thesis: J,v |= p => q
then ((Valid (p,J)) . v) '&' ((Valid (('not' q),J)) . v) = FALSE by MARGREL1:12;
then (Valid ((p '&' ('not' q)),J)) . v = FALSE by Th12;
then 'not' ((Valid ((p '&' ('not' q)),J)) . v) = TRUE by MARGREL1:11;
then (Valid (('not' (p '&' ('not' q))),J)) . v = TRUE by Th10;
then (Valid ((p => q),J)) . v = TRUE by QC_LANG2:def_2;
hence J,v |= p => q by Def7; ::_thesis: verum
end;
assume ( (Valid (p,J)) . v = FALSE or (Valid (q,J)) . v = TRUE ) ; ::_thesis: J,v |= p => q
hence J,v |= p => q by A4, A2; ::_thesis: verum
end;
now__::_thesis:_(_not_J,v_|=_p_=>_q_or_(Valid_(p,J))_._v_=_FALSE_or_(Valid_(q,J))_._v_=_TRUE_)
assume J,v |= p => q ; ::_thesis: ( (Valid (p,J)) . v = FALSE or (Valid (q,J)) . v = TRUE )
then (Valid ((p => q),J)) . v = TRUE by Def7;
then (Valid (('not' (p '&' ('not' q))),J)) . v = TRUE by QC_LANG2:def_2;
then 'not' ((Valid ((p '&' ('not' q)),J)) . v) = TRUE by Th10;
then (Valid ((p '&' ('not' q)),J)) . v = FALSE by MARGREL1:11;
then ((Valid (p,J)) . v) '&' ((Valid (('not' q),J)) . v) = FALSE by Th12;
then ((Valid (p,J)) . v) '&' ('not' ((Valid (q,J)) . v)) = FALSE by Th10;
then ( (Valid (p,J)) . v = FALSE or 'not' ((Valid (q,J)) . v) = FALSE ) by MARGREL1:12;
hence ( (Valid (p,J)) . v = FALSE or (Valid (q,J)) . v = TRUE ) by MARGREL1:11; ::_thesis: verum
end;
hence ( J,v |= p => q iff ( (Valid (p,J)) . v = FALSE or (Valid (q,J)) . v = TRUE ) ) by A1; ::_thesis: verum
end;
theorem Th24: :: VALUAT_1:24
for Al being QC-alphabet
for A being non empty set
for v being Element of Valuations_in (Al,A)
for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A holds
( J,v |= p => q iff ( J,v |= p implies J,v |= q ) )
proof
let Al be QC-alphabet ; ::_thesis: for A being non empty set
for v being Element of Valuations_in (Al,A)
for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A holds
( J,v |= p => q iff ( J,v |= p implies J,v |= q ) )
let A be non empty set ; ::_thesis: for v being Element of Valuations_in (Al,A)
for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A holds
( J,v |= p => q iff ( J,v |= p implies J,v |= q ) )
let v be Element of Valuations_in (Al,A); ::_thesis: for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A holds
( J,v |= p => q iff ( J,v |= p implies J,v |= q ) )
let p, q be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A holds
( J,v |= p => q iff ( J,v |= p implies J,v |= q ) )
let J be interpretation of Al,A; ::_thesis: ( J,v |= p => q iff ( J,v |= p implies J,v |= q ) )
hereby ::_thesis: ( ( J,v |= p implies J,v |= q ) implies J,v |= p => q )
assume J,v |= p => q ; ::_thesis: ( J,v |= p implies J,v |= q )
then ( (Valid (p,J)) . v = FALSE or (Valid (q,J)) . v = TRUE ) by Th23;
hence ( J,v |= p implies J,v |= q ) by Def7; ::_thesis: verum
end;
assume ( J,v |= p implies J,v |= q ) ; ::_thesis: J,v |= p => q
then ( (Valid (p,J)) . v = TRUE implies (Valid (q,J)) . v = TRUE ) by Def7;
then ( (Valid (p,J)) . v = FALSE or (Valid (q,J)) . v = TRUE ) by XBOOLEAN:def_3;
hence J,v |= p => q by Th23; ::_thesis: verum
end;
theorem Th25: :: VALUAT_1:25
for Al being QC-alphabet
for A being non empty set
for x being bound_QC-variable of Al
for v being Element of Valuations_in (Al,A)
for p being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) st (FOR_ALL (x,p)) . v = TRUE holds
p . v = TRUE
proof
let Al be QC-alphabet ; ::_thesis: for A being non empty set
for x being bound_QC-variable of Al
for v being Element of Valuations_in (Al,A)
for p being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) st (FOR_ALL (x,p)) . v = TRUE holds
p . v = TRUE
let A be non empty set ; ::_thesis: for x being bound_QC-variable of Al
for v being Element of Valuations_in (Al,A)
for p being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) st (FOR_ALL (x,p)) . v = TRUE holds
p . v = TRUE
let x be bound_QC-variable of Al; ::_thesis: for v being Element of Valuations_in (Al,A)
for p being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) st (FOR_ALL (x,p)) . v = TRUE holds
p . v = TRUE
let v be Element of Valuations_in (Al,A); ::_thesis: for p being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) st (FOR_ALL (x,p)) . v = TRUE holds
p . v = TRUE
let p be Element of Funcs ((Valuations_in (Al,A)),BOOLEAN); ::_thesis: ( (FOR_ALL (x,p)) . v = TRUE implies p . v = TRUE )
for y being bound_QC-variable of Al st x <> y holds
v . y = v . y ;
hence ( (FOR_ALL (x,p)) . v = TRUE implies p . v = TRUE ) by Th3; ::_thesis: verum
end;
definition
let Al be QC-alphabet ;
let A be non empty set ;
let J be interpretation of Al,A;
let p be Element of CQC-WFF Al;
predJ |= p means :Def8: :: VALUAT_1:def 8
for v being Element of Valuations_in (Al,A) holds J,v |= p;
end;
:: deftheorem Def8 defines |= VALUAT_1:def_8_:_
for Al being QC-alphabet
for A being non empty set
for J being interpretation of Al,A
for p being Element of CQC-WFF Al holds
( J |= p iff for v being Element of Valuations_in (Al,A) holds J,v |= p );
Lm2: for u, w, z being Element of BOOLEAN holds 'not' (('not' (u '&' ('not' w))) '&' (('not' (w '&' z)) '&' (u '&' z))) = TRUE
proof
let u, w, z be Element of BOOLEAN ; ::_thesis: 'not' (('not' (u '&' ('not' w))) '&' (('not' (w '&' z)) '&' (u '&' z))) = TRUE
percases ( ( z = TRUE & w = TRUE ) or ( w = FALSE & u = TRUE ) or u = FALSE or z = FALSE ) by XBOOLEAN:def_3;
suppose ( z = TRUE & w = TRUE ) ; ::_thesis: 'not' (('not' (u '&' ('not' w))) '&' (('not' (w '&' z)) '&' (u '&' z))) = TRUE
then 'not' (w '&' z) = FALSE by MARGREL1:11;
then ('not' (w '&' z)) '&' (u '&' z) = FALSE by MARGREL1:12;
then ('not' (u '&' ('not' w))) '&' (('not' (w '&' z)) '&' (u '&' z)) = FALSE by MARGREL1:12;
hence 'not' (('not' (u '&' ('not' w))) '&' (('not' (w '&' z)) '&' (u '&' z))) = TRUE by MARGREL1:11; ::_thesis: verum
end;
supposethat A1: w = FALSE and
A2: u = TRUE ; ::_thesis: 'not' (('not' (u '&' ('not' w))) '&' (('not' (w '&' z)) '&' (u '&' z))) = TRUE
'not' w = TRUE by A1, MARGREL1:11;
then 'not' (u '&' ('not' w)) = FALSE by A2, MARGREL1:11;
then ('not' (u '&' ('not' w))) '&' (('not' (w '&' z)) '&' (u '&' z)) = FALSE by MARGREL1:12;
hence 'not' (('not' (u '&' ('not' w))) '&' (('not' (w '&' z)) '&' (u '&' z))) = TRUE by MARGREL1:11; ::_thesis: verum
end;
suppose u = FALSE ; ::_thesis: 'not' (('not' (u '&' ('not' w))) '&' (('not' (w '&' z)) '&' (u '&' z))) = TRUE
then u '&' z = FALSE by MARGREL1:12;
then ('not' (w '&' z)) '&' (u '&' z) = FALSE by MARGREL1:12;
then ('not' (u '&' ('not' w))) '&' (('not' (w '&' z)) '&' (u '&' z)) = FALSE by MARGREL1:12;
hence 'not' (('not' (u '&' ('not' w))) '&' (('not' (w '&' z)) '&' (u '&' z))) = TRUE by MARGREL1:11; ::_thesis: verum
end;
suppose z = FALSE ; ::_thesis: 'not' (('not' (u '&' ('not' w))) '&' (('not' (w '&' z)) '&' (u '&' z))) = TRUE
then u '&' z = FALSE by MARGREL1:12;
then ('not' (w '&' z)) '&' (u '&' z) = FALSE by MARGREL1:12;
then ('not' (u '&' ('not' w))) '&' (('not' (w '&' z)) '&' (u '&' z)) = FALSE by MARGREL1:12;
hence 'not' (('not' (u '&' ('not' w))) '&' (('not' (w '&' z)) '&' (u '&' z))) = TRUE by MARGREL1:11; ::_thesis: verum
end;
end;
end;
Lm3: now__::_thesis:_for_Al_being_QC-alphabet_
for_A_being_non_empty_set_
for_Y,_Z_being_bound_QC-variable_of_Al
for_V1,_V2_being_Element_of_Valuations_in_(Al,A)_ex_v_being_Element_of_Valuations_in_(Al,A)_st_
(_(_for_x_being_bound_QC-variable_of_Al_st_x_<>_Y_holds_
v_._x_=_V1_._x_)_&_v_._Y_=_V2_._Z_)
let Al be QC-alphabet ; ::_thesis: for A being non empty set
for Y, Z being bound_QC-variable of Al
for V1, V2 being Element of Valuations_in (Al,A) ex v being Element of Valuations_in (Al,A) st
( ( for x being bound_QC-variable of Al st x <> Y holds
v . x = V1 . x ) & v . Y = V2 . Z )
let A be non empty set ; ::_thesis: for Y, Z being bound_QC-variable of Al
for V1, V2 being Element of Valuations_in (Al,A) ex v being Element of Valuations_in (Al,A) st
( ( for x being bound_QC-variable of Al st x <> Y holds
v . x = V1 . x ) & v . Y = V2 . Z )
let Y, Z be bound_QC-variable of Al; ::_thesis: for V1, V2 being Element of Valuations_in (Al,A) ex v being Element of Valuations_in (Al,A) st
( ( for x being bound_QC-variable of Al st x <> Y holds
v . x = V1 . x ) & v . Y = V2 . Z )
let V1, V2 be Element of Valuations_in (Al,A); ::_thesis: ex v being Element of Valuations_in (Al,A) st
( ( for x being bound_QC-variable of Al st x <> Y holds
v . x = V1 . x ) & v . Y = V2 . Z )
thus ex v being Element of Valuations_in (Al,A) st
( ( for x being bound_QC-variable of Al st x <> Y holds
v . x = V1 . x ) & v . Y = V2 . Z ) ::_thesis: verum
proof
deffunc H1( set ) -> Element of A = V2 . Z;
deffunc H2( set ) -> set = V1 . $1;
defpred S1[ set ] means for x1 being bound_QC-variable of Al st x1 = $1 holds
x1 <> Y;
A1: for x being set st x in bound_QC-variables Al holds
( ( S1[x] implies H2(x) in A ) & ( not S1[x] implies H1(x) in A ) ) by FUNCT_2:5;
consider f being Function of (bound_QC-variables Al),A such that
A2: for x being set st x in bound_QC-variables Al holds
( ( S1[x] implies f . x = H2(x) ) & ( not S1[x] implies f . x = H1(x) ) ) from FUNCT_2:sch_5(A1);
( dom f = bound_QC-variables Al & rng f c= A ) by FUNCT_2:def_1, RELAT_1:def_19;
then reconsider f = f as Element of Valuations_in (Al,A) by FUNCT_2:def_2;
take f ; ::_thesis: ( ( for x being bound_QC-variable of Al st x <> Y holds
f . x = V1 . x ) & f . Y = V2 . Z )
now__::_thesis:_for_x_being_bound_QC-variable_of_Al_holds_
(_(_x_<>_Y_implies_f_._x_=_V1_._x_)_&_(_x_=_Y_implies_f_._Y_=_V2_._Z_)_)
let x be bound_QC-variable of Al; ::_thesis: ( ( x <> Y implies f . x = V1 . x ) & ( x = Y implies f . Y = V2 . Z ) )
now__::_thesis:_(_x_<>_Y_implies_f_._x_=_V1_._x_)
assume A3: x <> Y ; ::_thesis: f . x = V1 . x
( ( for x1 being bound_QC-variable of Al st x1 = x holds
x1 <> Y ) implies f . x = V1 . x ) by A2;
hence f . x = V1 . x by A3; ::_thesis: verum
end;
hence ( x <> Y implies f . x = V1 . x ) ; ::_thesis: ( x = Y implies f . Y = V2 . Z )
thus ( x = Y implies f . Y = V2 . Z ) by A2; ::_thesis: verum
end;
hence ( ( for x being bound_QC-variable of Al st x <> Y holds
f . x = V1 . x ) & f . Y = V2 . Z ) ; ::_thesis: verum
end;
end;
theorem :: VALUAT_1:26
for Al being QC-alphabet
for A being non empty set
for Y, Z being bound_QC-variable of Al
for V1, V2 being Element of Valuations_in (Al,A) ex v being Element of Valuations_in (Al,A) st
( ( for x being bound_QC-variable of Al st x <> Y holds
v . x = V1 . x ) & v . Y = V2 . Z ) by Lm3;
theorem Th27: :: VALUAT_1:27
for Al being QC-alphabet
for A being non empty set
for x being bound_QC-variable of Al
for p being Element of CQC-WFF Al
for J being interpretation of Al,A st not x in still_not-bound_in p holds
for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
(Valid (p,J)) . v = (Valid (p,J)) . w
proof
let Al be QC-alphabet ; ::_thesis: for A being non empty set
for x being bound_QC-variable of Al
for p being Element of CQC-WFF Al
for J being interpretation of Al,A st not x in still_not-bound_in p holds
for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
(Valid (p,J)) . v = (Valid (p,J)) . w
let A be non empty set ; ::_thesis: for x being bound_QC-variable of Al
for p being Element of CQC-WFF Al
for J being interpretation of Al,A st not x in still_not-bound_in p holds
for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
(Valid (p,J)) . v = (Valid (p,J)) . w
let x be bound_QC-variable of Al; ::_thesis: for p being Element of CQC-WFF Al
for J being interpretation of Al,A st not x in still_not-bound_in p holds
for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
(Valid (p,J)) . v = (Valid (p,J)) . w
let p be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A st not x in still_not-bound_in p holds
for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
(Valid (p,J)) . v = (Valid (p,J)) . w
let J be interpretation of Al,A; ::_thesis: ( not x in still_not-bound_in p implies for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
(Valid (p,J)) . v = (Valid (p,J)) . w )
defpred S1[ Element of CQC-WFF Al] means ( not x in still_not-bound_in $1 implies for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
(Valid ($1,J)) . v = (Valid ($1,J)) . w );
A1: now__::_thesis:_for_s,_t_being_Element_of_CQC-WFF_Al
for_y_being_bound_QC-variable_of_Al
for_k_being_Element_of_NAT_
for_ll_being_CQC-variable_list_of_k,Al
for_P_being_QC-pred_symbol_of_k,Al_holds_
(_S1[_VERUM_Al]_&_S1[P_!_ll]_&_(_S1[s]_implies_S1[_'not'_s]_)_&_(_S1[s]_&_S1[t]_implies_S1[s_'&'_t]_)_&_(_S1[s]_implies_S1[_All_(y,s)]_)_)
let s, t be Element of CQC-WFF Al; ::_thesis: for y being bound_QC-variable of Al
for k being Element of NAT
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( S1[ VERUM Al] & S1[P ! ll] & ( S1[s] implies S1[ 'not' s] ) & ( S1[s] & S1[t] implies S1[s '&' t] ) & ( S1[s] implies S1[ All (y,s)] ) )
let y be bound_QC-variable of Al; ::_thesis: for k being Element of NAT
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( S1[ VERUM Al] & S1[P ! ll] & ( S1[s] implies S1[ 'not' s] ) & ( S1[s] & S1[t] implies S1[s '&' t] ) & ( S1[s] implies S1[ All (y,s)] ) )
let k be Element of NAT ; ::_thesis: for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( S1[ VERUM Al] & S1[P ! ll] & ( S1[s] implies S1[ 'not' s] ) & ( S1[s] & S1[t] implies S1[s '&' t] ) & ( S1[s] implies S1[ All (y,s)] ) )
let ll be CQC-variable_list of k,Al; ::_thesis: for P being QC-pred_symbol of k,Al holds
( S1[ VERUM Al] & S1[P ! ll] & ( S1[s] implies S1[ 'not' s] ) & ( S1[s] & S1[t] implies S1[s '&' t] ) & ( S1[s] implies S1[ All (y,s)] ) )
let P be QC-pred_symbol of k,Al; ::_thesis: ( S1[ VERUM Al] & S1[P ! ll] & ( S1[s] implies S1[ 'not' s] ) & ( S1[s] & S1[t] implies S1[s '&' t] ) & ( S1[s] implies S1[ All (y,s)] ) )
thus S1[ VERUM Al] ::_thesis: ( S1[P ! ll] & ( S1[s] implies S1[ 'not' s] ) & ( S1[s] & S1[t] implies S1[s '&' t] ) & ( S1[s] implies S1[ All (y,s)] ) )
proof
assume not x in still_not-bound_in (VERUM Al) ; ::_thesis: for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
(Valid ((VERUM Al),J)) . v = (Valid ((VERUM Al),J)) . w
thus for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
(Valid ((VERUM Al),J)) . v = (Valid ((VERUM Al),J)) . w ::_thesis: verum
proof
let v, w be Element of Valuations_in (Al,A); ::_thesis: ( ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) implies (Valid ((VERUM Al),J)) . v = (Valid ((VERUM Al),J)) . w )
assume for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ; ::_thesis: (Valid ((VERUM Al),J)) . v = (Valid ((VERUM Al),J)) . w
(Valid ((VERUM Al),J)) . v = TRUE by Th5;
hence (Valid ((VERUM Al),J)) . v = (Valid ((VERUM Al),J)) . w by Th5; ::_thesis: verum
end;
end;
A2: rng ll c= bound_QC-variables Al by RELAT_1:def_19;
thus S1[P ! ll] ::_thesis: ( ( S1[s] implies S1[ 'not' s] ) & ( S1[s] & S1[t] implies S1[s '&' t] ) & ( S1[s] implies S1[ All (y,s)] ) )
proof
assume A3: not x in still_not-bound_in (P ! ll) ; ::_thesis: for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
(Valid ((P ! ll),J)) . v = (Valid ((P ! ll),J)) . w
thus for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
(Valid ((P ! ll),J)) . v = (Valid ((P ! ll),J)) . w ::_thesis: verum
proof
let v, w be Element of Valuations_in (Al,A); ::_thesis: ( ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) implies (Valid ((P ! ll),J)) . v = (Valid ((P ! ll),J)) . w )
assume A4: for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ; ::_thesis: (Valid ((P ! ll),J)) . v = (Valid ((P ! ll),J)) . w
A5: now__::_thesis:_(_(Valid_((P_!_ll),J))_._v_=_TRUE_implies_(Valid_((P_!_ll),J))_._v_=_(Valid_((P_!_ll),J))_._w_)
A6: len (v *' ll) = k by Def3;
A7: now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_len_(v_*'_ll)_holds_
(v_*'_ll)_._i_=_(w_*'_ll)_._i
let i be Nat; ::_thesis: ( 1 <= i & i <= len (v *' ll) implies (v *' ll) . i = (w *' ll) . i )
assume A8: ( 1 <= i & i <= len (v *' ll) ) ; ::_thesis: (v *' ll) . i = (w *' ll) . i
A9: len (v *' ll) = len ll by A6, CARD_1:def_7;
then i in dom ll by A8, FINSEQ_3:25;
then ll . i in rng ll by FUNCT_1:def_3;
then reconsider z = ll . i as bound_QC-variable of Al by A2;
A10: i in NAT by ORDINAL1:def_12;
ll . i <> x
proof
reconsider M = still_not-bound_in ll as set ;
not x in M by A3, QC_LANG3:5;
then not x in variables_in (ll,(bound_QC-variables Al)) by QC_LANG3:2;
then not x in { (ll . i2) where i2 is Element of NAT : ( 1 <= i2 & i2 <= len ll & ll . i2 in bound_QC-variables Al ) } by QC_LANG3:def_1;
hence ll . i <> x by A8, A10, A9; ::_thesis: verum
end;
then A11: w . z = v . z by A4;
(v *' ll) . i = v . (ll . i) by A6, A8, Def3;
hence (v *' ll) . i = (w *' ll) . i by A6, A8, A11, Def3; ::_thesis: verum
end;
assume A12: (Valid ((P ! ll),J)) . v = TRUE ; ::_thesis: (Valid ((P ! ll),J)) . v = (Valid ((P ! ll),J)) . w
then (ll 'in' (J . P)) . v = TRUE by Lm1;
then A13: v *' ll in J . P by Def4;
len (w *' ll) = k by Def3;
then w *' ll in J . P by A13, A6, A7, FINSEQ_1:14;
then (ll 'in' (J . P)) . w = TRUE by Def4;
hence (Valid ((P ! ll),J)) . v = (Valid ((P ! ll),J)) . w by A12, Lm1; ::_thesis: verum
end;
now__::_thesis:_(_(Valid_((P_!_ll),J))_._v_=_FALSE_implies_(Valid_((P_!_ll),J))_._v_=_(Valid_((P_!_ll),J))_._w_)
A14: len (v *' ll) = k by Def3;
A15: now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_len_(v_*'_ll)_holds_
(v_*'_ll)_._i_=_(w_*'_ll)_._i
let i be Nat; ::_thesis: ( 1 <= i & i <= len (v *' ll) implies (v *' ll) . i = (w *' ll) . i )
assume A16: ( 1 <= i & i <= len (v *' ll) ) ; ::_thesis: (v *' ll) . i = (w *' ll) . i
A17: len (v *' ll) = len ll by A14, CARD_1:def_7;
then i in dom ll by A16, FINSEQ_3:25;
then ll . i in rng ll by FUNCT_1:def_3;
then reconsider z = ll . i as bound_QC-variable of Al by A2;
ll . i <> x
proof
reconsider M = still_not-bound_in ll as set ;
not x in M by A3, QC_LANG3:5;
then not x in variables_in (ll,(bound_QC-variables Al)) by QC_LANG3:2;
then ( i in NAT & not x in { (ll . i2) where i2 is Element of NAT : ( 1 <= i2 & i2 <= len ll & ll . i2 in bound_QC-variables Al ) } ) by ORDINAL1:def_12, QC_LANG3:def_1;
hence ll . i <> x by A16, A17; ::_thesis: verum
end;
then A18: w . z = v . z by A4;
(v *' ll) . i = v . (ll . i) by A14, A16, Def3;
hence (v *' ll) . i = (w *' ll) . i by A14, A16, A18, Def3; ::_thesis: verum
end;
assume A19: (Valid ((P ! ll),J)) . v = FALSE ; ::_thesis: (Valid ((P ! ll),J)) . v = (Valid ((P ! ll),J)) . w
then (ll 'in' (J . P)) . v = FALSE by Lm1;
then A20: not v *' ll in J . P by Def4;
len (w *' ll) = k by Def3;
then not w *' ll in J . P by A20, A14, A15, FINSEQ_1:14;
then (ll 'in' (J . P)) . w = FALSE by Def4;
hence (Valid ((P ! ll),J)) . v = (Valid ((P ! ll),J)) . w by A19, Lm1; ::_thesis: verum
end;
hence (Valid ((P ! ll),J)) . v = (Valid ((P ! ll),J)) . w by A5, XBOOLEAN:def_3; ::_thesis: verum
end;
end;
thus ( S1[s] implies S1[ 'not' s] ) ::_thesis: ( ( S1[s] & S1[t] implies S1[s '&' t] ) & ( S1[s] implies S1[ All (y,s)] ) )
proof
assume A21: ( ( not x in still_not-bound_in s implies for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
(Valid (s,J)) . v = (Valid (s,J)) . w ) & not x in still_not-bound_in ('not' s) ) ; ::_thesis: for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
(Valid (('not' s),J)) . v = (Valid (('not' s),J)) . w
thus for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
(Valid (('not' s),J)) . v = (Valid (('not' s),J)) . w ::_thesis: verum
proof
let v, w be Element of Valuations_in (Al,A); ::_thesis: ( ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) implies (Valid (('not' s),J)) . v = (Valid (('not' s),J)) . w )
assume A22: for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ; ::_thesis: (Valid (('not' s),J)) . v = (Valid (('not' s),J)) . w
A23: now__::_thesis:_(_(Valid_(('not'_s),J))_._v_=_FALSE_implies_(Valid_(('not'_s),J))_._v_=_(Valid_(('not'_s),J))_._w_)
assume A24: (Valid (('not' s),J)) . v = FALSE ; ::_thesis: (Valid (('not' s),J)) . v = (Valid (('not' s),J)) . w
then 'not' ((Valid (s,J)) . v) = FALSE by Th10;
then (Valid (s,J)) . v = TRUE by MARGREL1:11;
then (Valid (s,J)) . w = TRUE by A21, A22, QC_LANG3:7;
then 'not' ((Valid (s,J)) . w) = FALSE by MARGREL1:11;
hence (Valid (('not' s),J)) . v = (Valid (('not' s),J)) . w by A24, Th10; ::_thesis: verum
end;
now__::_thesis:_(_(Valid_(('not'_s),J))_._v_=_TRUE_implies_(Valid_(('not'_s),J))_._v_=_(Valid_(('not'_s),J))_._w_)
assume A25: (Valid (('not' s),J)) . v = TRUE ; ::_thesis: (Valid (('not' s),J)) . v = (Valid (('not' s),J)) . w
then 'not' ((Valid (s,J)) . v) = TRUE by Th10;
then (Valid (s,J)) . v = FALSE by MARGREL1:11;
then (Valid (s,J)) . w = FALSE by A21, A22, QC_LANG3:7;
then 'not' ((Valid (s,J)) . w) = TRUE by MARGREL1:11;
hence (Valid (('not' s),J)) . v = (Valid (('not' s),J)) . w by A25, Th10; ::_thesis: verum
end;
hence (Valid (('not' s),J)) . v = (Valid (('not' s),J)) . w by A23, XBOOLEAN:def_3; ::_thesis: verum
end;
end;
thus ( S1[s] & S1[t] implies S1[s '&' t] ) ::_thesis: ( S1[s] implies S1[ All (y,s)] )
proof
assume that
A26: ( not x in still_not-bound_in s implies for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
(Valid (s,J)) . v = (Valid (s,J)) . w ) and
A27: ( not x in still_not-bound_in t implies for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
(Valid (t,J)) . v = (Valid (t,J)) . w ) and
A28: not x in still_not-bound_in (s '&' t) ; ::_thesis: for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
(Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w
A29: not x in (still_not-bound_in s) \/ (still_not-bound_in t) by A28, QC_LANG3:10;
thus for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
(Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w ::_thesis: verum
proof
let v, w be Element of Valuations_in (Al,A); ::_thesis: ( ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) implies (Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w )
assume A30: for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ; ::_thesis: (Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w
A31: now__::_thesis:_(_(Valid_((s_'&'_t),J))_._v_=_FALSE_implies_(Valid_((s_'&'_t),J))_._v_=_(Valid_((s_'&'_t),J))_._w_)
assume A32: (Valid ((s '&' t),J)) . v = FALSE ; ::_thesis: (Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w
A33: now__::_thesis:_(_(Valid_(s,J))_._v_=_FALSE_implies_(Valid_((s_'&'_t),J))_._v_=_(Valid_((s_'&'_t),J))_._w_)
assume (Valid (s,J)) . v = FALSE ; ::_thesis: (Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w
then (Valid (s,J)) . w = FALSE by A26, A29, A30, XBOOLE_0:def_3;
then ((Valid (s,J)) . w) '&' ((Valid (t,J)) . w) = FALSE by MARGREL1:12;
hence (Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w by A32, Th12; ::_thesis: verum
end;
A34: now__::_thesis:_(_(Valid_(t,J))_._v_=_FALSE_implies_(Valid_((s_'&'_t),J))_._v_=_(Valid_((s_'&'_t),J))_._w_)
assume (Valid (t,J)) . v = FALSE ; ::_thesis: (Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w
then (Valid (t,J)) . w = FALSE by A27, A29, A30, XBOOLE_0:def_3;
then ((Valid (s,J)) . w) '&' ((Valid (t,J)) . w) = FALSE by MARGREL1:12;
hence (Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w by A32, Th12; ::_thesis: verum
end;
((Valid (s,J)) . v) '&' ((Valid (t,J)) . v) = FALSE by A32, Th12;
hence (Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w by A33, A34, MARGREL1:12; ::_thesis: verum
end;
now__::_thesis:_(_(Valid_((s_'&'_t),J))_._v_=_TRUE_implies_(Valid_((s_'&'_t),J))_._v_=_(Valid_((s_'&'_t),J))_._w_)
assume A35: (Valid ((s '&' t),J)) . v = TRUE ; ::_thesis: (Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w
then A36: ((Valid (s,J)) . v) '&' ((Valid (t,J)) . v) = TRUE by Th12;
then (Valid (t,J)) . v = TRUE by MARGREL1:12;
then A37: (Valid (t,J)) . w = TRUE by A27, A29, A30, XBOOLE_0:def_3;
(Valid (s,J)) . v = TRUE by A36, MARGREL1:12;
then (Valid (s,J)) . w = TRUE by A26, A29, A30, XBOOLE_0:def_3;
then ((Valid (s,J)) . w) '&' ((Valid (t,J)) . w) = TRUE by A37;
hence (Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w by A35, Th12; ::_thesis: verum
end;
hence (Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w by A31, XBOOLEAN:def_3; ::_thesis: verum
end;
end;
thus ( S1[s] implies S1[ All (y,s)] ) ::_thesis: verum
proof
assume that
A38: ( not x in still_not-bound_in s implies for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al 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)) ; ::_thesis: for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
(Valid ((All (y,s)),J)) . v = (Valid ((All (y,s)),J)) . w
A40: not x in (still_not-bound_in s) \ {y} by A39, QC_LANG3:12;
thus for v, w being Element of Valuations_in (Al,A) st ( for z being bound_QC-variable of Al st x <> z holds
w . z = v . z ) holds
(Valid ((All (y,s)),J)) . v = (Valid ((All (y,s)),J)) . w ::_thesis: verum
proof
let v, w be Element of Valuations_in (Al,A); ::_thesis: ( ( for z being bound_QC-variable of Al st x <> z holds
w . z = v . z ) implies (Valid ((All (y,s)),J)) . v = (Valid ((All (y,s)),J)) . w )
assume A41: for z being bound_QC-variable of Al st x <> z holds
w . z = v . z ; ::_thesis: (Valid ((All (y,s)),J)) . v = (Valid ((All (y,s)),J)) . w
A42: now__::_thesis:_(_(Valid_((All_(y,s)),J))_._v_=_FALSE_implies_(Valid_((All_(y,s)),J))_._v_=_(Valid_((All_(y,s)),J))_._w_)
assume A43: (Valid ((All (y,s)),J)) . v = FALSE ; ::_thesis: (Valid ((All (y,s)),J)) . v = (Valid ((All (y,s)),J)) . w
then (FOR_ALL (y,(Valid (s,J)))) . v = FALSE by Lm1;
then consider v1 being Element of Valuations_in (Al,A) such that
A44: (Valid (s,J)) . v1 = FALSE and
A45: for z being bound_QC-variable of Al st y <> z holds
v1 . z = v . z by Th2;
A46: now__::_thesis:_(_not_x_in_still_not-bound_in_s_implies_ex_v2_being_Element_of_Valuations_in_(Al,A)_st_
(_(Valid_(s,J))_._v2_=_FALSE_&_(_for_z_being_bound_QC-variable_of_Al_st_y_<>_z_holds_
v2_._z_=_w_._z_)_)_)
assume A47: not x in still_not-bound_in s ; ::_thesis: ex v2 being Element of Valuations_in (Al,A) st
( (Valid (s,J)) . v2 = FALSE & ( for z being bound_QC-variable of Al st y <> z holds
v2 . z = w . z ) )
consider v2 being Element of Valuations_in (Al,A) such that
A48: ( ( for z being bound_QC-variable of Al st z <> y holds
v2 . z = w . z ) & v2 . y = v1 . y ) by Lm3;
take v2 = v2; ::_thesis: ( (Valid (s,J)) . v2 = FALSE & ( for z being bound_QC-variable of Al st y <> z holds
v2 . z = w . z ) )
for z being bound_QC-variable of Al st x <> z holds
v2 . z = v1 . z
proof
let z be bound_QC-variable of Al; ::_thesis: ( x <> z implies v2 . z = v1 . z )
assume A49: x <> z ; ::_thesis: v2 . z = v1 . z
now__::_thesis:_(_z_<>_y_implies_v2_._z_=_v1_._z_)
assume A50: z <> y ; ::_thesis: v2 . z = v1 . z
hence v2 . z = w . z by A48
.= v . z by A41, A49
.= v1 . z by A45, A50 ;
::_thesis: verum
end;
hence v2 . z = v1 . z by A48; ::_thesis: verum
end;
hence (Valid (s,J)) . v2 = FALSE by A38, A44, A47; ::_thesis: for z being bound_QC-variable of Al st y <> z holds
v2 . z = w . z
thus for z being bound_QC-variable of Al st y <> z holds
v2 . z = w . z by A48; ::_thesis: verum
end;
now__::_thesis:_(_x_in_{y}_implies_ex_v2_being_Element_of_Valuations_in_(Al,A)_st_
(_(Valid_(s,J))_._v2_=_FALSE_&_(_for_z_being_bound_QC-variable_of_Al_st_y_<>_z_holds_
v2_._z_=_w_._z_)_)_)
assume A51: x in {y} ; ::_thesis: ex v2 being Element of Valuations_in (Al,A) st
( (Valid (s,J)) . v2 = FALSE & ( for z being bound_QC-variable of Al st y <> z holds
v2 . z = w . z ) )
take v2 = v1; ::_thesis: ( (Valid (s,J)) . v2 = FALSE & ( for z being bound_QC-variable of Al st y <> z holds
v2 . z = w . z ) )
thus (Valid (s,J)) . v2 = FALSE by A44; ::_thesis: for z being bound_QC-variable of Al st y <> z holds
v2 . z = w . z
for z being bound_QC-variable of Al st y <> z holds
v1 . z = w . z
proof
let z be bound_QC-variable of Al; ::_thesis: ( y <> z implies v1 . z = w . z )
assume A52: y <> z ; ::_thesis: v1 . z = w . z
then A53: x <> z by A51, TARSKI:def_1;
thus v1 . z = v . z by A45, A52
.= w . z by A41, A53 ; ::_thesis: verum
end;
hence for z being bound_QC-variable of Al st y <> z holds
v2 . z = w . z ; ::_thesis: verum
end;
then (FOR_ALL (y,(Valid (s,J)))) . w = FALSE by A40, A46, Th2, XBOOLE_0:def_5;
hence (Valid ((All (y,s)),J)) . v = (Valid ((All (y,s)),J)) . w by A43, Lm1; ::_thesis: verum
end;
now__::_thesis:_(_(Valid_((All_(y,s)),J))_._v_=_TRUE_implies_(Valid_((All_(y,s)),J))_._v_=_(Valid_((All_(y,s)),J))_._w_)
assume A54: (Valid ((All (y,s)),J)) . v = TRUE ; ::_thesis: (Valid ((All (y,s)),J)) . v = (Valid ((All (y,s)),J)) . w
then A55: (FOR_ALL (y,(Valid (s,J)))) . v = TRUE by Lm1;
for v1 being Element of Valuations_in (Al,A) st ( for z being bound_QC-variable of Al st y <> z holds
v1 . z = w . z ) holds
(Valid (s,J)) . v1 = TRUE
proof
let v1 be Element of Valuations_in (Al,A); ::_thesis: ( ( for z being bound_QC-variable of Al st y <> z holds
v1 . z = w . z ) implies (Valid (s,J)) . v1 = TRUE )
assume A56: for z being bound_QC-variable of Al st y <> z holds
v1 . z = w . z ; ::_thesis: (Valid (s,J)) . v1 = TRUE
A57: now__::_thesis:_(_not_x_in_still_not-bound_in_s_implies_(Valid_(s,J))_._v1_=_TRUE_)
assume A58: not x in still_not-bound_in s ; ::_thesis: (Valid (s,J)) . v1 = TRUE
consider v2 being Element of Valuations_in (Al,A) such that
A59: ( ( for z being bound_QC-variable of Al st z <> y holds
v2 . z = v . z ) & v2 . y = v1 . y ) by Lm3;
A60: for z being bound_QC-variable of Al st x <> z holds
v2 . z = v1 . z
proof
let z be bound_QC-variable of Al; ::_thesis: ( x <> z implies v2 . z = v1 . z )
assume A61: x <> z ; ::_thesis: v2 . z = v1 . z
now__::_thesis:_(_z_<>_y_implies_v2_._z_=_v1_._z_)
assume A62: z <> y ; ::_thesis: v2 . z = v1 . z
hence v2 . z = v . z by A59
.= w . z by A41, A61
.= v1 . z by A56, A62 ;
::_thesis: verum
end;
hence v2 . z = v1 . z by A59; ::_thesis: verum
end;
(Valid (s,J)) . v2 = TRUE by A55, A59, Th3;
hence (Valid (s,J)) . v1 = TRUE by A38, A58, A60; ::_thesis: verum
end;
now__::_thesis:_(_x_in_{y}_implies_(Valid_(s,J))_._v1_=_TRUE_)
assume x in {y} ; ::_thesis: (Valid (s,J)) . v1 = TRUE
then A63: x = y by TARSKI:def_1;
for z being bound_QC-variable of Al st y <> z holds
v1 . z = v . z
proof
let z be bound_QC-variable of Al; ::_thesis: ( y <> z implies v1 . z = v . z )
assume A64: y <> z ; ::_thesis: v1 . z = v . z
hence v . z = w . z by A41, A63
.= v1 . z by A56, A64 ;
::_thesis: verum
end;
hence (Valid (s,J)) . v1 = TRUE by A55, Th3; ::_thesis: verum
end;
hence (Valid (s,J)) . v1 = TRUE by A40, A57, XBOOLE_0:def_5; ::_thesis: verum
end;
then (FOR_ALL (y,(Valid (s,J)))) . w = TRUE by Th3;
hence (Valid ((All (y,s)),J)) . v = (Valid ((All (y,s)),J)) . w by A54, Lm1; ::_thesis: verum
end;
hence (Valid ((All (y,s)),J)) . v = (Valid ((All (y,s)),J)) . w by A42, XBOOLEAN:def_3; ::_thesis: verum
end;
end;
end;
for s being Element of CQC-WFF Al holds S1[s] from CQC_LANG:sch_1(A1);
hence ( not x in still_not-bound_in p implies for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
(Valid (p,J)) . v = (Valid (p,J)) . w ) ; ::_thesis: verum
end;
theorem Th28: :: VALUAT_1:28
for Al being QC-alphabet
for A being non empty set
for x being bound_QC-variable of Al
for v being Element of Valuations_in (Al,A)
for p being Element of CQC-WFF Al
for J being interpretation of Al,A st J,v |= p & not x in still_not-bound_in p holds
for w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
J,w |= p
proof
let Al be QC-alphabet ; ::_thesis: for A being non empty set
for x being bound_QC-variable of Al
for v being Element of Valuations_in (Al,A)
for p being Element of CQC-WFF Al
for J being interpretation of Al,A st J,v |= p & not x in still_not-bound_in p holds
for w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
J,w |= p
let A be non empty set ; ::_thesis: for x being bound_QC-variable of Al
for v being Element of Valuations_in (Al,A)
for p being Element of CQC-WFF Al
for J being interpretation of Al,A st J,v |= p & not x in still_not-bound_in p holds
for w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
J,w |= p
let x be bound_QC-variable of Al; ::_thesis: for v being Element of Valuations_in (Al,A)
for p being Element of CQC-WFF Al
for J being interpretation of Al,A st J,v |= p & not x in still_not-bound_in p holds
for w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
J,w |= p
let v be Element of Valuations_in (Al,A); ::_thesis: for p being Element of CQC-WFF Al
for J being interpretation of Al,A st J,v |= p & not x in still_not-bound_in p holds
for w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
J,w |= p
let p be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A st J,v |= p & not x in still_not-bound_in p holds
for w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
J,w |= p
let J be interpretation of Al,A; ::_thesis: ( J,v |= p & not x in still_not-bound_in p implies for w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
J,w |= p )
assume that
A1: J,v |= p and
A2: not x in still_not-bound_in p ; ::_thesis: for w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
J,w |= p
now__::_thesis:_for_w_being_Element_of_Valuations_in_(Al,A)_st_(_for_y_being_bound_QC-variable_of_Al_st_x_<>_y_holds_
w_._y_=_v_._y_)_holds_
J,w_|=_p
let w be Element of Valuations_in (Al,A); ::_thesis: ( ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) implies J,w |= p )
assume A3: for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ; ::_thesis: J,w |= p
(Valid (p,J)) . v = TRUE by A1, Def7;
then (Valid (p,J)) . w = TRUE by A2, A3, Th27;
hence J,w |= p by Def7; ::_thesis: verum
end;
hence for w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
J,w |= p ; ::_thesis: verum
end;
theorem Th29: :: VALUAT_1:29
for Al being QC-alphabet
for A being non empty set
for x being bound_QC-variable of Al
for v being Element of Valuations_in (Al,A)
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds
( J,v |= All (x,p) iff for w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
J,w |= p )
proof
let Al be QC-alphabet ; ::_thesis: for A being non empty set
for x being bound_QC-variable of Al
for v being Element of Valuations_in (Al,A)
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds
( J,v |= All (x,p) iff for w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
J,w |= p )
let A be non empty set ; ::_thesis: for x being bound_QC-variable of Al
for v being Element of Valuations_in (Al,A)
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds
( J,v |= All (x,p) iff for w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
J,w |= p )
let x be bound_QC-variable of Al; ::_thesis: for v being Element of Valuations_in (Al,A)
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds
( J,v |= All (x,p) iff for w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
J,w |= p )
let v be Element of Valuations_in (Al,A); ::_thesis: for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds
( J,v |= All (x,p) iff for w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
J,w |= p )
let p be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A holds
( J,v |= All (x,p) iff for w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
J,w |= p )
let J be interpretation of Al,A; ::_thesis: ( J,v |= All (x,p) iff for w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
J,w |= p )
A1: now__::_thesis:_(_(_for_w_being_Element_of_Valuations_in_(Al,A)_st_(_for_y_being_bound_QC-variable_of_Al_st_x_<>_y_holds_
w_._y_=_v_._y_)_holds_
J,w_|=_p_)_implies_J,v_|=_All_(x,p)_)
assume A2: for w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
J,w |= p ; ::_thesis: J,v |= All (x,p)
for w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
(Valid (p,J)) . w = TRUE
proof
let w be Element of Valuations_in (Al,A); ::_thesis: ( ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) implies (Valid (p,J)) . w = TRUE )
assume for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ; ::_thesis: (Valid (p,J)) . w = TRUE
then J,w |= p by A2;
hence (Valid (p,J)) . w = TRUE by Def7; ::_thesis: verum
end;
hence J,v |= All (x,p) by Th20; ::_thesis: verum
end;
now__::_thesis:_(_J,v_|=_All_(x,p)_implies_for_w_being_Element_of_Valuations_in_(Al,A)_st_(_for_y_being_bound_QC-variable_of_Al_st_x_<>_y_holds_
w_._y_=_v_._y_)_holds_
J,w_|=_p_)
assume A3: J,v |= All (x,p) ; ::_thesis: for w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
J,w |= p
let w be Element of Valuations_in (Al,A); ::_thesis: ( ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) implies J,w |= p )
assume for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ; ::_thesis: J,w |= p
then (Valid (p,J)) . w = TRUE by A3, Th20;
hence J,w |= p by Def7; ::_thesis: verum
end;
hence ( J,v |= All (x,p) iff for w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
J,w |= p ) by A1; ::_thesis: verum
end;
theorem Th30: :: VALUAT_1:30
for Al being QC-alphabet
for A being non empty set
for x, y being bound_QC-variable of Al
for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A
for s9 being QC-formula of Al st x <> y & p = s9 . x & q = s9 . y holds
for v being Element of Valuations_in (Al,A) st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v
proof
let Al be QC-alphabet ; ::_thesis: for A being non empty set
for x, y being bound_QC-variable of Al
for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A
for s9 being QC-formula of Al st x <> y & p = s9 . x & q = s9 . y holds
for v being Element of Valuations_in (Al,A) st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v
let A be non empty set ; ::_thesis: for x, y being bound_QC-variable of Al
for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A
for s9 being QC-formula of Al st x <> y & p = s9 . x & q = s9 . y holds
for v being Element of Valuations_in (Al,A) st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v
let x, y be bound_QC-variable of Al; ::_thesis: for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A
for s9 being QC-formula of Al st x <> y & p = s9 . x & q = s9 . y holds
for v being Element of Valuations_in (Al,A) st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v
let p, q be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A
for s9 being QC-formula of Al st x <> y & p = s9 . x & q = s9 . y holds
for v being Element of Valuations_in (Al,A) st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v
let J be interpretation of Al,A; ::_thesis: for s9 being QC-formula of Al st x <> y & p = s9 . x & q = s9 . y holds
for v being Element of Valuations_in (Al,A) st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v
let s9 be QC-formula of Al; ::_thesis: ( x <> y & p = s9 . x & q = s9 . y implies for v being Element of Valuations_in (Al,A) st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v )
defpred S1[ Element of QC-WFF Al] means for x, y being bound_QC-variable of Al
for p, q being Element of CQC-WFF Al st x <> y & p = $1 . x & q = $1 . y holds
for v being Element of Valuations_in (Al,A) st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v;
A1: now__::_thesis:_for_s_being_Element_of_QC-WFF_Al_holds_
(_(_s_is_atomic_implies_S1[s]_)_&_S1[_VERUM_Al]_&_(_s_is_negative_&_S1[_the_argument_of_s]_implies_S1[s]_)_&_(_s_is_conjunctive_&_S1[_the_left_argument_of_s]_&_S1[_the_right_argument_of_s]_implies_S1[s]_)_&_(_s_is_universal_&_S1[_the_scope_of_s]_implies_S1[s]_)_)
let s be Element of QC-WFF Al; ::_thesis: ( ( s is atomic implies S1[s] ) & S1[ VERUM Al] & ( s is negative & S1[ the_argument_of s] implies S1[s] ) & ( s is conjunctive & S1[ the_left_argument_of s] & S1[ the_right_argument_of s] implies S1[s] ) & ( s is universal & S1[ the_scope_of s] implies S1[s] ) )
thus ( s is atomic implies S1[s] ) ::_thesis: ( S1[ VERUM Al] & ( s is negative & S1[ the_argument_of s] implies S1[s] ) & ( s is conjunctive & S1[ the_left_argument_of s] & S1[ the_right_argument_of s] implies S1[s] ) & ( s is universal & S1[ the_scope_of s] implies S1[s] ) )
proof
assume A2: s is atomic ; ::_thesis: S1[s]
thus for x, y being bound_QC-variable of Al
for p, q being Element of CQC-WFF Al st x <> y & p = s . x & q = s . y holds
for v being Element of Valuations_in (Al,A) st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v ::_thesis: verum
proof
consider k being Element of NAT , P being QC-pred_symbol of k,Al, l being QC-variable_list of k,Al such that
A3: s = P ! l by A2, QC_LANG1:def_18;
let x, y be bound_QC-variable of Al; ::_thesis: for p, q being Element of CQC-WFF Al st x <> y & p = s . x & q = s . y holds
for v being Element of Valuations_in (Al,A) st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v
let p, q be Element of CQC-WFF Al; ::_thesis: ( x <> y & p = s . x & q = s . y implies for v being Element of Valuations_in (Al,A) st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v )
assume that
x <> y and
A4: p = s . x and
A5: q = s . y ; ::_thesis: for v being Element of Valuations_in (Al,A) st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v
set lx = Subst (l,((Al a. 0) .--> x));
set ly = Subst (l,((Al a. 0) .--> y));
let v be Element of Valuations_in (Al,A); ::_thesis: ( v . x = v . y implies (Valid (p,J)) . v = (Valid (q,J)) . v )
assume A6: v . x = v . y ; ::_thesis: (Valid (p,J)) . v = (Valid (q,J)) . v
A7: p = P ! (Subst (l,((Al a. 0) .--> x))) by A4, A3, CQC_LANG:17;
then A8: { ((Subst (l,((Al a. 0) .--> x))) . i) where i is Element of NAT : ( 1 <= i & i <= len (Subst (l,((Al a. 0) .--> x))) & (Subst (l,((Al a. 0) .--> x))) . i in free_QC-variables Al ) } = {} by CQC_LANG:7;
A9: q = P ! (Subst (l,((Al a. 0) .--> y))) by A5, A3, CQC_LANG:17;
then A10: { ((Subst (l,((Al a. 0) .--> y))) . i) where i is Element of NAT : ( 1 <= i & i <= len (Subst (l,((Al a. 0) .--> y))) & (Subst (l,((Al a. 0) .--> y))) . i in free_QC-variables Al ) } = {} by CQC_LANG:7;
A11: { ((Subst (l,((Al a. 0) .--> y))) . j) where j is Element of NAT : ( 1 <= j & j <= len (Subst (l,((Al a. 0) .--> y))) & (Subst (l,((Al a. 0) .--> y))) . j in fixed_QC-variables Al ) } = {} by A9, CQC_LANG:7;
{ ((Subst (l,((Al a. 0) .--> x))) . j) where j is Element of NAT : ( 1 <= j & j <= len (Subst (l,((Al a. 0) .--> x))) & (Subst (l,((Al a. 0) .--> x))) . j in fixed_QC-variables Al ) } = {} by A7, CQC_LANG:7;
then reconsider lx = Subst (l,((Al a. 0) .--> x)), ly = Subst (l,((Al a. 0) .--> y)) as CQC-variable_list of k,Al by A8, A10, A11, CQC_LANG:5;
A12: len (v *' lx) = k by Def3;
A13: now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_len_(v_*'_lx)_holds_
(v_*'_lx)_._i_=_(v_*'_ly)_._i
let i be Nat; ::_thesis: ( 1 <= i & i <= len (v *' lx) implies (v *' lx) . i = (v *' ly) . i )
assume that
A14: 1 <= i and
A15: i <= len (v *' lx) ; ::_thesis: (v *' lx) . i = (v *' ly) . i
A16: i in NAT by ORDINAL1:def_12;
A17: i <= len l by A12, A15, CARD_1:def_7;
A18: now__::_thesis:_(_l_._i_<>_Al_a._0_implies_(v_*'_lx)_._i_=_(v_*'_ly)_._i_)
assume l . i <> Al a. 0 ; ::_thesis: (v *' lx) . i = (v *' ly) . i
then A19: ( lx . i = l . i & ly . i = l . i ) by A14, A17, A16, CQC_LANG:3;
v . (lx . i) = (v *' lx) . i by A12, A14, A15, Def3;
hence (v *' lx) . i = (v *' ly) . i by A12, A14, A15, A19, Def3; ::_thesis: verum
end;
now__::_thesis:_(_l_._i_=_Al_a._0_implies_(v_*'_lx)_._i_=_(v_*'_ly)_._i_)
assume l . i = Al a. 0 ; ::_thesis: (v *' lx) . i = (v *' ly) . i
then A20: ( lx . i = x & ly . i = y ) by A14, A17, A16, CQC_LANG:3;
v . (lx . i) = (v *' lx) . i by A12, A14, A15, Def3;
hence (v *' lx) . i = (v *' ly) . i by A6, A12, A14, A15, A20, Def3; ::_thesis: verum
end;
hence (v *' lx) . i = (v *' ly) . i by A18; ::_thesis: verum
end;
len (v *' ly) = k by Def3;
then A21: v *' lx = v *' ly by A12, A13, FINSEQ_1:14;
A22: now__::_thesis:_(_(Valid_(p,J))_._v_=_FALSE_implies_(Valid_(q,J))_._v_=_FALSE_)
assume (Valid (p,J)) . v = FALSE ; ::_thesis: (Valid (q,J)) . v = FALSE
then not v *' lx in J . P by A7, Th8;
hence (Valid (q,J)) . v = FALSE by A9, A21, Th8; ::_thesis: verum
end;
now__::_thesis:_(_(Valid_(p,J))_._v_=_TRUE_implies_(Valid_(q,J))_._v_=_TRUE_)
assume (Valid (p,J)) . v = TRUE ; ::_thesis: (Valid (q,J)) . v = TRUE
then v *' lx in J . P by A7, Th7;
hence (Valid (q,J)) . v = TRUE by A9, A21, Th7; ::_thesis: verum
end;
hence (Valid (p,J)) . v = (Valid (q,J)) . v by A22, XBOOLEAN:def_3; ::_thesis: verum
end;
end;
thus S1[ VERUM Al] ::_thesis: ( ( s is negative & S1[ the_argument_of s] implies S1[s] ) & ( s is conjunctive & S1[ the_left_argument_of s] & S1[ the_right_argument_of s] implies S1[s] ) & ( s is universal & S1[ the_scope_of s] implies S1[s] ) )
proof
let x, y be bound_QC-variable of Al; ::_thesis: for p, q being Element of CQC-WFF Al st x <> y & p = (VERUM Al) . x & q = (VERUM Al) . y holds
for v being Element of Valuations_in (Al,A) st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v
let p, q be Element of CQC-WFF Al; ::_thesis: ( x <> y & p = (VERUM Al) . x & q = (VERUM Al) . y implies for v being Element of Valuations_in (Al,A) st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v )
assume that
x <> y and
A23: p = (VERUM Al) . x and
A24: q = (VERUM Al) . y ; ::_thesis: for v being Element of Valuations_in (Al,A) st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v
let v be Element of Valuations_in (Al,A); ::_thesis: ( v . x = v . y implies (Valid (p,J)) . v = (Valid (q,J)) . v )
assume v . x = v . y ; ::_thesis: (Valid (p,J)) . v = (Valid (q,J)) . v
p = VERUM Al by A23, CQC_LANG:15;
hence (Valid (p,J)) . v = (Valid (q,J)) . v by A24, CQC_LANG:15; ::_thesis: verum
end;
thus ( s is negative & S1[ the_argument_of s] implies S1[s] ) ::_thesis: ( ( s is conjunctive & S1[ the_left_argument_of s] & S1[ the_right_argument_of s] implies S1[s] ) & ( s is universal & S1[ the_scope_of s] implies S1[s] ) )
proof
assume that
A25: s is negative and
A26: for x, y being bound_QC-variable of Al
for p, q being Element of CQC-WFF Al st x <> y & p = (the_argument_of s) . x & q = (the_argument_of s) . y holds
for v being Element of Valuations_in (Al,A) st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v ; ::_thesis: S1[s]
thus for x, y being bound_QC-variable of Al
for p, q being Element of CQC-WFF Al st x <> y & p = s . x & q = s . y holds
for v being Element of Valuations_in (Al,A) st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v ::_thesis: verum
proof
let x, y be bound_QC-variable of Al; ::_thesis: for p, q being Element of CQC-WFF Al st x <> y & p = s . x & q = s . y holds
for v being Element of Valuations_in (Al,A) st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v
let p, q be Element of CQC-WFF Al; ::_thesis: ( x <> y & p = s . x & q = s . y implies for v being Element of Valuations_in (Al,A) st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v )
assume that
x <> y and
A27: p = s . x and
A28: q = s . y ; ::_thesis: for v being Element of Valuations_in (Al,A) st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v
A29: s . y = 'not' ((the_argument_of s) . y) by A25, CQC_LANG:18;
then reconsider qa = (the_argument_of s) . y as Element of CQC-WFF Al by A28, CQC_LANG:8;
A30: s . x = 'not' ((the_argument_of s) . x) by A25, CQC_LANG:18;
then reconsider pa = (the_argument_of s) . x as Element of CQC-WFF Al by A27, CQC_LANG:8;
let v be Element of Valuations_in (Al,A); ::_thesis: ( v . x = v . y implies (Valid (p,J)) . v = (Valid (q,J)) . v )
assume A31: v . x = v . y ; ::_thesis: (Valid (p,J)) . v = (Valid (q,J)) . v
A32: now__::_thesis:_(_(Valid_(p,J))_._v_=_FALSE_implies_(Valid_(q,J))_._v_=_FALSE_)
assume (Valid (p,J)) . v = FALSE ; ::_thesis: (Valid (q,J)) . v = FALSE
then 'not' ((Valid (pa,J)) . v) = FALSE by A27, A30, Th10;
then (Valid (pa,J)) . v = TRUE by MARGREL1:11;
then (Valid (qa,J)) . v = TRUE by A26, A31;
then 'not' ((Valid (qa,J)) . v) = FALSE by MARGREL1:11;
hence (Valid (q,J)) . v = FALSE by A28, A29, Th10; ::_thesis: verum
end;
now__::_thesis:_(_(Valid_(p,J))_._v_=_TRUE_implies_(Valid_(q,J))_._v_=_TRUE_)
assume (Valid (p,J)) . v = TRUE ; ::_thesis: (Valid (q,J)) . v = TRUE
then 'not' ((Valid (pa,J)) . v) = TRUE by A27, A30, Th10;
then (Valid (pa,J)) . v = FALSE by MARGREL1:11;
then (Valid (qa,J)) . v = FALSE by A26, A31;
then 'not' ((Valid (qa,J)) . v) = TRUE by MARGREL1:11;
hence (Valid (q,J)) . v = TRUE by A28, A29, Th10; ::_thesis: verum
end;
hence (Valid (p,J)) . v = (Valid (q,J)) . v by A32, XBOOLEAN:def_3; ::_thesis: verum
end;
end;
thus ( s is conjunctive & S1[ the_left_argument_of s] & S1[ the_right_argument_of s] implies S1[s] ) ::_thesis: ( s is universal & S1[ the_scope_of s] implies S1[s] )
proof
assume that
A33: s is conjunctive and
A34: for x, y being bound_QC-variable of Al
for p, q being Element of CQC-WFF Al st x <> y & p = (the_left_argument_of s) . x & q = (the_left_argument_of s) . y holds
for v being Element of Valuations_in (Al,A) st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v and
A35: for x, y being bound_QC-variable of Al
for p, q being Element of CQC-WFF Al st x <> y & p = (the_right_argument_of s) . x & q = (the_right_argument_of s) . y holds
for v being Element of Valuations_in (Al,A) st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v ; ::_thesis: S1[s]
thus for x, y being bound_QC-variable of Al
for p, q being Element of CQC-WFF Al st x <> y & p = s . x & q = s . y holds
for v being Element of Valuations_in (Al,A) st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v ::_thesis: verum
proof
let x, y be bound_QC-variable of Al; ::_thesis: for p, q being Element of CQC-WFF Al st x <> y & p = s . x & q = s . y holds
for v being Element of Valuations_in (Al,A) st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v
let p, q be Element of CQC-WFF Al; ::_thesis: ( x <> y & p = s . x & q = s . y implies for v being Element of Valuations_in (Al,A) st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v )
assume that
x <> y and
A36: p = s . x and
A37: q = s . y ; ::_thesis: for v being Element of Valuations_in (Al,A) st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v
A38: s . x = ((the_left_argument_of s) . x) '&' ((the_right_argument_of s) . x) by A33, CQC_LANG:20;
then reconsider pla = (the_left_argument_of s) . x, pra = (the_right_argument_of s) . x as Element of CQC-WFF Al by A36, CQC_LANG:9;
A39: s . y = ((the_left_argument_of s) . y) '&' ((the_right_argument_of s) . y) by A33, CQC_LANG:20;
then reconsider qla = (the_left_argument_of s) . y, qra = (the_right_argument_of s) . y as Element of CQC-WFF Al by A37, CQC_LANG:9;
let v be Element of Valuations_in (Al,A); ::_thesis: ( v . x = v . y implies (Valid (p,J)) . v = (Valid (q,J)) . v )
assume A40: v . x = v . y ; ::_thesis: (Valid (p,J)) . v = (Valid (q,J)) . v
A41: now__::_thesis:_(_(Valid_(p,J))_._v_=_FALSE_implies_(Valid_(p,J))_._v_=_(Valid_(q,J))_._v_)
assume A42: (Valid (p,J)) . v = FALSE ; ::_thesis: (Valid (p,J)) . v = (Valid (q,J)) . v
A43: now__::_thesis:_(_(Valid_(pla,J))_._v_=_FALSE_implies_(Valid_(p,J))_._v_=_(Valid_(q,J))_._v_)
assume (Valid (pla,J)) . v = FALSE ; ::_thesis: (Valid (p,J)) . v = (Valid (q,J)) . v
then (Valid (qla,J)) . v = FALSE by A34, A40;
then ((Valid (qla,J)) . v) '&' ((Valid (qra,J)) . v) = FALSE by MARGREL1:12;
hence (Valid (p,J)) . v = (Valid (q,J)) . v by A37, A39, A42, Th12; ::_thesis: verum
end;
A44: now__::_thesis:_(_(Valid_(pra,J))_._v_=_FALSE_implies_(Valid_(p,J))_._v_=_(Valid_(q,J))_._v_)
assume (Valid (pra,J)) . v = FALSE ; ::_thesis: (Valid (p,J)) . v = (Valid (q,J)) . v
then (Valid (qra,J)) . v = FALSE by A35, A40;
then ((Valid (qla,J)) . v) '&' ((Valid (qra,J)) . v) = FALSE by MARGREL1:12;
hence (Valid (p,J)) . v = (Valid (q,J)) . v by A37, A39, A42, Th12; ::_thesis: verum
end;
((Valid (pla,J)) . v) '&' ((Valid (pra,J)) . v) = FALSE by A36, A38, A42, Th12;
hence (Valid (p,J)) . v = (Valid (q,J)) . v by A43, A44, MARGREL1:12; ::_thesis: verum
end;
now__::_thesis:_(_(Valid_(p,J))_._v_=_TRUE_implies_(Valid_(q,J))_._v_=_TRUE_)
assume (Valid (p,J)) . v = TRUE ; ::_thesis: (Valid (q,J)) . v = TRUE
then A45: ((Valid (pla,J)) . v) '&' ((Valid (pra,J)) . v) = TRUE by A36, A38, Th12;
then (Valid (pra,J)) . v = TRUE by MARGREL1:12;
then A46: (Valid (qra,J)) . v = TRUE by A35, A40;
(Valid (pla,J)) . v = TRUE by A45, MARGREL1:12;
then (Valid (qla,J)) . v = TRUE by A34, A40;
then ((Valid (qla,J)) . v) '&' ((Valid (qra,J)) . v) = TRUE by A46;
hence (Valid (q,J)) . v = TRUE by A37, A39, Th12; ::_thesis: verum
end;
hence (Valid (p,J)) . v = (Valid (q,J)) . v by A41, XBOOLEAN:def_3; ::_thesis: verum
end;
end;
thus ( s is universal & S1[ the_scope_of s] implies S1[s] ) ::_thesis: verum
proof
assume that
A47: s is universal and
A48: for x, y being bound_QC-variable of Al
for p, q being Element of CQC-WFF Al st x <> y & p = (the_scope_of s) . x & q = (the_scope_of s) . y holds
for v being Element of Valuations_in (Al,A) st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v ; ::_thesis: S1[s]
consider xx being bound_QC-variable of Al, pp being Element of QC-WFF Al such that
A49: s = All (xx,pp) by A47, QC_LANG1:def_21;
A50: xx = bound_in s by A47, A49, QC_LANG1:def_27;
thus for x, y being bound_QC-variable of Al
for p, q being Element of CQC-WFF Al st x <> y & p = s . x & q = s . y holds
for v being Element of Valuations_in (Al,A) st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v ::_thesis: verum
proof
let x, y be bound_QC-variable of Al; ::_thesis: for p, q being Element of CQC-WFF Al st x <> y & p = s . x & q = s . y holds
for v being Element of Valuations_in (Al,A) st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v
let p, q be Element of CQC-WFF Al; ::_thesis: ( x <> y & p = s . x & q = s . y implies for v being Element of Valuations_in (Al,A) st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v )
assume that
x <> y and
A51: p = s . x and
A52: q = s . y ; ::_thesis: for v being Element of Valuations_in (Al,A) st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v
let v be Element of Valuations_in (Al,A); ::_thesis: ( v . x = v . y implies (Valid (p,J)) . v = (Valid (q,J)) . v )
assume A53: v . x = v . y ; ::_thesis: (Valid (p,J)) . v = (Valid (q,J)) . v
A54: now__::_thesis:_(_x_<>_bound_in_s_implies_(Valid_(p,J))_._v_=_(Valid_(q,J))_._v_)
assume A55: x <> bound_in s ; ::_thesis: (Valid (p,J)) . v = (Valid (q,J)) . v
then s . x = All ((bound_in s),((the_scope_of s) . x)) by A47, CQC_LANG:23;
then reconsider ps = (the_scope_of s) . x as Element of CQC-WFF Al by A51, CQC_LANG:13;
A56: All ((bound_in s),ps) = p by A47, A51, A55, CQC_LANG:23;
A57: now__::_thesis:_(_y_<>_bound_in_s_implies_(Valid_(p,J))_._v_=_(Valid_(q,J))_._v_)
assume A58: y <> bound_in s ; ::_thesis: (Valid (p,J)) . v = (Valid (q,J)) . v
then s . y = All ((bound_in s),((the_scope_of s) . y)) by A47, CQC_LANG:23;
then reconsider qs = (the_scope_of s) . y as Element of CQC-WFF Al by A52, CQC_LANG:13;
A59: Valid ((All ((bound_in s),qs)),J) = FOR_ALL ((bound_in s),(Valid (qs,J))) by Lm1;
A60: Valid ((All ((bound_in s),ps)),J) = FOR_ALL ((bound_in s),(Valid (ps,J))) by Lm1;
A61: All ((bound_in s),qs) = q by A47, A52, A58, CQC_LANG:23;
A62: now__::_thesis:_(_(Valid_(p,J))_._v_=_TRUE_implies_(Valid_(q,J))_._v_=_TRUE_)
assume A63: (Valid (p,J)) . v = TRUE ; ::_thesis: (Valid (q,J)) . v = TRUE
for v1 being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st bound_in s <> y holds
v1 . y = v . y ) holds
(Valid (qs,J)) . v1 = TRUE
proof
let v1 be Element of Valuations_in (Al,A); ::_thesis: ( ( for y being bound_QC-variable of Al st bound_in s <> y holds
v1 . y = v . y ) implies (Valid (qs,J)) . v1 = TRUE )
assume A64: for y being bound_QC-variable of Al st bound_in s <> y holds
v1 . y = v . y ; ::_thesis: (Valid (qs,J)) . v1 = TRUE
then A65: ( v1 . x = v . x & v1 . y = v . y ) by A55, A58;
(Valid (ps,J)) . v1 = TRUE by A56, A60, A63, A64, Th3;
hence (Valid (qs,J)) . v1 = TRUE by A48, A53, A65; ::_thesis: verum
end;
hence (Valid (q,J)) . v = TRUE by A61, A59, Th3; ::_thesis: verum
end;
now__::_thesis:_(_(Valid_(p,J))_._v_=_FALSE_implies_(Valid_(q,J))_._v_=_FALSE_)
assume A66: (Valid (p,J)) . v = FALSE ; ::_thesis: (Valid (q,J)) . v = FALSE
ex v1 being Element of Valuations_in (Al,A) st
( (Valid (qs,J)) . v1 = FALSE & ( for y being bound_QC-variable of Al st bound_in s <> y holds
v1 . y = v . y ) )
proof
consider v1 being Element of Valuations_in (Al,A) such that
A67: (Valid (ps,J)) . v1 = FALSE and
A68: for y being bound_QC-variable of Al st bound_in s <> y holds
v1 . y = v . y by A56, A60, A66, Th2;
( v1 . x = v . x & v1 . y = v . y ) by A55, A58, A68;
then (Valid (qs,J)) . v1 = FALSE by A48, A53, A67;
hence ex v1 being Element of Valuations_in (Al,A) st
( (Valid (qs,J)) . v1 = FALSE & ( for y being bound_QC-variable of Al st bound_in s <> y holds
v1 . y = v . y ) ) by A68; ::_thesis: verum
end;
hence (Valid (q,J)) . v = FALSE by A61, A59, Th2; ::_thesis: verum
end;
hence (Valid (p,J)) . v = (Valid (q,J)) . v by A62, XBOOLEAN:def_3; ::_thesis: verum
end;
now__::_thesis:_(_y_=_bound_in_s_implies_(Valid_(p,J))_._v_=_(Valid_(q,J))_._v_)
assume A69: y = bound_in s ; ::_thesis: (Valid (p,J)) . v = (Valid (q,J)) . v
then q = All (y,pp) by A49, A50, A52, CQC_LANG:24;
hence (Valid (p,J)) . v = (Valid (q,J)) . v by A49, A50, A51, A69, CQC_LANG:27; ::_thesis: verum
end;
hence (Valid (p,J)) . v = (Valid (q,J)) . v by A57; ::_thesis: verum
end;
now__::_thesis:_(_x_=_bound_in_s_implies_(Valid_(p,J))_._v_=_(Valid_(q,J))_._v_)
assume A70: x = bound_in s ; ::_thesis: (Valid (p,J)) . v = (Valid (q,J)) . v
then p = All (x,pp) by A49, A50, A51, CQC_LANG:24;
hence (Valid (p,J)) . v = (Valid (q,J)) . v by A49, A50, A52, A70, CQC_LANG:27; ::_thesis: verum
end;
hence (Valid (p,J)) . v = (Valid (q,J)) . v by A54; ::_thesis: verum
end;
end;
end;
for s being Element of QC-WFF Al holds S1[s] from QC_LANG1:sch_2(A1);
hence ( x <> y & p = s9 . x & q = s9 . y implies for v being Element of Valuations_in (Al,A) st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v ) ; ::_thesis: verum
end;
theorem Th31: :: VALUAT_1:31
for Al being QC-alphabet
for x, y being bound_QC-variable of Al
for s9 being QC-formula of Al st x <> y & not x in still_not-bound_in s9 holds
not x in still_not-bound_in (s9 . y)
proof
let Al be QC-alphabet ; ::_thesis: for x, y being bound_QC-variable of Al
for s9 being QC-formula of Al st x <> y & not x in still_not-bound_in s9 holds
not x in still_not-bound_in (s9 . y)
let x, y be bound_QC-variable of Al; ::_thesis: for s9 being QC-formula of Al st x <> y & not x in still_not-bound_in s9 holds
not x in still_not-bound_in (s9 . y)
let s9 be QC-formula of Al; ::_thesis: ( x <> y & not x in still_not-bound_in s9 implies not x in still_not-bound_in (s9 . y) )
defpred S1[ Element of QC-WFF Al] means ( x <> y & not x in still_not-bound_in $1 implies not x in still_not-bound_in ($1 . y) );
A1: now__::_thesis:_for_s_being_Element_of_QC-WFF_Al_holds_
(_(_s_is_atomic_implies_S1[s]_)_&_S1[_VERUM_Al]_&_(_s_is_negative_&_S1[_the_argument_of_s]_implies_S1[s]_)_&_(_s_is_conjunctive_&_S1[_the_left_argument_of_s]_&_S1[_the_right_argument_of_s]_implies_S1[s]_)_&_(_s_is_universal_&_S1[_the_scope_of_s]_implies_S1[s]_)_)
let s be Element of QC-WFF Al; ::_thesis: ( ( s is atomic implies S1[s] ) & S1[ VERUM Al] & ( s is negative & S1[ the_argument_of s] implies S1[s] ) & ( s is conjunctive & S1[ the_left_argument_of s] & S1[ the_right_argument_of s] implies S1[s] ) & ( s is universal & S1[ the_scope_of s] implies S1[s] ) )
thus ( s is atomic implies S1[s] ) ::_thesis: ( S1[ VERUM Al] & ( s is negative & S1[ the_argument_of s] implies S1[s] ) & ( s is conjunctive & S1[ the_left_argument_of s] & S1[ the_right_argument_of s] implies S1[s] ) & ( s is universal & S1[ the_scope_of s] implies S1[s] ) )
proof
assume that
A2: s is atomic and
A3: x <> y and
A4: not x in still_not-bound_in s ; ::_thesis: not x in still_not-bound_in (s . y)
thus not x in still_not-bound_in (s . y) ::_thesis: verum
proof
set l = the_arguments_of s;
set ll = Subst ((the_arguments_of s),((Al a. 0) .--> y));
A5: still_not-bound_in s = still_not-bound_in (the_arguments_of s) by A2, QC_LANG3:4
.= variables_in ((the_arguments_of s),(bound_QC-variables Al)) by QC_LANG3:2
.= { ((the_arguments_of s) . k) where k is Element of NAT : ( 1 <= k & k <= len (the_arguments_of s) & (the_arguments_of s) . k in bound_QC-variables Al ) } by QC_LANG3:def_1 ;
A6: ( x in { ((Subst ((the_arguments_of s),((Al a. 0) .--> y))) . k) where k is Element of NAT : ( 1 <= k & k <= len (Subst ((the_arguments_of s),((Al a. 0) .--> y))) & (Subst ((the_arguments_of s),((Al a. 0) .--> y))) . k in bound_QC-variables Al ) } implies x in { ((the_arguments_of s) . i) where i is Element of NAT : ( 1 <= i & i <= len (the_arguments_of s) & (the_arguments_of s) . i in bound_QC-variables Al ) } )
proof
assume x in { ((Subst ((the_arguments_of s),((Al a. 0) .--> y))) . k) where k is Element of NAT : ( 1 <= k & k <= len (Subst ((the_arguments_of s),((Al a. 0) .--> y))) & (Subst ((the_arguments_of s),((Al a. 0) .--> y))) . k in bound_QC-variables Al ) } ; ::_thesis: x in { ((the_arguments_of s) . i) where i is Element of NAT : ( 1 <= i & i <= len (the_arguments_of s) & (the_arguments_of s) . i in bound_QC-variables Al ) }
then consider k being Element of NAT such that
A7: x = (Subst ((the_arguments_of s),((Al a. 0) .--> y))) . k and
A8: 1 <= k and
A9: k <= len (Subst ((the_arguments_of s),((Al a. 0) .--> y))) and
(Subst ((the_arguments_of s),((Al a. 0) .--> y))) . k in bound_QC-variables Al ;
A10: k <= len (the_arguments_of s) by A9, CQC_LANG:def_1;
then x = (the_arguments_of s) . k by A3, A7, A8, CQC_LANG:3;
hence x in { ((the_arguments_of s) . i) where i is Element of NAT : ( 1 <= i & i <= len (the_arguments_of s) & (the_arguments_of s) . i in bound_QC-variables Al ) } by A8, A10; ::_thesis: verum
end;
A11: s . y = (the_pred_symbol_of s) ! (Subst ((the_arguments_of s),((Al a. 0) .--> y))) by A2, CQC_LANG:16;
A12: ( s . y is atomic & the_arguments_of (s . y) = Subst ((the_arguments_of s),((Al a. 0) .--> y)) )
proof
consider k being Element of NAT , p being QC-pred_symbol of k,Al, l2 being QC-variable_list of k,Al such that
A13: s = p ! l2 by A2, QC_LANG1:def_18;
l2 = the_arguments_of s by A2, A13, QC_LANG1:def_23;
then reconsider l3 = Subst ((the_arguments_of s),((Al a. 0) .--> y)) as QC-variable_list of k,Al ;
A14: s . y = p ! l3 by A2, A11, A13, QC_LANG1:def_22;
hence s . y is atomic by QC_LANG1:def_18; ::_thesis: the_arguments_of (s . y) = Subst ((the_arguments_of s),((Al a. 0) .--> y))
hence the_arguments_of (s . y) = Subst ((the_arguments_of s),((Al a. 0) .--> y)) by A14, QC_LANG1:def_23; ::_thesis: verum
end;
then still_not-bound_in (the_arguments_of (s . y)) = variables_in ((Subst ((the_arguments_of s),((Al a. 0) .--> y))),(bound_QC-variables Al)) by QC_LANG3:2
.= { ((Subst ((the_arguments_of s),((Al a. 0) .--> y))) . k) where k is Element of NAT : ( 1 <= k & k <= len (Subst ((the_arguments_of s),((Al a. 0) .--> y))) & (Subst ((the_arguments_of s),((Al a. 0) .--> y))) . k in bound_QC-variables Al ) } by QC_LANG3:def_1 ;
hence not x in still_not-bound_in (s . y) by A4, A5, A12, A6, QC_LANG3:4; ::_thesis: verum
end;
end;
thus S1[ VERUM Al] by CQC_LANG:15; ::_thesis: ( ( s is negative & S1[ the_argument_of s] implies S1[s] ) & ( s is conjunctive & S1[ the_left_argument_of s] & S1[ the_right_argument_of s] implies S1[s] ) & ( s is universal & S1[ the_scope_of s] implies S1[s] ) )
thus ( s is negative & S1[ the_argument_of s] implies S1[s] ) ::_thesis: ( ( s is conjunctive & S1[ the_left_argument_of s] & S1[ the_right_argument_of s] implies S1[s] ) & ( s is universal & S1[ the_scope_of s] implies S1[s] ) )
proof
assume that
A15: s is negative and
A16: ( ( 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) ) & x <> y & not x in still_not-bound_in s ) ; ::_thesis: not x in still_not-bound_in (s . y)
not x in still_not-bound_in ('not' ((the_argument_of s) . y)) by A15, A16, QC_LANG3:6, QC_LANG3:7;
hence not x in still_not-bound_in (s . y) by A15, CQC_LANG:18; ::_thesis: verum
end;
thus ( s is conjunctive & S1[ the_left_argument_of s] & S1[ the_right_argument_of s] implies S1[s] ) ::_thesis: ( s is universal & S1[ the_scope_of s] implies S1[s] )
proof
assume that
A17: s is conjunctive and
A18: ( ( 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) ) & ( 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) ) & x <> y & not x in still_not-bound_in s ) ; ::_thesis: not x in still_not-bound_in (s . y)
still_not-bound_in s = (still_not-bound_in (the_left_argument_of s)) \/ (still_not-bound_in (the_right_argument_of s)) by A17, QC_LANG3:9;
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 A18, XBOOLE_0:def_3;
then not x in still_not-bound_in (((the_left_argument_of s) . y) '&' ((the_right_argument_of s) . y)) by QC_LANG3:10;
hence not x in still_not-bound_in (s . y) by A17, CQC_LANG:20; ::_thesis: verum
end;
thus ( s is universal & S1[ the_scope_of s] implies S1[s] ) ::_thesis: verum
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 and
A22: not x in still_not-bound_in s ; ::_thesis: not x in still_not-bound_in (s . y)
A23: still_not-bound_in s = (still_not-bound_in (the_scope_of s)) \ {(bound_in s)} by A19, QC_LANG3:11;
thus not x in still_not-bound_in (s . y) ::_thesis: verum
proof
A24: now__::_thesis:_(_x_in_{(bound_in_s)}_implies_not_x_in_still_not-bound_in_(s_._y)_)
still_not-bound_in (All (x,((the_scope_of s) . y))) = (still_not-bound_in ((the_scope_of s) . y)) \ {x} by QC_LANG3:12;
then A25: ( ( not x in still_not-bound_in ((the_scope_of s) . y) or x in {x} ) iff not x in still_not-bound_in (All (x,((the_scope_of s) . y))) ) by XBOOLE_0:def_5;
assume x in {(bound_in s)} ; ::_thesis: not x in still_not-bound_in (s . y)
then x = bound_in s by TARSKI:def_1;
hence not x in still_not-bound_in (s . y) by A19, A21, A25, CQC_LANG:23, TARSKI:def_1; ::_thesis: verum
end;
now__::_thesis:_(_not_x_in_still_not-bound_in_(the_scope_of_s)_implies_not_x_in_still_not-bound_in_(s_._y)_)
assume not x in still_not-bound_in (the_scope_of s) ; ::_thesis: not x in still_not-bound_in (s . y)
then not x in (still_not-bound_in ((the_scope_of s) . y)) \ {(bound_in s)} by A20, A21, XBOOLE_0:def_5;
then not x in still_not-bound_in (All ((bound_in s),((the_scope_of s) . y))) by QC_LANG3:12;
hence not x in still_not-bound_in (s . y) by A19, A22, CQC_LANG:22, CQC_LANG:23; ::_thesis: verum
end;
hence not x in still_not-bound_in (s . y) by A22, A23, A24, XBOOLE_0:def_5; ::_thesis: verum
end;
end;
end;
for s being Element of QC-WFF Al holds S1[s] from QC_LANG1:sch_2(A1);
hence ( x <> y & not x in still_not-bound_in s9 implies not x in still_not-bound_in (s9 . y) ) ; ::_thesis: verum
end;
theorem Th32: :: VALUAT_1:32
for Al being QC-alphabet
for A being non empty set
for v being Element of Valuations_in (Al,A)
for J being interpretation of Al,A holds J,v |= VERUM Al
proof
let Al be QC-alphabet ; ::_thesis: for A being non empty set
for v being Element of Valuations_in (Al,A)
for J being interpretation of Al,A holds J,v |= VERUM Al
let A be non empty set ; ::_thesis: for v being Element of Valuations_in (Al,A)
for J being interpretation of Al,A holds J,v |= VERUM Al
let v be Element of Valuations_in (Al,A); ::_thesis: for J being interpretation of Al,A holds J,v |= VERUM Al
let J be interpretation of Al,A; ::_thesis: J,v |= VERUM Al
((Valuations_in (Al,A)) --> TRUE) . v = TRUE by FUNCOP_1:7;
then (Valid ((VERUM Al),J)) . v = TRUE by Lm1;
hence J,v |= VERUM Al by Def7; ::_thesis: verum
end;
theorem Th33: :: VALUAT_1:33
for Al being QC-alphabet
for A being non empty set
for v being Element of Valuations_in (Al,A)
for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A holds J,v |= (p '&' q) => (q '&' p)
proof
let Al be QC-alphabet ; ::_thesis: for A being non empty set
for v being Element of Valuations_in (Al,A)
for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A holds J,v |= (p '&' q) => (q '&' p)
let A be non empty set ; ::_thesis: for v being Element of Valuations_in (Al,A)
for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A holds J,v |= (p '&' q) => (q '&' p)
let v be Element of Valuations_in (Al,A); ::_thesis: for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A holds J,v |= (p '&' q) => (q '&' p)
let p, q be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A holds J,v |= (p '&' q) => (q '&' p)
let J be interpretation of Al,A; ::_thesis: J,v |= (p '&' q) => (q '&' p)
thus (Valid (((p '&' q) => (q '&' p)),J)) . v = TRUE :: according to VALUAT_1:def_7 ::_thesis: verum
proof
assume not (Valid (((p '&' q) => (q '&' p)),J)) . v = TRUE ; ::_thesis: contradiction
then A1: (Valid (((p '&' q) => (q '&' p)),J)) . v = FALSE by XBOOLEAN:def_3;
(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 Th10
.= 'not' (((Valid ((p '&' q),J)) . v) '&' ((Valid (('not' (q '&' p)),J)) . v)) by Th12
.= 'not' (((Valid ((p '&' q),J)) . v) '&' ('not' ((Valid ((q '&' p),J)) . v))) by Th10 ;
then A2: ((Valid ((p '&' q),J)) . v) '&' ('not' ((Valid ((q '&' p),J)) . v)) = TRUE by A1, MARGREL1:11;
then 'not' ((Valid ((q '&' p),J)) . v) = TRUE by MARGREL1:12;
then A3: (Valid ((q '&' p),J)) . v = FALSE by MARGREL1:11;
(Valid ((p '&' q),J)) . v = TRUE by A2, MARGREL1:12;
then ((Valid (p,J)) . v) '&' ((Valid (q,J)) . v) = TRUE by Th12;
hence contradiction by A3, Th12; ::_thesis: verum
end;
end;
theorem Th34: :: VALUAT_1:34
for Al being QC-alphabet
for A being non empty set
for v being Element of Valuations_in (Al,A)
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds J,v |= (('not' p) => p) => p
proof
let Al be QC-alphabet ; ::_thesis: for A being non empty set
for v being Element of Valuations_in (Al,A)
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds J,v |= (('not' p) => p) => p
let A be non empty set ; ::_thesis: for v being Element of Valuations_in (Al,A)
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds J,v |= (('not' p) => p) => p
let v be Element of Valuations_in (Al,A); ::_thesis: for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds J,v |= (('not' p) => p) => p
let p be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A holds J,v |= (('not' p) => p) => p
let J be interpretation of Al,A; ::_thesis: J,v |= (('not' p) => p) => p
('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 Th10
.= 'not' (((Valid (('not' (('not' p) '&' ('not' p))),J)) . v) '&' ((Valid (('not' p),J)) . v)) by Th12 ;
(Valid (('not' (('not' p) '&' ('not' p))),J)) . v = 'not' ((Valid ((('not' p) '&' ('not' p)),J)) . v) by Th10
.= 'not' ((Valid (('not' p),J)) . v) by Th22
.= 'not' ('not' ((Valid (p,J)) . v)) by Th10
.= (Valid (p,J)) . v ;
then (Valid (((('not' p) => p) => p),J)) . v = 'not' (((Valid (p,J)) . v) '&' ('not' ((Valid (p,J)) . v))) by A1, Th10
.= TRUE by XBOOLEAN:102 ;
hence (Valid (((('not' p) => p) => p),J)) . v = TRUE ; :: according to VALUAT_1:def_7 ::_thesis: verum
end;
theorem Th35: :: VALUAT_1:35
for Al being QC-alphabet
for A being non empty set
for v being Element of Valuations_in (Al,A)
for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A holds J,v |= p => (('not' p) => q)
proof
let Al be QC-alphabet ; ::_thesis: for A being non empty set
for v being Element of Valuations_in (Al,A)
for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A holds J,v |= p => (('not' p) => q)
let A be non empty set ; ::_thesis: for v being Element of Valuations_in (Al,A)
for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A holds J,v |= p => (('not' p) => q)
let v be Element of Valuations_in (Al,A); ::_thesis: for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A holds J,v |= p => (('not' p) => q)
let p, q be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A holds J,v |= p => (('not' p) => q)
let J be interpretation of Al,A; ::_thesis: J,v |= p => (('not' p) => q)
('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 Th10
.= 'not' (((Valid (p,J)) . v) '&' ((Valid (('not' ('not' (('not' p) '&' ('not' q)))),J)) . v)) by Th12 ;
(Valid (('not' ('not' (('not' p) '&' ('not' q)))),J)) . v = 'not' ((Valid (('not' (('not' p) '&' ('not' q))),J)) . v) by Th10
.= 'not' ('not' ((Valid ((('not' p) '&' ('not' q)),J)) . v)) by Th10
.= ((Valid (('not' p),J)) . v) '&' ((Valid (('not' q),J)) . v) by Th12
.= ('not' ((Valid (p,J)) . v)) '&' ((Valid (('not' q),J)) . v) by Th10
.= ('not' ((Valid (p,J)) . v)) '&' ('not' ((Valid (q,J)) . v)) by Th10 ;
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:16
.= 'not' (FALSE '&' ('not' ((Valid (q,J)) . v))) by XBOOLEAN:138 ;
FALSE '&' ('not' ((Valid (q,J)) . v)) = FALSE by MARGREL1:13;
hence (Valid ((p => (('not' p) => q)),J)) . v = TRUE by A2, MARGREL1:11; :: according to VALUAT_1:def_7 ::_thesis: verum
end;
theorem Th36: :: VALUAT_1:36
for Al being QC-alphabet
for A being non empty set
for v being Element of Valuations_in (Al,A)
for p, q, t being Element of CQC-WFF Al
for J being interpretation of Al,A holds J,v |= (p => q) => (('not' (q '&' t)) => ('not' (p '&' t)))
proof
let Al be QC-alphabet ; ::_thesis: for A being non empty set
for v being Element of Valuations_in (Al,A)
for p, q, t being Element of CQC-WFF Al
for J being interpretation of Al,A holds J,v |= (p => q) => (('not' (q '&' t)) => ('not' (p '&' t)))
let A be non empty set ; ::_thesis: for v being Element of Valuations_in (Al,A)
for p, q, t being Element of CQC-WFF Al
for J being interpretation of Al,A holds J,v |= (p => q) => (('not' (q '&' t)) => ('not' (p '&' t)))
let v be Element of Valuations_in (Al,A); ::_thesis: for p, q, t being Element of CQC-WFF Al
for J being interpretation of Al,A holds J,v |= (p => q) => (('not' (q '&' t)) => ('not' (p '&' t)))
let p, q, t be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A holds J,v |= (p => q) => (('not' (q '&' t)) => ('not' (p '&' t)))
let J be interpretation of Al,A; ::_thesis: J,v |= (p => q) => (('not' (q '&' t)) => ('not' (p '&' t)))
( p => q = 'not' (p '&' ('not' q)) & ('not' (q '&' t)) => ('not' (p '&' t)) = 'not' (('not' (q '&' t)) '&' ('not' ('not' (p '&' t)))) ) by QC_LANG2:def_2;
then A1: (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 QC_LANG2:def_2
.= 'not' ((Valid ((('not' (p '&' ('not' q))) '&' ('not' ('not' (('not' (q '&' t)) '&' ('not' ('not' (p '&' t))))))),J)) . v) by Th10
.= 'not' (((Valid (('not' (p '&' ('not' q))),J)) . v) '&' ((Valid (('not' ('not' (('not' (q '&' t)) '&' ('not' ('not' (p '&' t)))))),J)) . v)) by Th12 ;
A2: (Valid (('not' (p '&' ('not' q))),J)) . v = 'not' ((Valid ((p '&' ('not' q)),J)) . v) by Th10
.= 'not' (((Valid (p,J)) . v) '&' ((Valid (('not' q),J)) . v)) by Th12
.= 'not' (((Valid (p,J)) . v) '&' ('not' ((Valid (q,J)) . v))) by Th10 ;
(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 Th10
.= 'not' ('not' ((Valid ((('not' (q '&' t)) '&' ('not' ('not' (p '&' t)))),J)) . v)) by Th10
.= ((Valid (('not' (q '&' t)),J)) . v) '&' ((Valid (('not' ('not' (p '&' t))),J)) . v) by Th12
.= ('not' ((Valid ((q '&' t),J)) . v)) '&' ((Valid (('not' ('not' (p '&' t))),J)) . v) by Th10
.= ('not' ((Valid ((q '&' t),J)) . v)) '&' ('not' ((Valid (('not' (p '&' t)),J)) . v)) by Th10
.= ('not' ((Valid ((q '&' t),J)) . v)) '&' ('not' ('not' ((Valid ((p '&' t),J)) . v))) by Th10
.= ('not' (((Valid (q,J)) . v) '&' ((Valid (t,J)) . v))) '&' ((Valid ((p '&' t),J)) . v) by Th12
.= ('not' (((Valid (q,J)) . v) '&' ((Valid (t,J)) . v))) '&' (((Valid (p,J)) . v) '&' ((Valid (t,J)) . v)) by Th12 ;
hence (Valid (((p => q) => (('not' (q '&' t)) => ('not' (p '&' t)))),J)) . v = TRUE by A1, A2, Lm2; :: according to VALUAT_1:def_7 ::_thesis: verum
end;
theorem :: VALUAT_1:37
for Al being QC-alphabet
for A being non empty set
for v being Element of Valuations_in (Al,A)
for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A st J,v |= p & J,v |= p => q holds
J,v |= q by Th24;
theorem Th38: :: VALUAT_1:38
for Al being QC-alphabet
for A being non empty set
for x being bound_QC-variable of Al
for v being Element of Valuations_in (Al,A)
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds J,v |= (All (x,p)) => p
proof
let Al be QC-alphabet ; ::_thesis: for A being non empty set
for x being bound_QC-variable of Al
for v being Element of Valuations_in (Al,A)
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds J,v |= (All (x,p)) => p
let A be non empty set ; ::_thesis: for x being bound_QC-variable of Al
for v being Element of Valuations_in (Al,A)
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds J,v |= (All (x,p)) => p
let x be bound_QC-variable of Al; ::_thesis: for v being Element of Valuations_in (Al,A)
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds J,v |= (All (x,p)) => p
let v be Element of Valuations_in (Al,A); ::_thesis: for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds J,v |= (All (x,p)) => p
let p be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A holds J,v |= (All (x,p)) => p
let J be interpretation of Al,A; ::_thesis: J,v |= (All (x,p)) => p
thus (Valid (((All (x,p)) => p),J)) . v = TRUE :: according to VALUAT_1:def_7 ::_thesis: verum
proof
assume not (Valid (((All (x,p)) => p),J)) . v = TRUE ; ::_thesis: contradiction
then A1: (Valid (((All (x,p)) => p),J)) . v = FALSE by XBOOLEAN:def_3;
(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 Th10
.= 'not' (((Valid ((All (x,p)),J)) . v) '&' ((Valid (('not' p),J)) . v)) by Th12
.= 'not' (((Valid ((All (x,p)),J)) . v) '&' ('not' ((Valid (p,J)) . v))) by Th10 ;
then A2: ((Valid ((All (x,p)),J)) . v) '&' ('not' ((Valid (p,J)) . v)) = TRUE by A1, MARGREL1:11;
then 'not' ((Valid (p,J)) . v) = TRUE by MARGREL1:12;
then A3: (Valid (p,J)) . v = FALSE by MARGREL1:11;
(Valid ((All (x,p)),J)) . v = TRUE by A2, MARGREL1:12;
then (FOR_ALL (x,(Valid (p,J)))) . v = TRUE by Lm1;
hence contradiction by A3, Th25; ::_thesis: verum
end;
end;
theorem :: VALUAT_1:39
for Al being QC-alphabet
for A being non empty set
for J being interpretation of Al,A holds J |= VERUM Al
proof
let Al be QC-alphabet ; ::_thesis: for A being non empty set
for J being interpretation of Al,A holds J |= VERUM Al
let A be non empty set ; ::_thesis: for J being interpretation of Al,A holds J |= VERUM Al
let J be interpretation of Al,A; ::_thesis: J |= VERUM Al
let v be Element of Valuations_in (Al,A); :: according to VALUAT_1:def_8 ::_thesis: J,v |= VERUM Al
thus J,v |= VERUM Al by Th32; ::_thesis: verum
end;
theorem :: VALUAT_1:40
for Al being QC-alphabet
for A being non empty set
for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A holds J |= (p '&' q) => (q '&' p)
proof
let Al be QC-alphabet ; ::_thesis: for A being non empty set
for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A holds J |= (p '&' q) => (q '&' p)
let A be non empty set ; ::_thesis: for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A holds J |= (p '&' q) => (q '&' p)
let p, q be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A holds J |= (p '&' q) => (q '&' p)
let J be interpretation of Al,A; ::_thesis: J |= (p '&' q) => (q '&' p)
let v be Element of Valuations_in (Al,A); :: according to VALUAT_1:def_8 ::_thesis: J,v |= (p '&' q) => (q '&' p)
thus J,v |= (p '&' q) => (q '&' p) by Th33; ::_thesis: verum
end;
theorem :: VALUAT_1:41
for Al being QC-alphabet
for A being non empty set
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds J |= (('not' p) => p) => p
proof
let Al be QC-alphabet ; ::_thesis: for A being non empty set
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds J |= (('not' p) => p) => p
let A be non empty set ; ::_thesis: for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds J |= (('not' p) => p) => p
let p be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A holds J |= (('not' p) => p) => p
let J be interpretation of Al,A; ::_thesis: J |= (('not' p) => p) => p
let v be Element of Valuations_in (Al,A); :: according to VALUAT_1:def_8 ::_thesis: J,v |= (('not' p) => p) => p
thus J,v |= (('not' p) => p) => p by Th34; ::_thesis: verum
end;
theorem :: VALUAT_1:42
for Al being QC-alphabet
for A being non empty set
for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A holds J |= p => (('not' p) => q)
proof
let Al be QC-alphabet ; ::_thesis: for A being non empty set
for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A holds J |= p => (('not' p) => q)
let A be non empty set ; ::_thesis: for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A holds J |= p => (('not' p) => q)
let p, q be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A holds J |= p => (('not' p) => q)
let J be interpretation of Al,A; ::_thesis: J |= p => (('not' p) => q)
let v be Element of Valuations_in (Al,A); :: according to VALUAT_1:def_8 ::_thesis: J,v |= p => (('not' p) => q)
thus J,v |= p => (('not' p) => q) by Th35; ::_thesis: verum
end;
theorem :: VALUAT_1:43
for Al being QC-alphabet
for A being non empty set
for p, q, t being Element of CQC-WFF Al
for J being interpretation of Al,A holds J |= (p => q) => (('not' (q '&' t)) => ('not' (p '&' t)))
proof
let Al be QC-alphabet ; ::_thesis: for A being non empty set
for p, q, t being Element of CQC-WFF Al
for J being interpretation of Al,A holds J |= (p => q) => (('not' (q '&' t)) => ('not' (p '&' t)))
let A be non empty set ; ::_thesis: for p, q, t being Element of CQC-WFF Al
for J being interpretation of Al,A holds J |= (p => q) => (('not' (q '&' t)) => ('not' (p '&' t)))
let p, q, t be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A holds J |= (p => q) => (('not' (q '&' t)) => ('not' (p '&' t)))
let J be interpretation of Al,A; ::_thesis: J |= (p => q) => (('not' (q '&' t)) => ('not' (p '&' t)))
let v be Element of Valuations_in (Al,A); :: according to VALUAT_1:def_8 ::_thesis: J,v |= (p => q) => (('not' (q '&' t)) => ('not' (p '&' t)))
thus J,v |= (p => q) => (('not' (q '&' t)) => ('not' (p '&' t))) by Th36; ::_thesis: verum
end;
theorem :: VALUAT_1:44
for Al being QC-alphabet
for A being non empty set
for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A st J |= p & J |= p => q holds
J |= q
proof
let Al be QC-alphabet ; ::_thesis: for A being non empty set
for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A st J |= p & J |= p => q holds
J |= q
let A be non empty set ; ::_thesis: for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A st J |= p & J |= p => q holds
J |= q
let p, q be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A st J |= p & J |= p => q holds
J |= q
let J be interpretation of Al,A; ::_thesis: ( J |= p & J |= p => q implies J |= q )
assume A1: ( J |= p & J |= p => q ) ; ::_thesis: J |= q
now__::_thesis:_for_v_being_Element_of_Valuations_in_(Al,A)_holds_J,v_|=_q
let v be Element of Valuations_in (Al,A); ::_thesis: J,v |= q
( J,v |= p & J,v |= p => q ) by A1, Def8;
hence J,v |= q by Th24; ::_thesis: verum
end;
hence J |= q by Def8; ::_thesis: verum
end;
theorem :: VALUAT_1:45
for Al being QC-alphabet
for A being non empty set
for x being bound_QC-variable of Al
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds J |= (All (x,p)) => p
proof
let Al be QC-alphabet ; ::_thesis: for A being non empty set
for x being bound_QC-variable of Al
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds J |= (All (x,p)) => p
let A be non empty set ; ::_thesis: for x being bound_QC-variable of Al
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds J |= (All (x,p)) => p
let x be bound_QC-variable of Al; ::_thesis: for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds J |= (All (x,p)) => p
let p be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A holds J |= (All (x,p)) => p
let J be interpretation of Al,A; ::_thesis: J |= (All (x,p)) => p
let v be Element of Valuations_in (Al,A); :: according to VALUAT_1:def_8 ::_thesis: J,v |= (All (x,p)) => p
thus J,v |= (All (x,p)) => p by Th38; ::_thesis: verum
end;
theorem :: VALUAT_1:46
for Al being QC-alphabet
for A being non empty set
for x being bound_QC-variable of Al
for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A st J |= p => q & not x in still_not-bound_in p holds
J |= p => (All (x,q))
proof
let Al be QC-alphabet ; ::_thesis: for A being non empty set
for x being bound_QC-variable of Al
for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A st J |= p => q & not x in still_not-bound_in p holds
J |= p => (All (x,q))
let A be non empty set ; ::_thesis: for x being bound_QC-variable of Al
for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A st J |= p => q & not x in still_not-bound_in p holds
J |= p => (All (x,q))
let x be bound_QC-variable of Al; ::_thesis: for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A st J |= p => q & not x in still_not-bound_in p holds
J |= p => (All (x,q))
let p, q be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A st J |= p => q & not x in still_not-bound_in p holds
J |= p => (All (x,q))
let J be interpretation of Al,A; ::_thesis: ( J |= p => q & not x in still_not-bound_in p implies J |= p => (All (x,q)) )
assume that
A1: for v being Element of Valuations_in (Al,A) holds J,v |= p => q and
A2: not x in still_not-bound_in p ; :: according to VALUAT_1:def_8 ::_thesis: J |= p => (All (x,q))
let u be Element of Valuations_in (Al,A); :: according to VALUAT_1:def_8 ::_thesis: J,u |= p => (All (x,q))
now__::_thesis:_(_J,u_|=_p_implies_J,u_|=_All_(x,q)_)
assume A3: J,u |= p ; ::_thesis: J,u |= All (x,q)
now__::_thesis:_for_w_being_Element_of_Valuations_in_(Al,A)_st_(_for_y_being_bound_QC-variable_of_Al_st_x_<>_y_holds_
w_._y_=_u_._y_)_holds_
J,w_|=_q
let w be Element of Valuations_in (Al,A); ::_thesis: ( ( for y being bound_QC-variable of Al st x <> y holds
w . y = u . y ) implies J,w |= q )
assume for y being bound_QC-variable of Al st x <> y holds
w . y = u . y ; ::_thesis: J,w |= q
then A4: J,w |= p by A2, A3, Th28;
J,w |= p => q by A1;
hence J,w |= q by A4, Th24; ::_thesis: verum
end;
hence J,u |= All (x,q) by Th29; ::_thesis: verum
end;
hence J,u |= p => (All (x,q)) by Th24; ::_thesis: verum
end;
theorem :: VALUAT_1:47
for Al being QC-alphabet
for A being non empty set
for x, y being bound_QC-variable of Al
for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A
for s being QC-formula of Al st p = s . x & q = s . y & not x in still_not-bound_in s & J |= p holds
J |= q
proof
let Al be QC-alphabet ; ::_thesis: for A being non empty set
for x, y being bound_QC-variable of Al
for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A
for s being QC-formula of Al st p = s . x & q = s . y & not x in still_not-bound_in s & J |= p holds
J |= q
let A be non empty set ; ::_thesis: for x, y being bound_QC-variable of Al
for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A
for s being QC-formula of Al st p = s . x & q = s . y & not x in still_not-bound_in s & J |= p holds
J |= q
let x, y be bound_QC-variable of Al; ::_thesis: for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A
for s being QC-formula of Al st p = s . x & q = s . y & not x in still_not-bound_in s & J |= p holds
J |= q
let p, q be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A
for s being QC-formula of Al st p = s . x & q = s . y & not x in still_not-bound_in s & J |= p holds
J |= q
let J be interpretation of Al,A; ::_thesis: for s being QC-formula of Al st p = s . x & q = s . y & not x in still_not-bound_in s & J |= p holds
J |= q
let s be QC-formula of Al; ::_thesis: ( p = s . x & q = s . y & not x in still_not-bound_in s & J |= p implies J |= q )
assume that
A1: p = s . x and
A2: q = s . y and
A3: not x in still_not-bound_in s and
A4: J |= p ; ::_thesis: J |= q
now__::_thesis:_(_x_<>_y_implies_J_|=_q_)
assume A5: x <> y ; ::_thesis: J |= q
A6: now__::_thesis:_for_u_being_Element_of_Valuations_in_(Al,A)_holds_(Valid_(q,J))_._u_=_TRUE
let u be Element of Valuations_in (Al,A); ::_thesis: (Valid (q,J)) . u = TRUE
consider w being Element of Valuations_in (Al,A) such that
A7: ( ( for z being bound_QC-variable of Al st z <> x holds
w . z = u . z ) & w . x = u . y ) by Lm3;
w . x = w . y by A7;
then A8: (Valid (p,J)) . w = (Valid (q,J)) . w by A1, A2, Th30;
J,w |= p by A4, Def8;
then A9: (Valid (p,J)) . w = TRUE by Def7;
not x in still_not-bound_in q by A2, A3, A5, Th31;
hence (Valid (q,J)) . u = TRUE by A7, A8, A9, Th27; ::_thesis: verum
end;
now__::_thesis:_for_v_being_Element_of_Valuations_in_(Al,A)_holds_J,v_|=_q
let v be Element of Valuations_in (Al,A); ::_thesis: J,v |= q
(Valid (q,J)) . v = TRUE by A6;
hence J,v |= q by Def7; ::_thesis: verum
end;
hence J |= q by Def8; ::_thesis: verum
end;
hence J |= q by A1, A2, A4; ::_thesis: verum
end;