:: Interpretation and Satisfiability in the First Order Logic
:: by Edmund Woronowicz
::
:: Received June 1, 1990
:: Copyright (c) 1990-2011 Association of Mizar Users

begin

definition

let A be set ;
func Valuations_in A -> set equals :: VALUAT_1:def 1
Funcs (bound_QC-variables,A);
coherence
Funcs (bound_QC-variables,A) is set ;

end;

:: deftheorem defines Valuations_in VALUAT_1:def 1 :
for A being set holds Valuations_in A = Funcs (bound_QC-variables,A);

registration

let A be non empty set ;
cluster Valuations_in A -> functional non empty ;
coherence
( not Valuations_in A is empty & Valuations_in A is functional ) ;

end;

theorem :: VALUAT_1:1

canceled;

theorem Th2: :: VALUAT_1:2

for A being non empty set
for x being set st x is Element of Valuations_in A holds
x is Function of bound_QC-variables,A

proof end;

definition

let A be non empty set ;
:: original: Valuations_in
redefine func Valuations_in A -> FUNCTION_DOMAIN of bound_QC-variables ,A;
coherence
Valuations_in A is FUNCTION_DOMAIN of bound_QC-variables ,A

proof end;

end;

definition

canceled;
canceled;
canceled;
canceled;
canceled;
let A be non empty set ;
let x be bound_QC-variable;
let p be Element of Funcs ((Valuations_in A),BOOLEAN);
func FOR_ALL (x,p) -> Element of Funcs ((Valuations_in A),BOOLEAN) means :Def7: :: VALUAT_1:def 7
for v being Element of Valuations_in A holds it . v = ALL { (p . v9) where v9 is Element of Valuations_in A : for y being bound_QC-variable st x <> y holds
v9 . y = v . y } ;
existence
ex b₁ being Element of Funcs ((Valuations_in A),BOOLEAN) st
for v being Element of Valuations_in A holds b₁ . v = ALL { (p . v9) where v9 is Element of Valuations_in A : for y being bound_QC-variable st x <> y holds
v9 . y = v . y }

proof end;

uniqueness
for b₁, b₂ being Element of Funcs ((Valuations_in A),BOOLEAN) st ( for v being Element of Valuations_in A holds b₁ . v = ALL { (p . v9) where v9 is Element of Valuations_in A : for y being bound_QC-variable st x <> y holds
v9 . y = v . y } ) & ( for v being Element of Valuations_in A holds b₂ . v = ALL { (p . v9) where v9 is Element of Valuations_in A : for y being bound_QC-variable st x <> y holds
v9 . y = v . y } ) holds
b₁ = b₂

proof end;

end;

:: deftheorem VALUAT_1:def 2 :
canceled;

:: deftheorem VALUAT_1:def 3 :
canceled;

:: deftheorem VALUAT_1:def 4 :
canceled;

:: deftheorem VALUAT_1:def 5 :
canceled;

:: deftheorem VALUAT_1:def 6 :
canceled;

:: deftheorem Def7 defines FOR_ALL VALUAT_1:def 7 :
for A being non empty set
for x being bound_QC-variable
for p, b₄ being Element of Funcs ((Valuations_in A),BOOLEAN) holds
( b₄ = FOR_ALL (x,p) iff for v being Element of Valuations_in A holds b₄ . v = ALL { (p . v9) where v9 is Element of Valuations_in A : for y being bound_QC-variable st x <> y holds
v9 . y = v . y } );

theorem :: VALUAT_1:3

canceled;

theorem :: VALUAT_1:4

canceled;

theorem :: VALUAT_1:5

canceled;

theorem :: VALUAT_1:6

canceled;

theorem Th7: :: VALUAT_1:7

for A being non empty set
for x being bound_QC-variable
for v being Element of Valuations_in A
for p being Element of Funcs ((Valuations_in A),BOOLEAN) holds
( (FOR_ALL (x,p)) . v = FALSE iff ex v1 being Element of Valuations_in A st
( p . v1 = FALSE & ( for y being bound_QC-variable st x <> y holds
v1 . y = v . y ) ) )

