:: Interpretation and Satisfiability in the First Order Logic
:: by Edmund Woronowicz
::
:: Received June 1, 1990
:: Copyright (c) 1990 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 . v') where v' is Element of Valuations_in A : for y being bound_QC-variable st x <> y holds
v' . 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 . v') where v' is Element of Valuations_in A : for y being bound_QC-variable st x <> y holds
v' . 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 . v') where v' is Element of Valuations_in A : for y being bound_QC-variable st x <> y holds
v' . y = v . y } ) & ( for v being Element of Valuations_in A holds b₂ . v = ALL { (p . v') where v' is Element of Valuations_in A : for y being bound_QC-variable st x <> y holds
v' . 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 . v') where v' is Element of Valuations_in A : for y being bound_QC-variable st x <> y holds
v' . 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 ;
:: 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 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 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 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 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 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 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 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
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
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 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;

scheme :: VALUAT_1:sch 1
LambdaVal{ F₁() -> non empty set , F₂() -> bound_QC-variable, F₃() -> bound_QC-variable, F₄() -> Element of Valuations_in F₁(), F₅() -> Element of Valuations_in F₁() } :

ex v being Element of Valuations_in F₁() st
( ( for x being bound_QC-variable st x <> F₂() holds
v . x = F₄() . x ) & v . F₂() = F₅() . F₃() )

proof end;

theorem :: VALUAT_1:38

canceled;

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 s' being QC-formula st x <> y & p = s' . x & q = s' . 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 s' being QC-formula st x <> y & not x in still_not-bound_in s' holds
not x in still_not-bound_in (s' . 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;