Volume 2, 1990

University of Bialystok

Copyright (c) 1990 Association of Mizar Users

### The abstract of the Mizar article:

### Interpretation and Satisfiability in the First Order Logic

**by****Edmund Woronowicz**- Received June 1, 1990
- 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;

Back to top