proof end;

theorem Th8: :: VALUAT_1:8

for A being non empty set
for x being bound_QC-variable
for v being Element of Valuations_in A
for p being Element of Funcs ((Valuations_in A),BOOLEAN) holds
( (FOR_ALL (x,p)) . v = TRUE iff for v1 being Element of Valuations_in A st ( for y being bound_QC-variable st x <> y holds
v1 . y = v . y ) holds
p . v1 = TRUE )

proof end;

notation

let A be non empty set ;
let k be Element of NAT ;
let ll be CQC-variable_list of k;
let v be Element of Valuations_in A;
synonym v *' ll for k * A;

end;

definition

let A be non empty set ;
let k be Element of NAT ;
let ll be CQC-variable_list of k;
let v be Element of Valuations_in A;
:: original: *'
redefine func v *' ll -> FinSequence of A means :Def8: :: VALUAT_1:def 8
( len it = k & ( for i being Nat st 1 <= i & i <= k holds
it . i = v . (ll . i) ) );
coherence
*' is FinSequence of A

proof end;

compatibility
for b₁ being FinSequence of A holds
( b₁ = *' iff ( len b₁ = k & ( for i being Nat st 1 <= i & i <= k holds
b₁ . i = v . (ll . i) ) ) )

proof end;

end;

:: deftheorem Def8 defines *' VALUAT_1:def 8 :
for A being non empty set
for k being Element of NAT
for ll being CQC-variable_list of k
for v being Element of Valuations_in A
for b₅ being FinSequence of A holds
( b₅ = v *' ll iff ( len b₅ = k & ( for i being Nat st 1 <= i & i <= k holds
b₅ . i = v . (ll . i) ) ) );

definition

let A be non empty set ;
let k be Element of NAT ;
let ll be CQC-variable_list of k;
let r be Element of relations_on A;
func ll 'in' r -> Element of Funcs ((Valuations_in A),BOOLEAN) means :Def9: :: VALUAT_1:def 9
for v being Element of Valuations_in A holds
( ( v *' ll in r implies it . v = TRUE ) & ( not v *' ll in r implies it . v = FALSE ) );
existence
ex b₁ being Element of Funcs ((Valuations_in A),BOOLEAN) st
for v being Element of Valuations_in A holds
( ( v *' ll in r implies b₁ . v = TRUE ) & ( not v *' ll in r implies b₁ . v = FALSE ) )

proof end;

