Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

Interpretation and Satisfiability in the First Order Logic

by
Edmund Woronowicz

MML identifier: VALUAT_1
[ Mizar article, MML identifier index ]

```environ

vocabulary FUNCT_2, QC_LANG1, FRAENKEL, FUNCT_1, RELAT_1, MARGREL1, BOOLE,
ZF_LANG, CQC_LANG, FINSEQ_1, ARYTM_3, FUNCOP_1, ZF_MODEL, QC_LANG3,
CAT_1, VALUAT_1;
notation TARSKI, XBOOLE_0, SUBSET_1, XREAL_0, NAT_1, RELAT_1, FUNCT_1,
FUNCT_2, FINSEQ_1, FRAENKEL, QC_LANG1, QC_LANG3, CQC_LANG, MARGREL1;
constructors QC_LANG3, CQC_LANG, MARGREL1, XREAL_0, XCMPLX_0, MEMBERED,
XBOOLE_0;
clusters RELSET_1, MARGREL1, CQC_LANG, QC_LANG1, ARYTM_3, FINSEQ_1, FUNCT_1,
MEMBERED, ZFMISC_1, XBOOLE_0;
requirements NUMERALS, SUBSET, BOOLE;

begin

reserve i,j,k for Nat,
A,D for non empty set;

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

definition let A;
cluster Valuations_in A -> non empty functional;
end;

canceled;

theorem :: VALUAT_1:2
for x being set st x is Element of Valuations_in A holds
x is Function of bound_QC-variables ,A;

definition
let A;
redefine func Valuations_in A -> FUNCTION_DOMAIN of bound_QC-variables, A;
end;

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

definition
cluster boolean-valued Function;
end;

definition let f be boolean-valued Function, x be set;
cluster f.x -> boolean;
end;

definition let A be set;
cluster -> boolean-valued Element of Funcs(A,BOOLEAN);
end;

definition
let p be boolean-valued Function;
func 'not' p -> Function means
:: VALUAT_1:def 3
dom it = dom p &
for x being set st x in dom p holds it.x = 'not'(p.x);
let q be boolean-valued Function;
func p '&' q -> Function means
:: 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);
commutativity;
end;

definition
let p be boolean-valued Function;
cluster 'not' p -> boolean-valued;
let q be boolean-valued Function;
cluster p '&' q -> boolean-valued;
end;

reserve f1,f2 for Element of Funcs(Valuations_in A,BOOLEAN),
x,x1,y for bound_QC-variable,
v,v1 for Element of Valuations_in A;

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

definition
let A, x;
let p be Element of Funcs(Valuations_in A,BOOLEAN);
func FOR_ALL(x,p) -> Element of Funcs(Valuations_in A,BOOLEAN) means
:: VALUAT_1:def 7
for v holds
it.v = ALL{p.v' where v' is Element of Valuations_in A:
for y st x <> y holds v'.y = v.y};
end;

canceled 4;

theorem :: VALUAT_1:7
for p being Element of Funcs(Valuations_in A,BOOLEAN) holds
FOR_ALL(x,p).v = FALSE iff ex v1 st p.v1 = FALSE &
for y st x <> y holds v1.y = v.y;

theorem :: VALUAT_1:8
for p being Element of Funcs(Valuations_in A,BOOLEAN) holds
FOR_ALL(x,p).v = TRUE iff for v1 st for y st x <> y holds v1.y = v.y holds
p.v1 = TRUE;

reserve ll for CQC-variable_list of k;

definition
let A, k, ll, v;
redefine
func v*ll -> FinSequence of A means
:: VALUAT_1:def 8
len it = k & for i st 1 <= i & i <= k holds it.i = v.(ll.i);
synonym v*'ll;
end;

definition
let A, k, ll;
let r be Element of relations_on A;
func ll 'in' r -> Element of Funcs(Valuations_in A,BOOLEAN) means
:: 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);
end;

definition
let A;
let F be Function of CQC-WFF,Funcs(Valuations_in A, BOOLEAN);
let p be Element of CQC-WFF;
redefine func F.p -> Element of Funcs(Valuations_in A, BOOLEAN);
end;

definition
let D;
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),
r being Element of relations_on D st it.P = r holds
r = empty_rel(D) or the_arity_of P = the_arity_of r;
end;

reserve
p,q,s,t for Element of CQC-WFF,
J for interpretation of A,
P for QC-pred_symbol of k,
r for Element of relations_on A;

definition let A, k, J, P;
redefine func J.P -> Element of relations_on A;
end;

definition let A, J, p;
func Valid(p,J) -> Element of Funcs(Valuations_in A, BOOLEAN) means
:: 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,
x being bound_QC-variable, k being Nat,
ll being CQC-variable_list of k,
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));
end;

canceled 4;

theorem :: VALUAT_1:13
Valid(VERUM,J) = Valuations_in A --> TRUE;

theorem :: VALUAT_1:14
Valid(VERUM,J).v = TRUE;

theorem :: VALUAT_1:15
Valid(P!ll,J) = ll 'in' (J.P);

theorem :: VALUAT_1:16
p = P!ll & r = J.P implies (v*'ll in r iff Valid(p,J).v = TRUE);

theorem :: VALUAT_1:17
p = P!ll & r = J.P implies (not (v*'ll in r) iff Valid(p,J).v = FALSE);

canceled;

theorem :: VALUAT_1:19
Valid('not' p,J) = 'not' Valid(p,J);

theorem :: VALUAT_1:20
Valid('not' p,J).v = 'not'(Valid(p,J).v);

theorem :: VALUAT_1:21
Valid(p '&'q ,J) = Valid(p,J) '&' Valid(q,J);

theorem :: VALUAT_1:22
Valid(p '&'q ,J).v = (Valid(p,J).v) '&' (Valid(q,J).v);

theorem :: VALUAT_1:23
Valid(All(x,p),J) = FOR_ALL(x,Valid(p,J));

theorem :: VALUAT_1:24
Valid(p '&' 'not' p,J).v = FALSE;

theorem :: VALUAT_1:25
Valid('not'(p '&' 'not' p),J).v = TRUE;

definition
let A, p, J, v;
pred J,v |= p means
:: VALUAT_1:def 12
Valid(p,J).v = TRUE;
end;

canceled;

theorem :: VALUAT_1:27
J,v |= P!ll iff (ll 'in' (J.P)).v = TRUE;

theorem :: VALUAT_1:28
J,v |= 'not' p iff not J,v |= p;

theorem :: VALUAT_1:29
J,v |= (p '&' q) iff J,v |= p & J,v |= q;

theorem :: VALUAT_1:30
J,v |= All(x,p) iff FOR_ALL(x,Valid(p,J)).v = TRUE;

theorem :: VALUAT_1:31
J,v |= All(x,p) iff
for v1 st for y st x <> y holds v1.y = v.y holds Valid(p,J).v1 = TRUE;

theorem :: VALUAT_1:32
Valid('not' 'not' p,J) = Valid(p,J);

theorem :: VALUAT_1:33
Valid(p '&' p,J) = Valid(p,J);

canceled;

theorem :: VALUAT_1:35
J,v |= p => q iff
Valid(p, J).v = FALSE or Valid(q, J).v = TRUE;

theorem :: VALUAT_1:36
J,v |= p => q iff (J,v |= p implies J,v |= q);

theorem :: VALUAT_1:37
for p being Element of Funcs(Valuations_in A,BOOLEAN) holds
FOR_ALL(x,p).v = TRUE implies p.v = TRUE;

definition
let A, J, p;
pred J |= p means
:: VALUAT_1:def 13
for v holds J,v |= p;
end;

reserve u,w,z for Element of BOOLEAN;

reserve w,v2 for Element of Valuations_in A,
z for bound_QC-variable;

scheme Lambda_Val {A() -> non empty set, Y, Z() -> bound_QC-variable,
V1, V2() -> 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();

canceled;

theorem :: VALUAT_1:39

not x in still_not-bound_in p implies
for v,w st for y st x<>y holds w.y = v.y holds Valid(p,J).v = Valid(p,J).w;

theorem :: VALUAT_1:40

J,v |= p & not x in still_not-bound_in p implies
for w st for y st x<>y holds w.y = v.y holds J,w |= p;

theorem :: VALUAT_1:41

J,v |= All(x,p) iff
for w st for y st x<>y holds w.y = v.y holds J,w |= p;

reserve u,w for Element of Valuations_in A;
reserve s' for QC-formula;

theorem :: VALUAT_1:42

x <> y & p = s'.x & q = s'.y implies for v st v.x = v.y holds
Valid(p,J).v = Valid(q,J).v;

theorem :: VALUAT_1:43

x <> y & not x in still_not-bound_in s' implies
not x in still_not-bound_in (s'.y);

theorem :: VALUAT_1:44
J,v |= VERUM;

theorem :: VALUAT_1:45
J,v |= p '&' q => q '&' p;

theorem :: VALUAT_1:46
J,v |= ('not' p => p) => p;

theorem :: VALUAT_1:47
J,v |= p => ('not' p => q);

theorem :: VALUAT_1:48
J,v |= (p => q) => ('not'(q '&' t) => 'not'(p '&' t));

theorem :: VALUAT_1:49
J,v |= p & J,v |= (p => q) implies J,v |= q;

theorem :: VALUAT_1:50
J,v |= All(x,p) => p;

theorem :: VALUAT_1:51
J |= VERUM;

theorem :: VALUAT_1:52
J |= p '&' q => q '&' p;

theorem :: VALUAT_1:53
J |= ('not' p => p) => p;

theorem :: VALUAT_1:54
J |= p => ('not' p => q);

theorem :: VALUAT_1:55
J |= (p => q) => ('not'(q '&' t) => 'not'(p '&' t));

theorem :: VALUAT_1:56
J |= p & J |= (p => q) implies J |= q;

theorem :: VALUAT_1:57
J |= All(x,p) => p;

theorem :: VALUAT_1:58
(J |= p => q) & not x in still_not-bound_in p implies J |= p => All(x,q);

theorem :: VALUAT_1:59
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;
```