:: VALUAT_1 semantic presentation

definition

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

end;

:: deftheorem defines Valuations_in VALUAT_1:def 1 :

registration

let A be non empty set ;
cluster Valuations_in A -> non empty functional ;
coherence

proof end;

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

proof end;

end;

definition

let f be Function;
attr f is boolean-valued means :Def2: :: VALUAT_1:def 2
rng f c= BOOLEAN ;

end;

:: deftheorem Def2 defines boolean-valued VALUAT_1:def 2 :

registration

cluster boolean-valued set ;
existence

proof end;

end;

registration

let f be boolean-valued Function;
let x be set ;
cluster f . x -> boolean ;
coherence

proof end;

end;

registration

let A be set ;
cluster -> boolean-valued Element of Funcs A,BOOLEAN ;
coherence

proof end;

end;

definition

let p be boolean-valued Function;
func 'not' p -> Function means :Def3: :: VALUAT_1:def 3
( dom it = dom p & ( for x being set st x in dom p holds
it . x = 'not' (p . x) ) );
existence

proof end;

uniqueness

proof end;

let q be boolean-valued Function;
func p '&' q -> Function means :Def4: :: VALUAT_1:def 4
( dom it = (dom p) /\ (dom q) & ( for x being set st x in dom it holds
it . x = (p . x) '&' (q . x) ) );
existence

proof end;

uniqueness

proof end;

commutativity ;

end;

:: deftheorem Def3 defines 'not' VALUAT_1:def 3 :

:: deftheorem Def4 defines '&' VALUAT_1:def 4 :

registration

let p be boolean-valued Function;
cluster 'not' p -> boolean-valued ;
coherence

proof end;

let q be boolean-valued Function;
cluster p '&' q -> boolean-valued ;
coherence

proof end;

end;

definition

let A be non empty set ;
let p be Element of Funcs A,BOOLEAN ;
:: original: 'not'
redefine func 'not' p -> Element of Funcs A,BOOLEAN means :Def5: :: VALUAT_1:def 5
for x being Element of A holds it . x = 'not' (p . x);
coherence

proof end;

compatibility

proof end;

let q be Element of Funcs A,BOOLEAN ;
:: original: '&'
redefine func p '&' q -> Element of Funcs A,BOOLEAN means :Def6: :: VALUAT_1:def 6
for x being Element of A holds it . x = (p . x) '&' (q . x);
coherence

proof end;

compatibility

proof end;

end;

:: deftheorem Def5 defines 'not' VALUAT_1:def 5 :

:: deftheorem Def6 defines '&' VALUAT_1:def 6 :

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines FOR_ALL VALUAT_1:def 7 :

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 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 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

proof end;

compatibility

proof end;

end;

:: deftheorem Def8 defines *' VALUAT_1:def 8 :

definition

let A be non empty set ;
let k be 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines 'in' VALUAT_1:def 9 :

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

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

proof end;

end;

:: deftheorem defines interpretation VALUAT_1:def 10 :

definition

let A be non empty set ;
let k be 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 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 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

proof end;

end;

:: deftheorem Def11 defines Valid VALUAT_1:def 11 :

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 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:9

canceled;

theorem :: VALUAT_1:10

canceled;

theorem :: VALUAT_1:11

canceled;

theorem :: VALUAT_1:12

canceled;

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 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 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

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 :

theorem :: VALUAT_1:26

canceled;

theorem :: VALUAT_1:27

for k being 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 :

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;