uniqueness
for b₁, b₂ being Element of Funcs ((Valuations_in A),BOOLEAN) st ( for v being Element of Valuations_in A holds
( ( v *' ll in r implies b₁ . v = TRUE ) & ( not v *' ll in r implies b₁ . v = FALSE ) ) ) & ( for v being Element of Valuations_in A holds
( ( v *' ll in r implies b₂ . v = TRUE ) & ( not v *' ll in r implies b₂ . v = FALSE ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def9 defines 'in' VALUAT_1:def 9 :
for A being non empty set
for k being Element of NAT
for ll being CQC-variable_list of k
for r being Element of relations_on A
for b₅ being Element of Funcs ((Valuations_in A),BOOLEAN) holds
( b₅ = ll 'in' r iff for v being Element of Valuations_in A holds
( ( v *' ll in r implies b₅ . v = TRUE ) & ( not v *' ll in r implies b₅ . v = FALSE ) ) );

definition

let A be non empty set ;
let F be Function of CQC-WFF,(Funcs ((Valuations_in A),BOOLEAN));
let p be Element of CQC-WFF ;
:: original: .
redefine func F . p -> Element of Funcs ((Valuations_in A),BOOLEAN);
coherence
F . p is Element of Funcs ((Valuations_in A),BOOLEAN)

proof end;

end;

definition

let D be non empty set ;
mode interpretation of D -> Function of QC-pred_symbols,(relations_on D) means :: VALUAT_1:def 10
for P being Element of QC-pred_symbols
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 b₁ being Function of QC-pred_symbols,(relations_on D) st
for P being Element of QC-pred_symbols
for r being Element of relations_on D holds
( not b₁ . P = r or r = empty_rel D or the_arity_of P = the_arity_of r )

proof end;

end;

:: deftheorem defines interpretation VALUAT_1:def 10 :
for D being non empty set
for b₂ being Function of QC-pred_symbols,(relations_on D) holds
( b₂ is interpretation of D iff for P being Element of QC-pred_symbols
for r being Element of relations_on D holds
( not b₂ . P = r or r = empty_rel D or the_arity_of P = the_arity_of r ) );

definition

let A be non empty set ;
let k be Element of NAT ;
let J be interpretation of A;
let P be QC-pred_symbol of k;
:: original: .
redefine func J . P -> Element of relations_on A;
coherence
J . P is Element of relations_on A by FUNCT_2:7;

end;

definition

let A be non empty set ;
let J be interpretation of A;
let p be Element of CQC-WFF ;
func Valid (p,J) -> Element of Funcs ((Valuations_in A),BOOLEAN) means :Def11: :: VALUAT_1:def 11
ex F being Function of CQC-WFF,(Funcs ((Valuations_in A),BOOLEAN)) st
( it = F . p & F . VERUM = (Valuations_in A) --> TRUE & ( for p, q being Element of CQC-WFF
for x being bound_QC-variable
for k being Element of NAT
for ll being CQC-variable_list of k
for P being QC-pred_symbol of k holds
( F . (P ! ll) = ll 'in' (J . P) & F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) ) ) );
correctness
existence
ex b₁ being Element of Funcs ((Valuations_in A),BOOLEAN) ex F being Function of CQC-WFF,(Funcs ((Valuations_in A),BOOLEAN)) st
( b₁ = F . p & F . VERUM = (Valuations_in A) --> TRUE & ( for p, q being Element of CQC-WFF
for x being bound_QC-variable
for k being Element of NAT
for ll being CQC-variable_list of k
for P being QC-pred_symbol of k holds
( F . (P ! ll) = ll 'in' (J . P) & F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) ) ) );
uniqueness
for b₁, b₂ being Element of Funcs ((Valuations_in A),BOOLEAN) st ex F being Function of CQC-WFF,(Funcs ((Valuations_in A),BOOLEAN)) st
( b₁ = F . p & F . VERUM = (Valuations_in A) --> TRUE & ( for p, q being Element of CQC-WFF
for x being bound_QC-variable
for k being Element of NAT
for ll being CQC-variable_list of k
for P being QC-pred_symbol of k holds
( F . (P ! ll) = ll 'in' (J . P) & F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) ) ) ) & ex F being Function of CQC-WFF,(Funcs ((Valuations_in A),BOOLEAN)) st
( b₂ = F . p & F . VERUM = (Valuations_in A) --> TRUE & ( for p, q being Element of CQC-WFF
for x being bound_QC-variable
for k being Element of NAT
for ll being CQC-variable_list of k
for P being QC-pred_symbol of k holds
( F . (P ! ll) = ll 'in' (J . P) & F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) ) ) ) holds
b₁ = b₂;

proof end;

end;

:: deftheorem Def11 defines Valid VALUAT_1:def 11 :
for A being non empty set
for J being interpretation of A
for p being Element of CQC-WFF
for b₄ being Element of Funcs ((Valuations_in A),BOOLEAN) holds
( b₄ = Valid (p,J) iff ex F being Function of CQC-WFF,(Funcs ((Valuations_in A),BOOLEAN)) st
( b₄ = F . p & F . VERUM = (Valuations_in A) --> TRUE & ( for p, q being Element of CQC-WFF
for x being bound_QC-variable
for k being Element of NAT
for ll being CQC-variable_list of k
for P being QC-pred_symbol of k holds
( F . (P ! ll) = ll 'in' (J . P) & F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) ) ) ) );

