VALUAT_1: Interpretation and Satisfiability in the First Order Logic

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

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 ;

end;

:: deftheorem defines Valuations_in VALUAT_1:def 1 :

registration

let Al be QC-alphabet ;
let A be non empty set ;

cluster Valuations_in (Al,A) -> functional non empty ;

coherence ;

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

proof 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines FOR_ALL VALUAT_1:def 2 :

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

notation

let Al be QC-alphabet ;
let A be non empty set ;
let k be 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 Nat;
let ll be CQC-variable_list of k,Al;
let v be Element of Valuations_in (Al,A);

:: original: *'
redefine func v *' ll -> FinSequence of A means :Def3: :: VALUAT_1:def 3
( 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 Def3 defines *' VALUAT_1:def 3 :

definition

let Al be QC-alphabet ;
let A be non empty set ;
let k be Nat;
let ll be CQC-variable_list of k,Al;
let r be Element of relations_on A;

func ll '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

proof end;

uniqueness

proof end;

end;

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

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 func F . p -> Element of Funcs ((Valuations_in (Al,A)),BOOLEAN);
coherence

proof 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

proof end;

end;

:: deftheorem defines interpretation VALUAT_1:def 5 :

definition

let Al be QC-alphabet ;
let A be non empty set ;
let k be Nat;
let J be interpretation of Al,A;
let P be QC-pred_symbol of k,Al;
:: original: .
redefine func J . P -> Element of relations_on A;
coherence 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 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines Valid VALUAT_1:def 6 :

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

theorem :: VALUAT_1:6

for Al being QC-alphabet
for k being 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 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 end;

theorem Th8: :: VALUAT_1:8

proof 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 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 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 end;

theorem :: VALUAT_1:15

proof 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);

pred J,v |= p means :Def7: :: VALUAT_1:def 7
(Valid (p,J)) . v = TRUE ;

end;

:: deftheorem Def7 defines |= VALUAT_1:def 7 :

theorem :: VALUAT_1:16

for Al being QC-alphabet
for k being 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 ) by Lm1;

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 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 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 ) by Lm1;

theorem Th20: :: VALUAT_1:20

proof 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 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 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 end;

theorem Th24: :: VALUAT_1:24

proof end;

theorem Th25: :: VALUAT_1:25

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

pred J |= p means :: VALUAT_1:def 8
for v being Element of Valuations_in (Al,A) holds J,v |= p;

end;

:: deftheorem defines |= VALUAT_1:def 8 :

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

let Al be QC-alphabet ; :: thesis:
let A be non empty set ; :: thesis:
let Y, Z be bound_QC-variable of Al; :: thesis:
let V1, V2 be Element of Valuations_in (Al,A); :: thesis:
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:

proof

deffunc H₁( object ) -> Element of A = V2 . Z;
deffunc H₂( object ) -> set = V1 . $1;
defpred S₁[ object ] means for x1 being bound_QC-variable of Al st x1 = $1 holds
x1 <> Y;
A1: for x being object st x in bound_QC-variables Al holds
( ( S₁[x] implies H₂(x) in A ) & ( not S₁[x] implies H₁(x) in A ) ) by FUNCT_2:5;
consider f being Function of (bound_QC-variables Al),A such that
A2: for x being object st x in bound_QC-variables Al 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 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:

now :: thesis:

let x be bound_QC-variable of Al; :: thesis:

now :: thesis:

assume A3: x <> Y ; :: thesis:
( ( 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:

end;

hence ( x <> Y implies f . x = V1 . x ) ; :: thesis:
thus ( x = Y implies f . Y = V2 . Z ) by A2; :: thesis:

end;

hence ( ( for x being bound_QC-variable of Al st x <> Y holds
f . x = V1 . x ) & f . Y = V2 . Z ) ; :: thesis:

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 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 by Th27;

theorem Th29: :: VALUAT_1:29

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

proof 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 by Th32;

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) by Th33;

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 by Th34;

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) by Th35;

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))) by Th36;

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 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 by Th38;

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