:: Interpretation and Satisfiability in the First Order Logic
:: by Edmund Woronowicz
::
:: Received June 1, 1990
:: Copyright (c) 1990-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies SUBSET_1, NUMBERS, XBOOLE_0, FUNCT_2, QC_LANG1, FUNCT_1, RELAT_1,
TARSKI, MARGREL1, XBOOLEAN, CQC_LANG, ARYTM_3, FINSEQ_1, NAT_1, XXREAL_0,
ZF_LANG, FUNCOP_1, REALSET1, BVFUNC_2, ZF_MODEL, ZF_LANG1, QC_LANG3,
CARD_1, CLASSES2, VALUAT_1, FUNCT_7;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, RELAT_1, FUNCT_1,
FUNCT_2, FUNCT_7, NAT_1, FINSEQ_1, FUNCOP_1, QC_LANG1, QC_LANG3,
CQC_LANG, MARGREL1, XXREAL_0;
constructors XXREAL_0, MEMBERED, MARGREL1, QC_LANG3, CQC_LANG, FUNCOP_1,
RELSET_1, FUNCT_7, NUMBERS;
registrations XBOOLE_0, FUNCT_1, RELSET_1, MARGREL1, QC_LANG1, CQC_LANG,
XXREAL_0, FUNCT_2, ORDINAL1;
requirements NUMERALS, SUBSET, BOOLE;
begin
reserve Al for QC-alphabet;
reserve i,j,k for Nat,
A,D for non empty set;
definition
let Al;
let A be set;
func Valuations_in(Al,A) -> set equals
:: VALUAT_1:def 1
Funcs(bound_QC-variables(Al), A);
end;
registration
let Al,A;
cluster Valuations_in(Al,A) -> non empty functional;
end;
theorem :: VALUAT_1:1
for x being set st x is Element of Valuations_in(Al,A) holds x is
Function of bound_QC-variables(Al) ,A;
definition
let Al,A;
redefine func Valuations_in(Al,A) ->
FUNCTION_DOMAIN of bound_QC-variables(Al), A;
end;
reserve f1,f2 for Element of Funcs(Valuations_in(Al,A),BOOLEAN),
x,x1,y for bound_QC-variable of Al,
v,v1 for Element of Valuations_in(Al,A);
definition
let Al, A, x;
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
:: VALUAT_1:def 2
for v holds it.v =
ALL{p.v9 where v9 is Element of Valuations_in(Al,A) :
for y st x <> y holds v9.y = v.y};
end;
theorem :: VALUAT_1:2
for p being Element of Funcs(Valuations_in(Al,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:3
for p being Element of Funcs(Valuations_in(Al,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,Al;
notation
let Al, A, k, ll, v;
synonym v*'ll for v*ll;
end;
definition
let Al;
let A, k, ll, v;
redefine func v*'ll -> FinSequence of A means
:: VALUAT_1:def 3
len it = k & for i be Nat st
1 <= i & i <= k holds it.i = v.(ll.i);
end;
definition
let Al;
let A, k, ll;
let r be Element of relations_on A;
func ll 'in' r -> Element of Funcs(Valuations_in(Al,A),BOOLEAN) means
:: VALUAT_1:def 4
for
v being Element of Valuations_in(Al,A) holds
(v*'ll in r iff it.v = TRUE) & (not v*'ll in r iff it.v = FALSE);
end;
definition
let Al, A;
let F be Function of CQC-WFF(Al),Funcs(Valuations_in(Al,A), BOOLEAN);
let p be Element of CQC-WFF(Al);
redefine func F.p -> Element of Funcs(Valuations_in(Al,A), BOOLEAN);
end;
definition
let Al, D;
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)),
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(Al),
J for interpretation of Al,A,
P for QC-pred_symbol of k,Al,
r for Element of relations_on A;
definition
let Al, A, k, J, P;
redefine func J.P -> Element of relations_on A;
end;
definition
let Al, A, J, p;
func Valid(p,J) -> Element of Funcs(Valuations_in(Al,A), BOOLEAN) means
:: 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), x being bound_QC-variable of Al,
k being Nat, ll being CQC-variable_list of k,Al, 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));
end;
theorem :: VALUAT_1:4
Valid(VERUM(Al),J) = Valuations_in(Al,A) --> TRUE;
theorem :: VALUAT_1:5
Valid(VERUM(Al),J).v = TRUE;
theorem :: VALUAT_1:6
Valid(P!ll,J) = ll 'in' (J.P);
theorem :: VALUAT_1:7
p = P!ll & r = J.P implies (v*'ll in r iff Valid(p,J).v = TRUE);
theorem :: VALUAT_1:8
p = P!ll & r = J.P implies (not v*'ll in r iff Valid(p,J).v = FALSE);
theorem :: VALUAT_1:9
Valid('not' p,J) = 'not' Valid(p,J);
theorem :: VALUAT_1:10
Valid('not' p,J).v = 'not'(Valid(p,J).v);
theorem :: VALUAT_1:11
Valid(p '&'q,J) = Valid(p,J) '&' Valid(q,J);
theorem :: VALUAT_1:12
Valid(p '&'q,J).v = (Valid(p,J).v) '&' (Valid(q,J).v);
theorem :: VALUAT_1:13
Valid(All(x,p),J) = FOR_ALL(x,Valid(p,J));
theorem :: VALUAT_1:14
Valid(p '&' 'not' p,J).v = FALSE;
theorem :: VALUAT_1:15
Valid('not'(p '&' 'not' p),J).v = TRUE;
definition
let Al, A, p, J, v;
pred J,v |= p means
:: VALUAT_1:def 7
Valid(p,J).v = TRUE;
end;
theorem :: VALUAT_1:16
J,v |= P!ll iff (ll 'in' (J.P)).v = TRUE;
theorem :: VALUAT_1:17
J,v |= 'not' p iff not J,v |= p;
theorem :: VALUAT_1:18
J,v |= (p '&' q) iff J,v |= p & J,v |= q;
theorem :: VALUAT_1:19
J,v |= All(x,p) iff FOR_ALL(x,Valid(p,J)).v = TRUE;
theorem :: VALUAT_1:20
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:21
Valid('not' 'not' p,J) = Valid(p,J);
theorem :: VALUAT_1:22
Valid(p '&' p,J) = Valid(p,J);
theorem :: VALUAT_1:23
J,v |= p => q iff Valid(p, J).v = FALSE or Valid(q, J).v = TRUE;
theorem :: VALUAT_1:24
J,v |= p => q iff (J,v |= p implies J,v |= q);
theorem :: VALUAT_1:25
for p being Element of Funcs(Valuations_in(Al,A),BOOLEAN) holds
FOR_ALL(x,p).v = TRUE implies p.v = TRUE;
definition
let Al, A, J, p;
pred J |= p means
:: VALUAT_1:def 8
for v holds J,v |= p;
end;
reserve u,w,z for Element of BOOLEAN;
reserve w,v2 for Element of Valuations_in(Al,A),
z for bound_QC-variable of Al;
theorem :: VALUAT_1:26
for A be non empty set, Y, Z be bound_QC-variable of Al,
V1, V2 be 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;
theorem :: VALUAT_1:27
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:28
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:29
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(Al,A);
reserve s9 for QC-formula of Al;
theorem :: VALUAT_1:30
x <> y & p = s9.x & q = s9.y implies for v st v.x = v.y holds
Valid(p,J).v = Valid(q,J).v;
theorem :: VALUAT_1:31
x <> y & not x in still_not-bound_in s9 implies not x in
still_not-bound_in (s9.y);
theorem :: VALUAT_1:32
J,v |= VERUM(Al);
theorem :: VALUAT_1:33
J,v |= p '&' q => q '&' p;
theorem :: VALUAT_1:34
J,v |= ('not' p => p) => p;
theorem :: VALUAT_1:35
J,v |= p => ('not' p => q);
theorem :: VALUAT_1:36
J,v |= (p => q) => ('not'(q '&' t) => 'not'(p '&' t));
theorem :: VALUAT_1:37
J,v |= p & J,v |= (p => q) implies J,v |= q;
theorem :: VALUAT_1:38
J,v |= All(x,p) => p;
theorem :: VALUAT_1:39
J |= VERUM(Al);
theorem :: VALUAT_1:40
J |= p '&' q => q '&' p;
theorem :: VALUAT_1:41
J |= ('not' p => p) => p;
theorem :: VALUAT_1:42
J |= p => ('not' p => q);
theorem :: VALUAT_1:43
J |= (p => q) => ('not'(q '&' t) => 'not'(p '&' t));
theorem :: VALUAT_1:44
J |= p & J |= (p => q) implies J |= q;
theorem :: VALUAT_1:45
J |= All(x,p) => p;
theorem :: VALUAT_1:46
J |= p => q & not x in still_not-bound_in p implies J |= p => All(x,q);
theorem :: VALUAT_1:47
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;