theorem :: VALUAT_1:9

canceled;

theorem :: VALUAT_1:10

canceled;

theorem :: VALUAT_1:11

canceled;

theorem :: VALUAT_1:12

canceled;

Lm1: for p being Element of CQC-WFF
for A being non empty set
for J being interpretation of A holds
( Valid (VERUM,J) = (Valuations_in A) --> TRUE & ( for k being Element of NAT
for ll being CQC-variable_list of k
for P being QC-pred_symbol of k holds Valid ((P ! ll),J) = ll 'in' (J . P) ) & ( for p being Element of CQC-WFF holds Valid (('not' p),J) = 'not' (Valid (p,J)) ) & ( for q being Element of CQC-WFF holds Valid ((p '&' q),J) = (Valid (p,J)) '&' (Valid (q,J)) ) & ( for x being bound_QC-variable holds Valid ((All (x,p)),J) = FOR_ALL (x,(Valid (p,J))) ) )

proof end;

theorem :: VALUAT_1:13

for A being non empty set
for J being interpretation of A holds Valid (VERUM,J) = (Valuations_in A) --> TRUE by Lm1;

theorem Th14: :: VALUAT_1:14

for A being non empty set
for v being Element of Valuations_in A
for J being interpretation of A holds (Valid (VERUM,J)) . v = TRUE

proof end;

theorem :: VALUAT_1:15

for k being Element of NAT
for A being non empty set
for ll being CQC-variable_list of k
for J being interpretation of A
for P being QC-pred_symbol of k holds Valid ((P ! ll),J) = ll 'in' (J . P) by Lm1;

theorem Th16: :: VALUAT_1:16

for k being Element of NAT
for A being non empty set
for v being Element of Valuations_in A
for ll being CQC-variable_list of k
for p being Element of CQC-WFF
for J being interpretation of A
for P being QC-pred_symbol of k
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 end;

theorem Th17: :: VALUAT_1:17

for k being Element of NAT
for A being non empty set
for v being Element of Valuations_in A
for ll being CQC-variable_list of k
for p being Element of CQC-WFF
for J being interpretation of A
for P being QC-pred_symbol of k
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 end;

theorem :: VALUAT_1:18

canceled;

theorem :: VALUAT_1:19

for A being non empty set
for p being Element of CQC-WFF
for J being interpretation of A holds Valid (('not' p),J) = 'not' (Valid (p,J)) by Lm1;

theorem Th20: :: VALUAT_1:20

for A being non empty set
for v being Element of Valuations_in A
for p being Element of CQC-WFF
for J being interpretation of A holds (Valid (('not' p),J)) . v = 'not' ((Valid (p,J)) . v)

proof end;

theorem :: VALUAT_1:21

for A being non empty set
for p, q being Element of CQC-WFF
for J being interpretation of A holds Valid ((p '&' q),J) = (Valid (p,J)) '&' (Valid (q,J)) by Lm1;

theorem Th22: :: VALUAT_1:22

for A being non empty set
for v being Element of Valuations_in A
for p, q being Element of CQC-WFF
for J being interpretation of A holds (Valid ((p '&' q),J)) . v = ((Valid (p,J)) . v) '&' ((Valid (q,J)) . v)

proof end;

theorem :: VALUAT_1:23

for A being non empty set
for x being bound_QC-variable
for p being Element of CQC-WFF
for J being interpretation of A holds Valid ((All (x,p)),J) = FOR_ALL (x,(Valid (p,J))) by Lm1;

theorem Th24: :: VALUAT_1:24

for A being non empty set
for v being Element of Valuations_in A
for p being Element of CQC-WFF
for J being interpretation of A holds (Valid ((p '&' ('not' p)),J)) . v = FALSE

proof end;

theorem :: VALUAT_1:25

for A being non empty set
for v being Element of Valuations_in A
for p being Element of CQC-WFF
for J being interpretation of A holds (Valid (('not' (p '&' ('not' p))),J)) . v = TRUE

proof end;

definition

let A be non empty set ;
let p be Element of CQC-WFF ;
let J be interpretation of A;
let v be Element of Valuations_in A;
pred J,v |= p means :Def12: :: VALUAT_1:def 12
(Valid (p,J)) . v = TRUE ;

end;

:: deftheorem Def12 defines |= VALUAT_1:def 12 :
for A being non empty set
for p being Element of CQC-WFF
for J being interpretation of A
for v being Element of Valuations_in A holds
( J,v |= p iff (Valid (p,J)) . v = TRUE );

theorem :: VALUAT_1:26

canceled;

theorem :: VALUAT_1:27

for k being Element of NAT
for A being non empty set
for v being Element of Valuations_in A
for ll being CQC-variable_list of k
for J being interpretation of A
for P being QC-pred_symbol of k holds
( J,v |= P ! ll iff (ll 'in' (J . P)) . v = TRUE )

proof end;

theorem :: VALUAT_1:28

for A being non empty set
for v being Element of Valuations_in A
for p being Element of CQC-WFF
for J being interpretation of A holds
( J,v |= 'not' p iff not J,v |= p )

proof end;

theorem :: VALUAT_1:29

for A being non empty set
for v being Element of Valuations_in A
for p, q being Element of CQC-WFF
for J being interpretation of A holds
( J,v |= p '&' q iff ( J,v |= p & J,v |= q ) )

proof end;

theorem Th30: :: VALUAT_1:30

for A being non empty set
for x being bound_QC-variable
for v being Element of Valuations_in A
for p being Element of CQC-WFF
for J being interpretation of A holds
( J,v |= All (x,p) iff (FOR_ALL (x,(Valid (p,J)))) . v = TRUE )

proof end;

theorem Th31: :: VALUAT_1:31

for A being non empty set
for x being bound_QC-variable
for v being Element of Valuations_in A
for p being Element of CQC-WFF
for J being interpretation of A holds
( J,v |= All (x,p) iff for v1 being Element of Valuations_in A st ( for y being bound_QC-variable st x <> y holds
v1 . y = v . y ) holds
(Valid (p,J)) . v1 = TRUE )

proof end;

theorem :: VALUAT_1:32

for A being non empty set
for p being Element of CQC-WFF
for J being interpretation of A holds Valid (('not' ('not' p)),J) = Valid (p,J)

proof end;

theorem Th33: :: VALUAT_1:33

for A being non empty set
for p being Element of CQC-WFF
for J being interpretation of A holds Valid ((p '&' p),J) = Valid (p,J)

proof end;

theorem :: VALUAT_1:34

canceled;

theorem Th35: :: VALUAT_1:35

for A being non empty set
for v being Element of Valuations_in A
for p, q being Element of CQC-WFF
for J being interpretation of A holds
( J,v |= p => q iff ( (Valid (p,J)) . v = FALSE or (Valid (q,J)) . v = TRUE ) )

proof end;

theorem Th36: :: VALUAT_1:36

for A being non empty set
for v being Element of Valuations_in A
for p, q being Element of CQC-WFF
for J being interpretation of A holds
( J,v |= p => q iff ( J,v |= p implies J,v |= q ) )

proof end;

theorem Th37: :: VALUAT_1:37

for A being non empty set
for x being bound_QC-variable
for v being Element of Valuations_in A
for p being Element of Funcs ((Valuations_in A),BOOLEAN) st (FOR_ALL (x,p)) . v = TRUE holds
p . v = TRUE

proof end;

definition

let A be non empty set ;
let J be interpretation of A;
let p be Element of CQC-WFF ;
pred J |= p means :Def13: :: VALUAT_1:def 13
for v being Element of Valuations_in A holds J,v |= p;

end;

:: deftheorem Def13 defines |= VALUAT_1:def 13 :
for A being non empty set
for J being interpretation of A
for p being Element of CQC-WFF holds
( J |= p iff for v being Element of Valuations_in 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 end;

Lm3: now

let A be non empty set ; :: thesis: for Y, Z being bound_QC-variable
for V1, V2 being Element of Valuations_in A ex v being Element of Valuations_in A st
( ( for x being bound_QC-variable st x <> Y holds
v . x = V1 . x ) & v . Y = V2 . Z )
let Y, Z be bound_QC-variable; :: thesis: for V1, V2 being Element of Valuations_in A ex v being Element of Valuations_in A st
( ( for x being bound_QC-variable st x <> Y holds
v . x = V1 . x ) & v . Y = V2 . Z )
let V1, V2 be Element of Valuations_in A; :: thesis: ex v being Element of Valuations_in A st
( ( for x being bound_QC-variable st x <> Y holds
v . x = V1 . x ) & v . Y = V2 . Z )
thus ex v being Element of Valuations_in A st
( ( for x being bound_QC-variable st x <> Y holds
v . x = V1 . x ) & v . Y = V2 . Z ) :: thesis: verum

proof

deffunc H₁( set ) -> Element of A = V2 . Z;
deffunc H₂( set ) -> set = V1 . $1;
defpred S₁[ set ] means for x1 being bound_QC-variable st x1 = $1 holds
x1 <> Y;
A1: for x being set st x in bound_QC-variables holds
( ( S₁[x] implies H₂(x) in A ) & ( not S₁[x] implies H₁(x) in A ) ) by FUNCT_2:7;
consider f being Function of bound_QC-variables,A such that
A2: for x being set st x in bound_QC-variables holds
( ( S₁[x] implies f . x = H₂(x) ) & ( not S₁[x] implies f . x = H₁(x) ) ) from FUNCT_2:sch 5(A1);
( dom f = bound_QC-variables & rng f c= A ) by FUNCT_2:def 1, RELAT_1:def 19;
then reconsider f = f as Element of Valuations_in A by FUNCT_2:def 2;
take f ; :: thesis: ( ( for x being bound_QC-variable st x <> Y holds
f . x = V1 . x ) & f . Y = V2 . Z )

now

let x be bound_QC-variable; :: thesis: ( ( x <> Y implies f . x = V1 . x ) & ( x = Y implies f . Y = V2 . Z ) )

now

assume A3: x <> Y ; :: thesis: f . x = V1 . x
( ( for x1 being bound_QC-variable 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 st x <> Y holds
f . x = V1 . x ) & f . Y = V2 . Z ) ; :: thesis: verum

end;

end;

theorem :: VALUAT_1:38

for A being non empty set
for Y, Z being bound_QC-variable
for V1, V2 being Element of Valuations_in A ex v being Element of Valuations_in A st
( ( for x being bound_QC-variable st x <> Y holds
v . x = V1 . x ) & v . Y = V2 . Z ) by Lm3;

theorem Th39: :: VALUAT_1:39

for A being non empty set
for x being bound_QC-variable
for p being Element of CQC-WFF
for J being interpretation of A st not x in still_not-bound_in p holds
for v, w being Element of Valuations_in A st ( for y being bound_QC-variable st x <> y holds
w . y = v . y ) holds
(Valid (p,J)) . v = (Valid (p,J)) . w

proof end;

theorem Th40: :: VALUAT_1:40

for A being non empty set
for x being bound_QC-variable
for v being Element of Valuations_in A
for p being Element of CQC-WFF
for J being interpretation of A st J,v |= p & not x in still_not-bound_in p holds
for w being Element of Valuations_in A st ( for y being bound_QC-variable st x <> y holds
w . y = v . y ) holds
J,w |= p

proof end;

theorem Th41: :: VALUAT_1:41

for A being non empty set
for x being bound_QC-variable
for v being Element of Valuations_in A
for p being Element of CQC-WFF
for J being interpretation of A holds
( J,v |= All (x,p) iff for w being Element of Valuations_in A st ( for y being bound_QC-variable st x <> y holds
w . y = v . y ) holds
J,w |= p )

proof end;

theorem Th42: :: VALUAT_1:42

for A being non empty set
for x, y being bound_QC-variable
for p, q being Element of CQC-WFF
for J being interpretation of A
for s9 being QC-formula st x <> y & p = s9 . x & q = s9 . y holds
for v being Element of Valuations_in A st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v

proof end;

theorem Th43: :: VALUAT_1:43

for x, y being bound_QC-variable
for s9 being QC-formula st x <> y & not x in still_not-bound_in s9 holds
not x in still_not-bound_in (s9 . y)

proof end;

theorem Th44: :: VALUAT_1:44

for A being non empty set
for v being Element of Valuations_in A
for J being interpretation of A holds J,v |= VERUM

proof end;

theorem Th45: :: VALUAT_1:45

for A being non empty set
for v being Element of Valuations_in A
for p, q being Element of CQC-WFF
for J being interpretation of A holds J,v |= (p '&' q) => (q '&' p)

proof end;

theorem Th46: :: VALUAT_1:46

for A being non empty set
for v being Element of Valuations_in A
for p being Element of CQC-WFF
for J being interpretation of A holds J,v |= (('not' p) => p) => p

proof end;

theorem Th47: :: VALUAT_1:47

for A being non empty set
for v being Element of Valuations_in A
for p, q being Element of CQC-WFF
for J being interpretation of A holds J,v |= p => (('not' p) => q)

proof end;

theorem Th48: :: VALUAT_1:48

for A being non empty set
for v being Element of Valuations_in A
for p, q, t being Element of CQC-WFF
for J being interpretation of A holds J,v |= (p => q) => (('not' (q '&' t)) => ('not' (p '&' t)))

proof end;

theorem :: VALUAT_1:49

for A being non empty set
for v being Element of Valuations_in A
for p, q being Element of CQC-WFF
for J being interpretation of A st J,v |= p & J,v |= p => q holds
J,v |= q by Th36;

theorem Th50: :: VALUAT_1:50

for A being non empty set
for x being bound_QC-variable
for v being Element of Valuations_in A
for p being Element of CQC-WFF
for J being interpretation of A holds J,v |= (All (x,p)) => p

proof end;

theorem :: VALUAT_1:51

for A being non empty set
for J being interpretation of A holds J |= VERUM

proof end;

theorem :: VALUAT_1:52

for A being non empty set
for p, q being Element of CQC-WFF
for J being interpretation of A holds J |= (p '&' q) => (q '&' p)

proof end;

theorem :: VALUAT_1:53

for A being non empty set
for p being Element of CQC-WFF
for J being interpretation of A holds J |= (('not' p) => p) => p

proof end;

theorem :: VALUAT_1:54

for A being non empty set
for p, q being Element of CQC-WFF
for J being interpretation of A holds J |= p => (('not' p) => q)

proof end;

theorem :: VALUAT_1:55

for A being non empty set
for p, q, t being Element of CQC-WFF
for J being interpretation of A holds J |= (p => q) => (('not' (q '&' t)) => ('not' (p '&' t)))

proof end;

theorem :: VALUAT_1:56

for A being non empty set
for p, q being Element of CQC-WFF
for J being interpretation of A st J |= p & J |= p => q holds
J |= q

proof end;

theorem :: VALUAT_1:57

for A being non empty set
for x being bound_QC-variable
for p being Element of CQC-WFF
for J being interpretation of A holds J |= (All (x,p)) => p

proof end;

theorem :: VALUAT_1:58

for A being non empty set
for x being bound_QC-variable
for p, q being Element of CQC-WFF
for J being interpretation of A st J |= p => q & not x in still_not-bound_in p holds
J |= p => (All (x,q))

proof end;

theorem :: VALUAT_1:59

for A being non empty set
for x, y being bound_QC-variable
for p, q being Element of CQC-WFF
for J being interpretation of A
for s being QC-formula st p = s . x & q = s . y & not x in still_not-bound_in s & J |= p holds
J |= q

proof end;