:: Interpretation and Satisfiability in the First Order Logic
:: by Edmund Woronowicz
::
:: Received June 1, 1990
:: Copyright (c) 1990-2026 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;
equalities XBOOLEAN;
theorems TARSKI, FINSEQ_1, FUNCT_1, FUNCT_2, FUNCOP_1, QC_LANG1, QC_LANG2,
QC_LANG3, CQC_LANG, MARGREL1, RELSET_1, RELAT_1, FINSEQ_3, XBOOLE_0,
XBOOLE_1, XBOOLEAN, ORDINAL1, CARD_1, SUBSET_1;
schemes QC_LANG1, CQC_LANG, FUNCT_2;
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
Funcs(bound_QC-variables(Al), A);
coherence;
end;
registration
let Al,A;
cluster Valuations_in(Al,A) -> non empty functional;
coherence;
end;
theorem Th1:
for x being set st x is Element of Valuations_in(Al,A) holds x is
Function of bound_QC-variables(Al) ,A
proof
let x be set;
assume x is Element of Valuations_in(Al,A);
then ex f being Function st x = f & dom f = bound_QC-variables(Al)
& rng f c= A by FUNCT_2:def 2;
hence thesis by FUNCT_2:def 1,RELSET_1:4;
end;
definition
let Al,A;
redefine func Valuations_in(Al,A) -> :: redefines Valuations_in (VALUAT_1, definition)
FUNCTION_DOMAIN of bound_QC-variables(Al), A;
coherence
proof
for x be Element of Valuations_in(Al,A) holds x is Function of
bound_QC-variables(Al) ,A by Th1;
hence thesis by FUNCT_2:def 12;
end;
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
:Def2:
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};
existence
proof
deffunc F(Function) =
ALL{p.v9 where v9 is Element of Valuations_in(Al,A):
for y st x <> y holds v9.y = $1.y};
consider f being Function of Valuations_in(Al,A), BOOLEAN such that
A1: for v holds f.v = F(v) from FUNCT_2:sch 4;
dom f = Valuations_in(Al,A) &
rng f c= BOOLEAN by FUNCT_2:def 1,RELAT_1:def 19;
then reconsider f as Element of Funcs(Valuations_in(Al,A),BOOLEAN) by
FUNCT_2:def 2;
take f;
thus thesis by A1;
end;
uniqueness
proof
let f1,f2;
assume that
A2: for v holds f1.v = ALL{p.v9 where v9 is Element of Valuations_in(Al,A)
: for y st x <> y holds v9.y = v.y} and
A3: for v holds f2.v = ALL{p.v9 where v9 is Element of Valuations_in(Al,A)
: for y st x <> y holds v9.y = v.y};
for v holds f1.v = f2.v
proof
let v;
f1.v = ALL{p.v9 where v9 is Element of Valuations_in(Al,A): for y st x
<> y holds v9.y = v.y} by A2;
hence thesis by A3;
end;
hence thesis by FUNCT_2:63;
end;
end;
theorem Th2:
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
proof
let p be Element of Funcs(Valuations_in(Al,A),BOOLEAN);
A1: now
assume ex v1 st p.v1 = FALSE & for y st x <> y holds v1.y = v.y;
then
FALSE in {p.v99 where v99 is Element of Valuations_in(Al,A): for y st x <>
y holds v99.y = v.y};
then ALL{p.v99 where v99 is Element of Valuations_in(Al,A): for y st x <> y
holds v99.y = v.y} = FALSE by MARGREL1:17;
hence FOR_ALL(x,p).v = FALSE by Def2;
end;
now
assume FOR_ALL(x,p).v = FALSE;
then ALL{p.v99 where v99 is Element of Valuations_in(Al,A): for y st x <> y
holds v99.y = v.y} = FALSE by Def2;
then
FALSE in {p.v99 where v99 is Element of Valuations_in(Al,A): for y st x <>
y holds v99.y = v.y} by MARGREL1:17;
hence ex v1 st p.v1 = FALSE & for y st x <> y holds v1.y = v.y;
end;
hence thesis by A1;
end;
theorem Th3:
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
proof
let p be Element of Funcs(Valuations_in(Al,A),BOOLEAN);
A1: now
assume FOR_ALL(x,p).v = TRUE;
then ALL{p.v99 where v99 is Element of Valuations_in(Al,A): for y st x <> y
holds v99.y = v.y} = TRUE by Def2;
then
A2: not FALSE in {p.v99 where v99 is Element of Valuations_in(Al,A): for y st
x <> y holds v99.y = v.y} by MARGREL1:17;
thus for v1 st for y st x <> y holds v1.y = v.y holds p.v1 = TRUE
proof
let v1;
assume for y st x <> y holds v1.y = v.y;
then not p.v1 = FALSE by A2;
hence thesis by XBOOLEAN:def 3;
end;
end;
now
assume for v1 st for y st x <> y holds v1.y = v.y holds p.v1 = TRUE;
then not ex v1 st p.v1 = FALSE & for y st x <> y holds v1.y = v.y;
then
not FALSE in {p.v99 where v99 is Element of Valuations_in(Al,A): for y st
x <> y holds v99.y = v.y};
then ALL{p.v99 where v99 is Element of Valuations_in(Al,A): for y st x <> y
holds v99.y = v.y} = TRUE by MARGREL1:17;
hence FOR_ALL(x,p).v = TRUE by Def2;
end;
hence thesis by A1;
end;
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 :: redefines *' (VALUAT_1, synonym) → * (FUNCT_1, synonym) → * (RELAT_1, synonym) → (#) (RELAT_1, definition)
:Def3:
len it = k & for i be Nat st
1 <= i & i <= k holds it.i = v.(ll.i);
coherence
proof
rng v c= A & rng(v*ll) c= rng v by RELAT_1:26,def 19;
then
A1: rng( v*ll) c= A by XBOOLE_1:1;
A2: len ll = k by CARD_1:def 7;
dom v = bound_QC-variables(Al) by FUNCT_2:def 1;
then rng ll c= dom v by RELAT_1:def 19;
then dom(v*ll) = dom ll by RELAT_1:27
.= Seg k by A2,FINSEQ_1:def 3;
then v*ll is FinSequence-like by FINSEQ_1:def 2;
hence thesis by A1,FINSEQ_1:def 4;
end;
compatibility
proof
let IT be FinSequence of A;
A3: len ll = k by CARD_1:def 7;
dom v = bound_QC-variables(Al) by FUNCT_2:def 1;
then
A4: rng ll c= dom v by RELAT_1:def 19;
thus IT = v*ll implies len IT = k & for i be Nat
st 1 <= i & i <= k holds IT.i = v.(ll.i)
proof
assume
A5: IT = v*ll;
then
A6: dom ll = dom IT by A4,RELAT_1:27;
hence len IT = k by A3,FINSEQ_3:29;
let i be Nat;
assume 1 <= i & i <= k;
then i in dom IT by A3,A6,FINSEQ_3:25;
hence thesis by A5,FUNCT_1:12;
end;
assume that
A7: len IT = k and
A8: for i be Nat st 1 <= i & i <= k holds IT.i = v.(ll.i);
A9: for x being object holds x in dom IT iff x in dom ll & ll.x in dom v
proof
let x be object;
thus x in dom IT implies x in dom ll & ll.x in dom v
proof
assume x in dom IT;
hence x in dom ll by A3,A7,FINSEQ_3:29;
then ll.x in rng ll by FUNCT_1:def 3;
hence thesis by A4;
end;
assume that
A10: x in dom ll and
ll.x in dom v;
thus thesis by A3,A7,A10,FINSEQ_3:29;
end;
for x being object st x in dom IT holds IT.x = v.(ll.x)
proof
let x be object;
assume
A11: x in dom IT;
then reconsider i = x as Element of NAT;
1 <= i & i <= k by A7,A11,FINSEQ_3:25;
hence thesis by A8;
end;
hence thesis by A9,FUNCT_1:10;
end;
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
:Def4:
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);
existence
proof
defpred C[object] means ex v being Element of Valuations_in(Al,A)
st $1 = v & v*' ll in r;
deffunc T(object) = TRUE;
deffunc F(object) = FALSE;
A1: for x being object st x in Valuations_in(Al,A) holds (C[x] implies T(x) in
BOOLEAN) & (not C[x] implies F(x) in BOOLEAN);
consider f being Function of Valuations_in(Al,A), BOOLEAN such that
A2: for x being object st x in Valuations_in(Al,A) holds (C[x] implies f.x =
T(x)) & (not C[x] implies f.x = F(x)) from FUNCT_2:sch 5(A1);
dom f = Valuations_in(Al,A) &
rng f c= BOOLEAN by FUNCT_2:def 1,RELAT_1:def 19;
then reconsider f as Element of Funcs(Valuations_in(Al,A),BOOLEAN) by
FUNCT_2:def 2;
take f;
let v be Element of Valuations_in(Al,A);
not (ex v9 being Element of Valuations_in(Al,A) st v = v9 & v9*'ll in r)
implies f.v = FALSE by A2;
hence thesis by A2;
end;
uniqueness
proof
let f1,f2 be Element of Funcs(Valuations_in(Al,A),BOOLEAN);
assume that
A3: for v being Element of Valuations_in(Al,A) holds (v*'ll in r iff
f1.v = TRUE) & (not v*'ll in r iff f1.v = FALSE) and
A4: for v being Element of Valuations_in(Al,A) holds (v*'ll in r iff
f2.v = TRUE) & (not v*'ll in r iff f2.v = FALSE);
for v being Element of Valuations_in(Al,A) holds f1.v = f2.v
proof
let v be Element of Valuations_in(Al,A);
per cases;
suppose
A5: v*'ll in r;
then f1.v = TRUE by A3;
hence thesis by A4,A5;
end;
suppose
A6: not v*'ll in r;
then f1.v = FALSE by A3;
hence thesis by A4,A6;
end;
end;
hence thesis by FUNCT_2:63;
end;
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); :: redefines . (FUNCT_1, definition)
coherence
proof
thus F.p is Element of Funcs(Valuations_in(Al,A), BOOLEAN);
end;
end;
definition
let Al, D;
mode interpretation of Al,D -> Function of QC-pred_symbols(Al),
relations_on D
means
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;
existence
proof
reconsider F1 = QC-pred_symbols(Al) --> empty_rel(D) as Function of
QC-pred_symbols(Al), relations_on D;
take F1;
let P be Element of QC-pred_symbols(Al);
thus thesis by FUNCOP_1:7;
end;
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; :: redefines . (FUNCT_1, definition)
coherence by FUNCT_2:5;
end;
definition
let Al, A, J, p;
func Valid(p,J) -> Element of Funcs(Valuations_in(Al,A), BOOLEAN) means
:Def6:
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));
existence
proof
deffunc A(Nat, QC-pred_symbol of $1, Al,
CQC-variable_list of $1,Al) = $3 'in' (J.$2);
set D = Funcs(Valuations_in(Al,A), BOOLEAN);
set V = In(Valuations_in(Al,A) --> TRUE,D);
deffunc N(Element of D) = In('not' $1,D);
deffunc C(Element of D, Element of D) = In($1 '&' $2,D);
deffunc Q(bound_QC-variable of Al, Element of D) = In(FOR_ALL($1,$2),D);
consider F being Function of CQC-WFF(Al),D such that
A1: F.VERUM(Al) = V and
A2: for r,s being (Element of CQC-WFF(Al)),
x being bound_QC-variable of Al, k being Nat
for l being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al
holds F.(P!l) = A(k,P,l) & F.('not' r) = N(F.r)
& F.(r '&' s) = C(F.r,F.s) & F.All(x,r) = Q(x,F.r)
from CQC_LANG:sch 2;
take F.p, F;
thus F.p = F.p;
Valuations_in(Al,A) --> TRUE in D by FUNCT_2:8;
hence F.VERUM(Al) = Valuations_in(Al,A) --> TRUE by A1,SUBSET_1:def 8;
let p,q be Element of CQC-WFF(Al), x be bound_QC-variable of Al,
k be Nat, ll be CQC-variable_list of k,Al,
P be QC-pred_symbol of k,Al;
thus F.(P!ll) = (ll 'in' (J.P)) by A2;
A3: 'not'(F.p) in D by FUNCT_2:8;
thus F.('not' p) = N(F.p) by A2
.= 'not'(F.p) by A3,SUBSET_1:def 8;
A4: (F.p) '&' (F.q) in D by FUNCT_2:8;
thus F.(p '&' q) = C(F.p,F.q) by A2
.= (F.p) '&' (F.q) by A4,SUBSET_1:def 8;
thus F.All(x,p) = Q(x,F.p) by A2
.= FOR_ALL(x,F.p) by SUBSET_1:def 8;
end;
uniqueness
proof
deffunc A(Nat, QC-pred_symbol of $1, Al,
CQC-variable_list of $1,Al) = $3 'in' (J.$2);
set D = Funcs(Valuations_in(Al,A), BOOLEAN);
set V = In(Valuations_in(Al,A) --> TRUE,D);
deffunc N(Element of D) = In('not' $1,D);
deffunc C(Element of D, Element of D) = In($1 '&' $2,D);
deffunc Q(bound_QC-variable of Al, Element of D) = In(FOR_ALL($1,$2),D);
let d1,d2 be Element of D;
given F1 being Function of CQC-WFF(Al), D such that
A5: d1 = F1.p and
A6: F1.VERUM(Al) = Valuations_in(Al,A) --> TRUE and
A7: for r,s being (Element of CQC-WFF(Al)),
x being bound_QC-variable of Al, k being Nat
for l being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al
holds F1.(P!l) = A(k,P,l) & F1.('not' r) = 'not' (F1.r) &
F1.(r '&' s) = F1.r '&' F1.s & F1.All(x,r) = FOR_ALL(x,F1.r);
A8: now
thus F1.VERUM(Al) = V by A6,SUBSET_1:def 8;
let r,s be (Element of CQC-WFF(Al)),x be bound_QC-variable of Al,
k be Nat, l be CQC-variable_list of k,Al,
P be QC-pred_symbol of k,Al;
thus F1.(P!l) = A(k,P,l) by A7;
A9: 'not' (F1.r) in D by FUNCT_2:8;
thus F1.('not' r) = 'not' (F1.r) by A7
.= N(F1.r) by A9,SUBSET_1:def 8;
A10: F1.r '&' F1.s in D by FUNCT_2:8;
thus F1.(r '&' s) = F1.r '&' F1.s by A7
.= C(F1.r,F1.s) by A10,SUBSET_1:def 8;
thus F1.All(x,r) = FOR_ALL(x,F1.r) by A7
.= Q(x,F1.r) by SUBSET_1:def 8;
end;
given F2 being Function of CQC-WFF(Al), D such that
A11: d2 = F2.p and
A12: F2.VERUM(Al) = Valuations_in(Al,A) --> TRUE and
A13: for r,s being Element of CQC-WFF(Al) ,
x being bound_QC-variable of Al, k being Nat
for l being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al
holds F2.(P!l) = A(k,P,l) & F2.('not' r) = 'not' (F2.r) &
F2.(r '&' s) = F2.r '&' F2.s & F2.All(x,r)= FOR_ALL(x,F2.r);
A14: now
thus F2.VERUM(Al) = V by A12,SUBSET_1:def 8;
let r,s be (Element of CQC-WFF(Al)),x be bound_QC-variable of Al,
k be Nat, l be CQC-variable_list of k,Al,
P be QC-pred_symbol of k,Al;
thus F2.(P!l) = A(k,P,l) by A13;
A15: 'not' (F2.r) in D by FUNCT_2:8;
thus F2.('not' r) = 'not' (F2.r) by A13
.= N(F2.r) by A15,SUBSET_1:def 8;
A16: F2.r '&' F2.s in D by FUNCT_2:8;
thus F2.(r '&' s) = F2.r '&' F2.s by A13
.= C(F2.r,F2.s) by A16,SUBSET_1:def 8;
thus F2.All(x,r) = FOR_ALL(x,F2.r) by A13
.= Q(x,F2.r) by SUBSET_1:def 8;
end;
F1 = F2 from CQC_LANG:sch 3(A8,A14);
hence thesis by A5,A11;
end;
end;
Lm1: for A, J holds Valid(VERUM(Al),J) = (Valuations_in(Al,A) --> TRUE) &
(for k, ll,P holds Valid(P!ll,J) = ll 'in' (J.P)) &
(for p holds Valid('not' p,J) = 'not' Valid(p,J)) &
(for q holds Valid(p '&' q,J) = Valid(p,J) '&' Valid(q,J)) & for
x holds Valid(All(x,p),J) = FOR_ALL(x,Valid(p,J))
proof
let A, J;
set D = Funcs(Valuations_in(Al,A), BOOLEAN);
set V = In(Valuations_in(Al,A) --> TRUE,D);
deffunc A(Nat, QC-pred_symbol of $1, Al,
CQC-variable_list of $1,Al) = $3 'in' (J.$2);
deffunc N(Element of D) = In('not' $1,D);
deffunc C(Element of D, Element of D) = In($1 '&' $2,D);
deffunc Q(bound_QC-variable of Al, Element of D) = In(FOR_ALL($1,$2),D);
deffunc X(Element of CQC-WFF(Al)) = Valid($1, J);
A1: for p holds for d be Element of D holds d = (X(p)) iff ex F being
Function of CQC-WFF(Al), D st d = F.p & F.VERUM(Al) = V &
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) = A(k, P, ll) &
F.('not' p) = N(F.p) & (F.(p '&' q)) = C(F.p,F.q) & F.(All(x,p)) = Q(x,F.p)
proof let p; let d be Element of D;
thus d = (X(p)) implies ex F being
Function of CQC-WFF(Al), D st d = F.p & F.VERUM(Al) = V &
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) = A(k, P, ll) &
F.('not' p) = N(F.p) & (F.(p '&' q)) = C(F.p,F.q) & F.(All(x,p)) = Q(x,F.p)
proof assume
d = X(p);
then consider F being
Function of CQC-WFF(Al),Funcs(Valuations_in(Al,A), BOOLEAN) such that
A2: d = F.p and
A3: F.VERUM(Al) = (Valuations_in(Al,A) --> TRUE) and
A4: 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)) by Def6;
take F;
thus d = F.p by A2;
thus F.VERUM(Al) = V by A3,SUBSET_1:def 8;
let p,q be Element of CQC-WFF(Al), x be bound_QC-variable of Al,
k be Nat, ll be CQC-variable_list of k,Al,
P be QC-pred_symbol of k,Al;
thus F.(P!ll) = A(k, P, ll) by A4;
A5: 'not' (F.p) in D by FUNCT_2:8;
thus F.('not' p) = 'not' (F.p) by A4
.= N(F.p) by A5,SUBSET_1:def 8;
A6: (F.p) '&' (F.q) in D by FUNCT_2:8;
thus (F.(p '&' q)) = (F.p) '&' (F.q) by A4
.= C(F.p,F.q) by A6,SUBSET_1:def 8;
thus F.(All(x,p)) = FOR_ALL(x,F.p) by A4
.= Q(x,F.p) by SUBSET_1:def 8;
end;
given F being Function of CQC-WFF(Al), D such that
A7: d = F.p and
A8: F.VERUM(Al) = V and
A9: 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) = A(k, P, ll) &
F.('not' p) = N(F.p) & (F.(p '&' q)) = C(F.p,F.q) & F.(All(x,p)) = Q(x,F.p);
Valuations_in(Al,A) --> TRUE in D by FUNCT_2:8;
then
A10: F.VERUM(Al) = Valuations_in(Al,A) --> TRUE by A8,SUBSET_1:def 8;
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) = A(k, P, ll) &
F.('not' p) = 'not' (F.p) &
F.(p '&' q) = (F.p) '&' (F.q) &
F.All(x,p) = FOR_ALL(x,F.p)
proof let p,q being Element of CQC-WFF(Al), x be bound_QC-variable of Al,
k be Nat, ll be CQC-variable_list of k,Al,
P be QC-pred_symbol of k,Al;
thus F.(P!ll) = A(k, P, ll) by A9;
A11: 'not' (F.p) in D by FUNCT_2:8;
thus F.('not' p) = N(F.p) by A9
.= 'not' (F.p) by A11,SUBSET_1:def 8;
A12: (F.p) '&' (F.q) in D by FUNCT_2:8;
thus F.(p '&' q) = C(F.p,F.q) by A9
.= (F.p) '&' (F.q) by A12,SUBSET_1:def 8;
thus F.All(x,p) = Q(x,F.p) by A9
.= FOR_ALL(x,F.p) by SUBSET_1:def 8;
end;
hence d = X(p) by A7,A10,Def6;
end;
A13: Valuations_in(Al,A) --> TRUE in D by FUNCT_2:8;
X(VERUM(Al)) = V from CQC_LANG:sch 5(A1);
hence X(VERUM(Al)) = Valuations_in(Al,A) --> TRUE by A13,SUBSET_1:def 8;
hereby
let k, ll, P;
thus X(P!ll) = A(k,P,ll) from CQC_LANG:sch 6(A1);
end;
hereby
let p;
A14: 'not' X(p) in D by FUNCT_2:8;
X('not' p) = N(X(p)) from CQC_LANG:sch 7(A1);
hence X('not' p) = 'not' X(p) by A14,SUBSET_1:def 8;
end;
hereby
let q;
A15: X(p) '&' X(q) in D by FUNCT_2:8;
X(p '&' q) = C(X(p), X(q)) from CQC_LANG:sch 8(A1);
hence X(p '&' q) = X(p) '&' X(q) by A15,SUBSET_1:def 8;
end;
let x;
X(All(x,p)) = Q(x,X(p)) from CQC_LANG:sch 9(A1);
hence X(All(x,p)) = FOR_ALL(x,X(p)) by SUBSET_1:def 8;
end;
theorem
Valid(VERUM(Al),J) = Valuations_in(Al,A) --> TRUE by Lm1;
theorem Th5:
Valid(VERUM(Al),J).v = TRUE
proof
(Valuations_in(Al,A) --> TRUE).v = TRUE by FUNCOP_1:7;
hence thesis by Lm1;
end;
theorem
Valid(P!ll,J) = ll 'in' (J.P) by Lm1;
theorem Th7:
p = P!ll & r = J.P implies (v*'ll in r iff Valid(p,J).v = TRUE)
proof
assume that
A1: p = P!ll and
A2: r = J.P;
A3: now
assume Valid(p,J).v = TRUE;
then (ll 'in' (J.P)).v <> FALSE by A1,Lm1;
hence v*'ll in r by A2,Def4;
end;
now
assume v*'ll in r;
then (ll 'in' (J.P)).v = TRUE by A2,Def4;
hence Valid(p,J).v = TRUE by A1,Lm1;
end;
hence thesis by A3;
end;
theorem Th8:
p = P!ll & r = J.P implies (not v*'ll in r iff Valid(p,J).v = FALSE)
proof
assume that
A1: p = P!ll and
A2: r = J.P;
A3: now
assume Valid(p,J).v = FALSE;
then (ll 'in' (J.P)).v <> TRUE by A1,Lm1;
hence not v*'ll in r by A2,Def4;
end;
now
assume not v*'ll in r;
then (ll 'in' (J.P)).v = FALSE by A2,Def4;
hence Valid(p,J).v = FALSE by A1,Lm1;
end;
hence thesis by A3;
end;
theorem
Valid('not' p,J) = 'not' Valid(p,J) by Lm1;
theorem Th10:
Valid('not' p,J).v = 'not'(Valid(p,J).v)
proof
Valid('not' p,J).v = ('not' Valid(p,J)).v by Lm1;
hence thesis by MARGREL1:def 19;
end;
theorem
Valid(p '&'q,J) = Valid(p,J) '&' Valid(q,J) by Lm1;
theorem Th12:
Valid(p '&'q,J).v = (Valid(p,J).v) '&' (Valid(q,J).v)
proof
Valid(p '&'q,J).v = (Valid(p,J) '&' Valid(q,J)).v by Lm1;
hence thesis by MARGREL1:def 20;
end;
theorem
Valid(All(x,p),J) = FOR_ALL(x,Valid(p,J)) by Lm1;
theorem Th14:
Valid(p '&' 'not' p,J).v = FALSE
proof
A1: now
assume (Valid(p,J)).v = TRUE;
then 'not'(Valid(p,J).v) = FALSE by MARGREL1:11;
hence (Valid(p,J).v) '&' 'not'(Valid(p,J).v) = FALSE by MARGREL1:12;
end;
A2: Valid(p,J).v = FALSE implies (Valid(p,J).v) '&' 'not' (Valid(p,J).v) =
FALSE by MARGREL1:12;
Valid(p '&' 'not' p,J).v = (Valid(p,J).v) '&' (Valid('not' p,J).v) by Th12
.= (Valid(p,J).v) '&' 'not'(Valid(p,J).v) by Th10;
hence thesis by A1,A2,XBOOLEAN:def 3;
end;
theorem
Valid('not'(p '&' 'not' p),J).v = TRUE
proof
Valid('not'(p '&' 'not' p),J).v = 'not'(Valid(p '&' 'not' p,J).v) by Th10
.= 'not' FALSE by Th14;
hence thesis by MARGREL1:11;
end;
definition
let Al, A, p, J, v;
pred J,v |= p means
:Def7:
Valid(p,J).v = TRUE;
end;
theorem
J,v |= P!ll iff (ll 'in' (J.P)).v = TRUE
by Lm1;
theorem
J,v |= 'not' p iff not J,v |= p
proof
A1: now
assume not J,v |= p;
then not Valid(p,J).v = TRUE;
then Valid(p,J).v = FALSE by XBOOLEAN:def 3;
then 'not'(Valid(p,J).v) = TRUE by MARGREL1:11;
then ('not' Valid(p,J)).v = TRUE by MARGREL1:def 19;
then Valid('not' p,J).v = TRUE by Lm1;
hence J,v |= 'not' p;
end;
now
assume J,v |= 'not' p;
then Valid('not' p,J).v = TRUE;
then ('not' Valid(p,J)).v = TRUE by Lm1;
then 'not'(Valid(p,J).v) = TRUE by MARGREL1:def 19;
then Valid(p,J).v = FALSE by MARGREL1:11;
hence not J,v |= p;
end;
hence thesis by A1;
end;
theorem
J,v |= (p '&' q) iff J,v |= p & J,v |= q
proof
A1: now
assume J,v |= p & J,v |= q;
then Valid(p,J).v = TRUE & Valid(q,J).v = TRUE;
then (Valid(p,J).v) '&' (Valid(q,J).v) = TRUE;
then (Valid(p,J) '&' Valid(q,J)).v = TRUE by MARGREL1:def 20;
then Valid(p '&' q,J).v = TRUE by Lm1;
hence J,v |= (p '&' q);
end;
now
assume J,v |= (p '&' q);
then Valid(p '&' q,J).v = TRUE;
then (Valid(p,J) '&' Valid(q,J)).v = TRUE by Lm1;
then (Valid(p,J).v) '&' (Valid(q,J).v) = TRUE by MARGREL1:def 20;
then Valid(p,J).v = TRUE & Valid(q,J).v = TRUE by MARGREL1:12;
hence J,v |= p & J,v |= q;
end;
hence thesis by A1;
end;
theorem Th19:
J,v |= All(x,p) iff FOR_ALL(x,Valid(p,J)).v = TRUE
by Lm1;
theorem Th20:
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
proof
hereby
assume J,v |= All(x,p);
then FOR_ALL(x,Valid(p,J)).v = TRUE by Th19;
hence
for v1 st for y st x <> y holds v1.y = v.y holds Valid(p,J).v1 = TRUE
by Th3;
end;
assume for v1 st for y st x <> y holds v1.y = v.y holds Valid(p,J).v1 = TRUE;
then FOR_ALL(x,Valid(p,J)).v = TRUE by Th3;
hence thesis by Th19;
end;
theorem
Valid('not' 'not' p,J) = Valid(p,J)
proof
now
let v;
thus Valid('not' 'not' p,J).v = 'not'(Valid('not' p,J).v) by Th10
.= 'not'('not'(Valid(p,J).v)) by Th10
.= Valid(p,J).v;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th22:
Valid(p '&' p,J) = Valid(p,J)
proof
now
let v;
thus Valid(p '&' p,J).v = (Valid(p,J).v) '&' (Valid(p,J).v) by Th12
.= Valid(p,J).v;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th23:
J,v |= p => q iff Valid(p, J).v = FALSE or Valid(q, J).v = TRUE
proof
A1: now
A2: now
assume
A3: Valid(q, J).v = TRUE;
assume not J,v |= p => q;
then Valid(p => q, J).v <> TRUE;
then Valid(p => q, J).v = FALSE by XBOOLEAN:def 3;
then Valid('not'(p '&' 'not' q), J).v = FALSE by QC_LANG2:def 2;
then 'not'(Valid(p '&' 'not' q, J).v) = FALSE by Th10;
then Valid(p '&' 'not' q, J).v = TRUE by MARGREL1:11;
then (Valid(p, J).v) '&' (Valid('not' q, J).v) = TRUE by Th12;
then (Valid(p, J).v) '&' 'not'(Valid(q, J).v) = TRUE by Th10;
then 'not' (Valid(q, J).v) = TRUE by MARGREL1:12;
hence contradiction by A3,MARGREL1:11;
end;
A4: now
assume Valid(p, J).v = FALSE;
then (Valid(p, J).v) '&' (Valid('not' q, J).v) = FALSE by MARGREL1:12;
then Valid(p '&' 'not' q, J).v = FALSE by Th12;
then 'not'(Valid(p '&' 'not' q, J).v) = TRUE by MARGREL1:11;
then Valid('not'(p '&' 'not' q), J).v = TRUE by Th10;
then Valid(p => q, J).v = TRUE by QC_LANG2:def 2;
hence J,v |= p => q;
end;
assume Valid(p, J).v = FALSE or Valid(q, J).v = TRUE;
hence J,v |= p => q by A4,A2;
end;
now
assume J,v |= p => q;
then Valid(p => q, J).v = TRUE;
then Valid('not'(p '&' 'not' q), J).v = TRUE by QC_LANG2:def 2;
then 'not'(Valid(p '&' 'not' q, J).v) = TRUE by Th10;
then Valid(p '&' 'not' q, J).v = FALSE by MARGREL1:11;
then (Valid(p, J).v) '&' (Valid('not' q, J).v) = FALSE by Th12;
then (Valid(p, J).v) '&' 'not'(Valid(q, J).v) = FALSE by Th10;
then Valid(p, J).v = FALSE or 'not' (Valid(q, J).v) = FALSE by MARGREL1:12;
hence Valid(p, J).v = FALSE or Valid(q, J).v = TRUE by MARGREL1:11;
end;
hence thesis by A1;
end;
theorem Th24:
J,v |= p => q iff (J,v |= p implies J,v |= q)
proof
thus J,v |= p => q & J,v |= p implies J,v |= q by Th23;
assume J,v |= p implies J,v |= q;
then Valid(p, J).v = TRUE implies Valid(q, J).v = TRUE;
then Valid(p, J).v = FALSE or Valid(q, J).v = TRUE by XBOOLEAN:def 3;
hence thesis by Th23;
end;
theorem Th25:
for p being Element of Funcs(Valuations_in(Al,A),BOOLEAN) holds
FOR_ALL(x,p).v = TRUE implies p.v = TRUE
proof
let p be Element of Funcs(Valuations_in(Al,A),BOOLEAN);
for y st x <> y holds v.y = v.y;
hence thesis by Th3;
end;
definition
let Al, A, J, p;
pred J |= p means
for v holds J,v |= p;
end;
reserve u,w,z for Element of BOOLEAN;
Lm2: 'not'('not'(u '&' 'not' w) '&' ('not'(w '&' z) '&' (u '&' z))) = TRUE
proof
per cases by XBOOLEAN:def 3;
suppose
z = TRUE & w = TRUE;
then 'not'(w '&' z) = FALSE by MARGREL1:11;
then 'not'(w '&' z) '&' (u '&' z) = FALSE by MARGREL1:12;
then 'not'(u '&' 'not' w) '&' ('not' (w '&' z) '&' (u '&' z)) = FALSE by
MARGREL1:12;
hence thesis by MARGREL1:11;
end;
suppose that
A1: w = FALSE and
A2: u = TRUE;
'not' w = TRUE by A1,MARGREL1:11;
then 'not'(u '&' 'not' w) = FALSE by A2,MARGREL1:11;
then 'not'(u '&' 'not' w) '&' ('not' (w '&' z) '&' (u '&' z)) = FALSE by
MARGREL1:12;
hence thesis by MARGREL1:11;
end;
suppose
u = FALSE;
then u '&' z = FALSE by MARGREL1:12;
then 'not'(w '&' z) '&' (u '&' z) = FALSE by MARGREL1:12;
then 'not'(u '&' 'not' w) '&' ('not' (w '&' z) '&' (u '&' z)) = FALSE by
MARGREL1:12;
hence thesis by MARGREL1:11;
end;
suppose
z = FALSE;
then u '&' z = FALSE by MARGREL1:12;
then 'not'(w '&' z) '&' (u '&' z) = FALSE by MARGREL1:12;
then 'not'(u '&' 'not' w) '&' ('not' (w '&' z) '&' (u '&' z)) = FALSE by
MARGREL1:12;
hence thesis by MARGREL1:11;
end;
end;
reserve w,v2 for Element of Valuations_in(Al,A),
z for bound_QC-variable of Al;
Lm3: now let Al; let A be non empty set, Y, Z be bound_QC-variable of Al,
V1, V2 be Element of Valuations_in(Al,A);
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
proof
deffunc G(object) = V2.Z;
deffunc F(object) = V1.$1;
defpred C[object] means for x1 st x1 = $1 holds x1 <> Y;
A1: for x being object st x in bound_QC-variables(Al) holds
(C[x] implies F(x) in A) & (not C[x] implies G(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 (C[x] implies f.x =
F(x)) & (not C[x] implies f.x = G(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 as Element of Valuations_in(Al,A) by FUNCT_2:def 2;
take f;
now
let x be bound_QC-variable of Al;
now
assume
A3: x <> Y;
(for x1 st x1 = x holds x1 <> Y) implies f.x = V1.x by A2;
hence f.x = V1.x by A3;
end;
hence x <> Y implies f.x = V1.x;
thus x = Y implies f.Y = V2.Z by A2;
end;
hence thesis;
end;
end;
theorem
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 by Lm3;
theorem Th27:
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
proof
defpred PP[Element of CQC-WFF(Al)] means
not x in still_not-bound_in $1 implies
for v,w st for y st x<>y holds w.y = v.y holds Valid($1,J).v = Valid($1,J).w;
A1: now
let s,t,y,k,ll,P;
thus PP[VERUM(Al)]
proof
assume not x in still_not-bound_in VERUM(Al);
thus for v,w st for y st x<>y holds w.y = v.y holds
Valid(VERUM(Al),J).v = Valid(VERUM(Al),J).w
proof
let v,w such that
for y st x <> y holds w.y = v.y;
Valid(VERUM(Al),J).v = TRUE by Th5;
hence thesis by Th5;
end;
end;
A2: rng ll c= bound_QC-variables(Al) by RELAT_1:def 19;
thus PP[P!ll]
proof
assume
A3: not x in still_not-bound_in (P!ll);
thus for v,w st for y st x<>y holds w.y = v.y holds Valid(P!ll,J).v =
Valid(P!ll,J).w
proof
let v,w such that
A4: for y st x <> y holds w.y = v.y;
A5: now
A6: len (v*'ll) = k by Def3;
A7: now
let i be Nat;
assume
A8: 1 <= i & i <= len (v*'ll);
A9: len (v*'ll) = len ll by A6,CARD_1:def 7;
then i in dom ll by A8,FINSEQ_3:25;
then ll.i in rng ll by FUNCT_1:def 3;
then reconsider z = ll.i as bound_QC-variable of Al by A2;
ll.i <> x
proof
reconsider M = still_not-bound_in ll as set;
not x in M by A3,QC_LANG3:5;
then not x in variables_in(ll,bound_QC-variables(Al))
by QC_LANG3:2;
then not x in {ll.i2 where i2 is Nat: 1 <= i2 & i2
<= len ll & ll.i2 in bound_QC-variables(Al)} by QC_LANG3:def 1;
hence thesis by A8,A9;
end;
then
A10: w.z = v.z by A4;
(v*'ll).i = v.(ll.i) by A6,A8,Def3;
hence (v*'ll).i = (w*'ll).i by A6,A8,A10,Def3;
end;
assume
A11: Valid(P!ll,J).v = TRUE;
then (ll 'in' (J.P)).v = TRUE by Lm1;
then
A12: v*'ll in (J.P) by Def4;
len (w*'ll) = k by Def3;
then w*'ll in (J.P) by A12,A6,A7,FINSEQ_1:14;
then (ll 'in' (J.P)).w = TRUE by Def4;
hence thesis by A11,Lm1;
end;
now
A13: len (v*'ll) = k by Def3;
A14: now
let i be Nat;
assume
A15: 1 <= i & i <= len (v*'ll);
A16: len (v*'ll) = len ll by A13,CARD_1:def 7;
then i in dom ll by A15,FINSEQ_3:25;
then ll.i in rng ll by FUNCT_1:def 3;
then reconsider z = ll.i as bound_QC-variable of Al by A2;
ll.i <> x
proof
reconsider M = still_not-bound_in ll as set;
not x in M by A3,QC_LANG3:5;
then not x in variables_in(ll,bound_QC-variables(Al))
by QC_LANG3:2;
then i in NAT & not x in {ll.i2 where i2 is Nat : 1
<= i2 & i2 <= len ll & ll.i2 in bound_QC-variables(Al)} by ORDINAL1:def 12
,QC_LANG3:def 1;
hence thesis by A15,A16;
end;
then
A17: w.z = v.z by A4;
(v*'ll).i = v.(ll.i) by A13,A15,Def3;
hence (v*'ll).i = (w*'ll).i by A13,A15,A17,Def3;
end;
assume
A18: Valid(P!ll,J).v = FALSE;
then (ll 'in' (J.P)).v = FALSE by Lm1;
then
A19: not v*'ll in (J.P) by Def4;
len (w*'ll) = k by Def3;
then not w*'ll in (J.P) by A19,A13,A14,FINSEQ_1:14;
then (ll 'in' (J.P)).w = FALSE by Def4;
hence thesis by A18,Lm1;
end;
hence thesis by A5,XBOOLEAN:def 3;
end;
end;
thus PP[s] implies PP['not' s]
proof
assume
A20: ( not x in still_not-bound_in s implies for v,w st for y st x<>
y holds w.y = v. y holds Valid(s,J).v = Valid(s,J).w)& not x in
still_not-bound_in 'not' s;
thus for v,w st for y st x<>y holds w.y = v.y holds Valid('not' s,J).v =
Valid('not' s,J).w
proof
let v,w such that
A21: for y st x<>y holds w.y = v.y;
A22: now
assume
A23: Valid('not' s,J).v = FALSE;
then 'not'(Valid(s,J).v) = FALSE by Th10;
then Valid(s,J).v = TRUE by MARGREL1:11;
then Valid(s,J).w = TRUE by A20,A21,QC_LANG3:7;
then 'not'(Valid(s,J).w) = FALSE by MARGREL1:11;
hence thesis by A23,Th10;
end;
now
assume
A24: Valid('not' s,J).v = TRUE;
then 'not'(Valid(s,J).v) = TRUE by Th10;
then Valid(s,J).v = FALSE by MARGREL1:11;
then Valid(s,J).w = FALSE by A20,A21,QC_LANG3:7;
then 'not'(Valid(s,J).w) = TRUE by MARGREL1:11;
hence thesis by A24,Th10;
end;
hence thesis by A22,XBOOLEAN:def 3;
end;
end;
thus PP[s] & PP[t] implies PP[s '&' t]
proof
assume that
A25: not x in still_not-bound_in s implies for v,w st for y st x<>y
holds w.y = v.y holds Valid(s,J).v = Valid(s,J).w and
A26: not x in still_not-bound_in t implies for v,w st for y st x<>y
holds w.y = v.y holds Valid(t,J).v = Valid(t,J).w and
A27: not x in still_not-bound_in s '&' t;
A28: not x in (still_not-bound_in s) \/ (still_not-bound_in t) by A27,
QC_LANG3:10;
thus for v,w st for y st x<>y holds w.y = v.y holds Valid(s '&' t,J).v =
Valid(s '&' t, J).w
proof
let v,w such that
A29: for y st x<>y holds w.y = v.y;
A30: now
assume
A31: Valid(s '&' t,J).v = FALSE;
A32: now
assume Valid(s,J).v = FALSE;
then Valid(s,J).w = FALSE by A25,A28,A29,XBOOLE_0:def 3;
then (Valid(s,J).w) '&' (Valid(t,J).w) = FALSE by MARGREL1:12;
hence thesis by A31,Th12;
end;
A33: now
assume Valid(t,J).v = FALSE;
then Valid(t,J).w = FALSE by A26,A28,A29,XBOOLE_0:def 3;
then (Valid(s,J).w) '&' (Valid(t,J).w) = FALSE by MARGREL1:12;
hence thesis by A31,Th12;
end;
(Valid(s,J).v) '&' (Valid(t,J).v) = FALSE by A31,Th12;
hence thesis by A32,A33,MARGREL1:12;
end;
now
assume
A34: Valid(s '&' t,J).v = TRUE;
then
A35: (Valid(s,J).v) '&' (Valid(t,J).v) = TRUE by Th12;
then Valid(t,J).v = TRUE by MARGREL1:12;
then
A36: Valid(t,J).w = TRUE by A26,A28,A29,XBOOLE_0:def 3;
Valid(s,J).v = TRUE by A35,MARGREL1:12;
then Valid(s,J).w = TRUE by A25,A28,A29,XBOOLE_0:def 3;
then (Valid(s,J).w) '&' (Valid(t,J).w) = TRUE by A36;
hence thesis by A34,Th12;
end;
hence thesis by A30,XBOOLEAN:def 3;
end;
end;
thus PP[s] implies PP[All(y,s)]
proof
assume that
A37: not x in still_not-bound_in s implies for v,w st for y st x<>y
holds w.y = v.y holds Valid(s,J).v = Valid(s,J).w and
A38: not x in still_not-bound_in All(y,s);
A39: not x in (still_not-bound_in s) \ {y} by A38,QC_LANG3:12;
thus for v,w st for z st x<>z holds w.z = v.z holds Valid(All(y,s),J).v
= Valid(All(y,s),J).w
proof
let v,w such that
A40: for z st x<>z holds w.z = v.z;
A41: now
assume
A42: Valid(All(y,s),J).v = FALSE;
then FOR_ALL(y,Valid(s,J)).v = FALSE by Lm1;
then consider v1 such that
A43: Valid(s,J).v1 = FALSE and
A44: for z st y <> z holds v1.z = v.z by Th2;
A45: now
assume
A46: not x in (still_not-bound_in s);
consider v2 such that
A47: (for z st z <> y holds v2.z = w.z) & v2.y = v1.y by Lm3;
take v2;
for z st x <> z holds v2.z = v1.z
proof
let z such that
A48: x <> z;
now
assume
A49: z <> y;
hence v2.z = w.z by A47
.= v.z by A40,A48
.= v1.z by A44,A49;
end;
hence thesis by A47;
end;
hence Valid(s,J).v2 = FALSE by A37,A43,A46;
thus for z st y <> z holds v2.z = w.z by A47;
end;
now
assume
A50: x in {y};
take v2 = v1;
thus Valid(s,J).v2 = FALSE by A43;
for z st y <> z holds v1.z = w.z
proof
let z;
assume
A51: y <> z;
then
A52: x <> z by A50,TARSKI:def 1;
thus v1.z = v.z by A44,A51
.= w.z by A40,A52;
end;
hence for z st y <> z holds v2.z = w.z;
end;
then FOR_ALL(y,Valid(s,J)).w = FALSE by A39,A45,Th2,XBOOLE_0:def 5;
hence thesis by A42,Lm1;
end;
now
assume
A53: Valid(All(y,s),J).v = TRUE;
then
A54: FOR_ALL(y,Valid(s,J)).v = TRUE by Lm1;
for v1 st for z st y<>z holds v1.z = w.z holds Valid(s,J).v1 = TRUE
proof
let v1 such that
A55: for z st y<>z holds v1.z = w.z;
A56: now
assume
A57: not x in (still_not-bound_in s);
consider v2 such that
A58: (for z st z <> y holds v2.z = v.z) & v2.y = v1.y by Lm3;
A59: for z st x <> z holds v2.z = v1.z
proof
let z such that
A60: x <> z;
now
assume
A61: z <> y;
hence v2.z = v.z by A58
.= w.z by A40,A60
.= v1.z by A55,A61;
end;
hence thesis by A58;
end;
Valid(s,J).v2 = TRUE by A54,A58,Th3;
hence thesis by A37,A57,A59;
end;
now
assume x in {y};
then
A62: x = y by TARSKI:def 1;
for z st y <> z holds v1.z = v.z
proof
let z;
assume
A63: y <> z;
hence v.z = w.z by A40,A62
.= v1.z by A55,A63;
end;
hence thesis by A54,Th3;
end;
hence thesis by A39,A56,XBOOLE_0:def 5;
end;
then FOR_ALL(y,Valid(s,J)).w = TRUE by Th3;
hence thesis by A53,Lm1;
end;
hence thesis by A41,XBOOLEAN:def 3;
end;
end;
end;
for s holds PP[s] from CQC_LANG:sch 1(A1);
hence thesis;
end;
theorem Th28:
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 by Th27;
theorem Th29:
J,v |= All(x,p) iff for w st for y st x<>y holds w.y = v.y holds J,w |= p
proof
A1: now
assume
A2: for w st for y st x<>y holds w.y = v.y holds J,w |= p;
for w st for y st x<>y holds w.y = v.y holds Valid(p,J).w = TRUE
by A2,Def7;
hence J,v |= All(x,p) by Th20;
end;
J,v |= All(x,p) implies for w st for y st x<>y holds w.y = v.y holds J,w |= p
by Th20;
hence thesis by A1;
end;
reserve u,w for Element of Valuations_in(Al,A);
reserve s9 for QC-formula of Al;
theorem Th30:
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
proof
defpred PP[Element of QC-WFF(Al)] means
for x,y,p,q st x <> y & p = $1.x & q =$1.y holds
for v st v.x = v.y holds Valid(p,J).v = Valid(q,J).v;
A1: now
let s be Element of QC-WFF(Al);
thus s is atomic implies PP[s]
proof
assume
A2: s is atomic;
thus for x,y,p,q st x <> y & p = s.x & q = s.y holds for v st v.x = v.y
holds Valid(p,J).v = Valid(q,J).v
proof
consider k being Nat, P being (QC-pred_symbol of k,Al), l
being QC-variable_list of k,Al such that
A3: s = P!l by A2,QC_LANG1:def 18;
let x,y,p,q such that
x <> y and
A4: p = s.x and
A5: q = s.y;
set lx = Subst(l, (Al)a.0 .-->x), ly = Subst(l, (Al)a.0 .-->y);
let v such that
A6: v.x = v.y;
A7: p = P!Subst(l, (Al)a.0 .-->x) by A4,A3,CQC_LANG:17;
then
A8: {lx.i : 1 <= i & i <= len lx & lx.i in free_QC-variables(Al)} = {} by
CQC_LANG:7;
A9: q = P!Subst(l, (Al)a.0 .-->y) by A5,A3,CQC_LANG:17;
then
A10: {ly.i : 1 <= i & i <= len ly & ly.i in free_QC-variables(Al)} = {} by
CQC_LANG:7;
A11: {ly.j : 1 <= j & j <= len ly & ly.j in fixed_QC-variables(Al)} = {}
by A9,CQC_LANG:7;
{lx.j : 1 <= j & j <= len lx & lx.j in fixed_QC-variables(Al)} = {}
by A7,CQC_LANG:7;
then reconsider lx,ly as CQC-variable_list of k,Al by A8,A10,A11,
CQC_LANG:5;
A12: len (v*'lx) = k by Def3;
A13: now
let i be Nat;
assume that
A14: 1 <= i and
A15: i <= len (v*'lx);
A16: i <= len l by A12,A15,CARD_1:def 7;
A17: now
assume l.i <> (Al)a.0;
then
A18: lx.i = l.i & ly.i = l.i by A14,A16,CQC_LANG:3;
v.(lx.i) = (v*'lx).i by A12,A14,A15,Def3;
hence (v*'lx).i = (v*'ly).i by A12,A14,A15,A18,Def3;
end;
now
assume l.i = (Al)a.0;
then
A19: lx.i = x & ly.i = y by A14,A16,CQC_LANG:3;
v.(lx.i) = (v*'lx).i by A12,A14,A15,Def3;
hence (v*'lx).i = (v*'ly).i by A6,A12,A14,A15,A19,Def3;
end;
hence (v*'lx).i = (v*'ly).i by A17;
end;
len (v*'ly) = k by Def3;
then
A20: v*'lx = v*'ly by A12,A13,FINSEQ_1:14;
A21: now
assume Valid(p,J).v = FALSE;
then not v*'lx in J.P by A7,Th8;
hence Valid(q,J).v = FALSE by A9,A20,Th8;
end;
now
assume Valid(p,J).v = TRUE;
then v*'lx in J.P by A7,Th7;
hence Valid(q,J).v = TRUE by A9,A20,Th7;
end;
hence thesis by A21,XBOOLEAN:def 3;
end;
end;
thus PP[VERUM(Al)]
proof
let x,y,p,q such that
x <> y and
A22: p = VERUM(Al).x and
A23: q = VERUM(Al).y;
let v such that
v.x = v.y;
p = VERUM(Al) by A22,CQC_LANG:15;
hence thesis by A23,CQC_LANG:15;
end;
thus s is negative & PP[the_argument_of s] implies PP[s]
proof
assume that
A24: s is negative and
A25: for x,y,p,q st x <> y & p = (the_argument_of s).x & q = (
the_argument_of s).y holds for v st v.x = v.y holds Valid(p,J).v = Valid(q,J).v
;
thus for x,y,p,q st x <> y & p = s.x & q = s.y holds for v st v.x = v.y
holds Valid(p,J).v = Valid(q,J).v
proof
let x,y,p,q such that
x <> y and
A26: p = s.x and
A27: q = s.y;
A28: s.y = 'not' ((the_argument_of s).y) by A24,CQC_LANG:18;
then reconsider
qa = (the_argument_of s).y as Element of CQC-WFF(Al)
by A27,CQC_LANG:8;
A29: s.x = 'not'((the_argument_of s).x) by A24,CQC_LANG:18;
then reconsider
pa = (the_argument_of s).x as Element of CQC-WFF(Al)
by A26,CQC_LANG:8;
let v such that
A30: v.x = v.y;
A31: now
assume Valid(p,J).v = FALSE;
then 'not'(Valid(pa,J).v) = FALSE by A26,A29,Th10;
then Valid(pa,J).v = TRUE by MARGREL1:11;
then Valid(qa,J).v = TRUE by A25,A30;
then 'not'(Valid(qa,J).v) = FALSE by MARGREL1:11;
hence Valid(q,J).v = FALSE by A27,A28,Th10;
end;
now
assume Valid(p,J).v = TRUE;
then 'not'(Valid(pa,J).v) = TRUE by A26,A29,Th10;
then Valid(pa,J).v = FALSE by MARGREL1:11;
then Valid(qa,J).v = FALSE by A25,A30;
then 'not'(Valid(qa,J).v) = TRUE by MARGREL1:11;
hence Valid(q,J).v = TRUE by A27,A28,Th10;
end;
hence thesis by A31,XBOOLEAN:def 3;
end;
end;
thus s is conjunctive & PP[the_left_argument_of s] & PP[
the_right_argument_of s] implies PP[s]
proof
assume that
A32: s is conjunctive and
A33: for x,y,p,q st x <> y & p = (the_left_argument_of s).x & q = (
the_left_argument_of s).y holds for v st v.x = v.y holds Valid(p,J).v = Valid(q
,J).v and
A34: for x,y,p,q st x <> y & p = (the_right_argument_of s).x & q = (
the_right_argument_of s).y holds for v st v.x = v.y holds Valid(p,J).v = Valid(
q,J).v;
thus for x,y,p,q st x <> y & p = s.x & q = s.y holds for v st v.x = v.y
holds Valid(p,J).v = Valid(q,J).v
proof
let x,y,p,q such that
x <> y and
A35: p = s.x and
A36: q = s.y;
A37: s.x=((the_left_argument_of s).x) '&' ((the_right_argument_of s).x
) by A32,CQC_LANG:20;
then reconsider pla = (the_left_argument_of s).x, pra = (
the_right_argument_of s).x as Element of CQC-WFF(Al)
by A35,CQC_LANG:9;
A38: s.y=((the_left_argument_of s).y) '&' ((the_right_argument_of s).y
) by A32,CQC_LANG:20;
then reconsider qla = (the_left_argument_of s).y, qra = (
the_right_argument_of s).y as Element of CQC-WFF(Al)
by A36,CQC_LANG:9;
let v such that
A39: v.x = v.y;
A40: now
assume
A41: Valid(p,J).v = FALSE;
A42: now
assume Valid(pla,J).v = FALSE;
then Valid(qla,J).v = FALSE by A33,A39;
then (Valid(qla,J).v) '&' (Valid(qra,J).v) = FALSE by MARGREL1:12;
hence thesis by A36,A38,A41,Th12;
end;
A43: now
assume Valid(pra,J).v = FALSE;
then Valid(qra,J).v = FALSE by A34,A39;
then (Valid(qla,J).v) '&' (Valid(qra,J).v) = FALSE by MARGREL1:12;
hence thesis by A36,A38,A41,Th12;
end;
(Valid(pla,J).v) '&' (Valid(pra,J).v) = FALSE by A35,A37,A41,Th12;
hence thesis by A42,A43,MARGREL1:12;
end;
now
assume Valid(p,J).v = TRUE;
then
A44: (Valid(pla,J).v) '&' (Valid(pra,J).v) = TRUE by A35,A37,Th12;
then Valid(pra,J).v = TRUE by MARGREL1:12;
then
A45: Valid(qra,J).v = TRUE by A34,A39;
Valid(pla,J).v = TRUE by A44,MARGREL1:12;
then Valid(qla,J).v = TRUE by A33,A39;
then (Valid(qla,J).v) '&' (Valid(qra,J).v) = TRUE by A45;
hence Valid(q,J).v = TRUE by A36,A38,Th12;
end;
hence thesis by A40,XBOOLEAN:def 3;
end;
end;
thus s is universal & PP[the_scope_of s] implies PP[s]
proof
assume that
A46: s is universal and
A47: for x,y,p,q st x<>y & p = (the_scope_of s).x & q = (
the_scope_of s).y holds for v st v.x = v.y holds Valid(p,J).v = Valid(q,J).v;
consider xx being bound_QC-variable of Al,
pp being Element of QC-WFF(Al) such that
A48: s = All(xx,pp) by A46,QC_LANG1:def 21;
A49: xx = bound_in s by A46,A48,QC_LANG1:def 27;
thus for x,y,p,q st x <> y & p = s.x & q = s.y holds for v st v.x = v.y
holds Valid(p,J).v = Valid(q,J).v
proof
let x,y,p,q such that
x <> y and
A50: p = s.x and
A51: q = s.y;
let v such that
A52: v.x = v.y;
A53: now
assume
A54: x <> bound_in s;
then s.x = All(bound_in s, (the_scope_of s).x) by A46,CQC_LANG:23;
then reconsider
ps = (the_scope_of s).x as Element of CQC-WFF(Al) by A50,CQC_LANG:13;
A55: All(bound_in s, ps) = p by A46,A50,A54,CQC_LANG:23;
A56: now
assume
A57: y <> bound_in s;
then s.y = All(bound_in s, (the_scope_of s).y) by A46,CQC_LANG:23;
then reconsider
qs = (the_scope_of s).y as Element of CQC-WFF(Al)
by A51,CQC_LANG:13;
A58: Valid(All(bound_in s, qs),J) = FOR_ALL(bound_in s, Valid(qs,
J)) by Lm1;
A59: Valid(All(bound_in s, ps),J) = FOR_ALL(bound_in s, Valid(ps,
J)) by Lm1;
A60: All(bound_in s, qs) = q by A46,A51,A57,CQC_LANG:23;
A61: now
assume
A62: Valid(p,J).v = TRUE;
for v1 st for y st (bound_in s) <> y holds v1.y = v.y
holds Valid(qs,J).v1 = TRUE
proof
let v1;
assume
A63: for y st (bound_in s) <> y holds v1.y = v.y;
then
A64: v1.x = v.x & v1.y = v.y by A54,A57;
Valid(ps,J).v1 = TRUE by A55,A59,A62,A63,Th3;
hence thesis by A47,A52,A64;
end;
hence Valid(q,J).v = TRUE by A60,A58,Th3;
end;
now
assume
A65: Valid(p,J).v = FALSE;
ex v1 st Valid(qs,J).v1 = FALSE & for y st (bound_in s) <>
y holds v1.y = v.y
proof
consider v1 such that
A66: Valid(ps,J).v1 = FALSE and
A67: for y st (bound_in s) <> y holds v1.y = v.y by A55,A59,A65,Th2;
v1.x = v.x & v1.y = v.y by A54,A57,A67;
then Valid(qs,J).v1 = FALSE by A47,A52,A66;
hence thesis by A67;
end;
hence Valid(q,J).v = FALSE by A60,A58,Th2;
end;
hence thesis by A61,XBOOLEAN:def 3;
end;
now
assume
A68: y = bound_in s;
then q = All(y,pp) by A48,A49,A51,CQC_LANG:24;
hence thesis by A48,A49,A50,A68,CQC_LANG:27;
end;
hence thesis by A56;
end;
now
assume
A69: x = bound_in s;
then p = All(x,pp) by A48,A49,A50,CQC_LANG:24;
hence thesis by A48,A49,A51,A69,CQC_LANG:27;
end;
hence thesis by A53;
end;
end;
end;
for s being Element of QC-WFF(Al) holds PP[s] from QC_LANG1:sch 2 (A1);
hence thesis;
end;
theorem Th31:
x <> y & not x in still_not-bound_in s9 implies not x in
still_not-bound_in (s9.y)
proof
defpred PP[Element of QC-WFF(Al)] means x <> y &
not x in still_not-bound_in ($1) implies
not x in still_not-bound_in ($1.y);
A1: now
let s be Element of QC-WFF(Al);
thus s is atomic implies PP[s]
proof
assume that
A2: s is atomic and
A3: x <> y and
A4: not x in still_not-bound_in s;
thus not x in still_not-bound_in (s.y)
proof
set l = the_arguments_of s;
set ll = Subst(l,(Al)a.0 .-->y);
A5: still_not-bound_in s = still_not-bound_in l by A2,QC_LANG3:4
.= variables_in(l, bound_QC-variables(Al)) by QC_LANG3:2
.={l.k : 1<=k & k<=len l & l.k in bound_QC-variables(Al)} by
QC_LANG3:def 1;
A6: x in {ll.k : 1 <= k & k <= len ll & ll.k in bound_QC-variables(Al)}
implies x in {l.i : 1 <= i & i <= len l &
l.i in bound_QC-variables(Al)}
proof
assume
x in {ll.k : 1 <= k & k <= len ll & ll.k in bound_QC-variables(Al)};
then consider k such that
A7: x = ll.k and
A8: 1 <= k and
A9: k <= len ll and
ll.k in bound_QC-variables(Al);
A10: k <= len l by A9,CQC_LANG:def 1;
then x = l.k by A3,A7,A8,CQC_LANG:3;
hence thesis by A8,A10;
end;
A11: s.y = (the_pred_symbol_of s)!Subst(l,(Al)a.0 .-->y) by A2,CQC_LANG:16;
A12: s.y is atomic & the_arguments_of s.y = ll
proof
consider k being Nat, p being (QC-pred_symbol of k,Al), l2
being QC-variable_list of k,Al such that
A13: s = p!l2 by A2,QC_LANG1:def 18;
l2 = l by A2,A13,QC_LANG1:def 23;
then reconsider l3 = Subst(l,(Al)a.0 .-->y)
as QC-variable_list of k,Al;
A14: s.y = p!l3 by A2,A11,A13,QC_LANG1:def 22;
hence s.y is atomic by QC_LANG1:def 18;
hence thesis by A14,QC_LANG1:def 23;
end;
then still_not-bound_in the_arguments_of s.y = variables_in(ll,
bound_QC-variables(Al)) by QC_LANG3:2
.={ll.k : 1<=k & k<= len ll & ll.k in bound_QC-variables(Al)} by
QC_LANG3:def 1;
hence thesis by A4,A5,A12,A6,QC_LANG3:4;
end;
end;
thus PP[VERUM(Al)] by CQC_LANG:15;
thus s is negative & PP[the_argument_of s] implies PP[s]
proof
assume that
A15: s is negative and
A16: ( x <> y & not x in still_not-bound_in (the_argument_of s)
implies not x in still_not-bound_in ((the_argument_of s).y))& x <> y & not x in
still_not-bound_in s;
not x in still_not-bound_in 'not'((the_argument_of s).y) by A15,A16,
QC_LANG3:6,7;
hence thesis by A15,CQC_LANG:18;
end;
thus s is conjunctive & PP[the_left_argument_of s] & PP[
the_right_argument_of s] implies PP[s]
proof
assume that
A17: s is conjunctive and
A18: ( x <> y & not x in still_not-bound_in (the_left_argument_of s)
implies not x in still_not-bound_in ((the_left_argument_of s).y))&( x <> y &
not x in still_not-bound_in (the_right_argument_of s) implies not x in
still_not-bound_in ((the_right_argument_of s).y)) & x <> y & not x in
still_not-bound_in s;
still_not-bound_in s = (still_not-bound_in (the_left_argument_of s)
) \/ (still_not-bound_in (the_right_argument_of s)) by A17,QC_LANG3:9;
then not x in still_not-bound_in ((the_left_argument_of s).y) \/
still_not-bound_in ((the_right_argument_of s).y) by A18,XBOOLE_0:def 3;
then not x in (still_not-bound_in ((the_left_argument_of s).y) '&' ((
the_right_argument_of s).y)) by QC_LANG3:10;
hence thesis by A17,CQC_LANG:20;
end;
thus s is universal & PP[the_scope_of s] implies PP[s]
proof
assume that
A19: s is universal and
A20: x <> y & not x in still_not-bound_in (the_scope_of s) implies
not x in still_not-bound_in ((the_scope_of s).y) and
A21: x <> y and
A22: not x in still_not-bound_in s;
A23: still_not-bound_in s = still_not-bound_in (the_scope_of s) \ {
bound_in s} by A19,QC_LANG3:11;
thus not x in still_not-bound_in (s.y)
proof
A24: now
still_not-bound_in All(x,(the_scope_of s).y) =
still_not-bound_in ((the_scope_of s).y) \ {x} by QC_LANG3:12;
then
A25: not x in still_not-bound_in All(x,(the_scope_of s).y) iff not x
in still_not-bound_in ((the_scope_of s).y) or x in {x} by XBOOLE_0:def 5;
assume x in {bound_in s};
then x = bound_in s by TARSKI:def 1;
hence thesis by A19,A21,A25,CQC_LANG:23,TARSKI:def 1;
end;
now
assume not x in still_not-bound_in (the_scope_of s);
then
not x in still_not-bound_in ((the_scope_of s).y) \ {bound_in s}
by A20,A21,XBOOLE_0:def 5;
then not x in still_not-bound_in All(bound_in s,(the_scope_of s).y)
by QC_LANG3:12;
hence thesis by A19,A22,CQC_LANG:22,23;
end;
hence thesis by A22,A23,A24,XBOOLE_0:def 5;
end;
end;
end;
for s being Element of QC-WFF(Al) holds PP[s] from QC_LANG1:sch 2 (A1);
hence thesis;
end;
theorem Th32:
J,v |= VERUM(Al)
proof
(Valuations_in(Al,A) --> TRUE).v = TRUE by FUNCOP_1:7;
then (Valid(VERUM(Al),J)).v = TRUE by Lm1;
hence thesis;
end;
theorem Th33:
J,v |= p '&' q => q '&' p
proof
thus Valid(p '&' q => q '&' p, J).v = TRUE
proof
assume not Valid(p '&' q => q '&' p, J).v = TRUE;
then
A1: Valid(p '&' q => q '&' p, J).v = FALSE by XBOOLEAN:def 3;
Valid(p '&' q => q '&' p, J).v = Valid('not'((p '&' q) '&' 'not' (q
'&' p)), J).v by QC_LANG2:def 2
.= 'not'(Valid(((p '&' q) '&' 'not'(q '&' p)), J).v) by Th10
.= 'not'((Valid(p '&' q, J).v) '&' (Valid('not' (q '&' p), J).v)) by Th12
.= 'not'((Valid(p '&' q, J).v) '&' 'not' (Valid(q '&' p, J).v)) by Th10;
then
A2: (Valid(p '&' q, J).v) '&' 'not'(Valid(q '&' p, J).v) = TRUE by A1,
MARGREL1:11;
then 'not' (Valid(q '&' p, J).v) = TRUE by MARGREL1:12;
then
A3: Valid(q '&' p, J).v = FALSE by MARGREL1:11;
Valid(p '&' q, J).v = TRUE by A2,MARGREL1:12;
then (Valid(p, J).v) '&' (Valid(q, J).v) = TRUE by Th12;
hence thesis by A3,Th12;
end;
end;
theorem Th34:
J,v |= ('not' p => p) => p
proof
'not' p => p = 'not'('not' p '&' 'not' p) by QC_LANG2:def 2;
then
A1: Valid(('not' p => p) => p, J).v = Valid('not'('not'('not' p '&' 'not' p)
'&' 'not' p), J).v by QC_LANG2:def 2
.= 'not'(Valid('not'('not' p '&' 'not' p) '&' 'not' p, J).v) by Th10
.= 'not'((Valid('not'('not' p '&' 'not' p), J).v) '&' (Valid('not' p, J)
.v)) by Th12;
Valid('not'('not' p '&' 'not' p), J).v = 'not'(Valid('not' p '&' 'not' p
, J).v) by Th10
.= 'not'(Valid('not' p, J).v) by Th22
.= 'not' 'not'(Valid(p, J).v) by Th10
.= Valid(p, J).v;
then
Valid(('not' p => p) => p, J).v='not'((Valid(p, J).v) '&' 'not' (Valid(p
, J).v)) by A1,Th10
.= TRUE by XBOOLEAN:102;
hence Valid(('not' p => p) => p, J).v = TRUE;
end;
theorem Th35:
J,v |= p => ('not' p => q)
proof
'not' p => q = 'not'('not' p '&' 'not' q) by QC_LANG2:def 2;
then
A1: Valid(p => ('not' p => q), J).v = Valid('not'(p '&' 'not'('not'('not' p
'&' 'not' q))), J).v by QC_LANG2:def 2
.= 'not'(Valid((p '&' 'not'('not'('not' p '&' 'not' q))), J).v) by Th10
.= 'not'((Valid(p,J).v) '&' (Valid('not'('not'('not' p '&' 'not' q)), J)
.v)) by Th12;
Valid('not'('not'('not' p '&' 'not' q)), J).v = 'not'(Valid('not'('not'
p '&' 'not' q), J).v) by Th10
.= 'not' 'not'(Valid('not' p '&' 'not' q, J).v) by Th10
.= (Valid('not' p, J).v) '&' (Valid('not' q, J).v) by Th12
.= 'not'(Valid(p, J).v) '&' (Valid('not' q, J).v) by Th10
.= 'not'(Valid(p, J).v) '&' 'not'(Valid(q, J).v) by Th10;
then
A2: Valid(p => ('not' p => q), J).v = 'not'(((Valid(p,J).v) '&' 'not'(Valid(
p, J).v)) '&' 'not'(Valid(q, J).v)) by A1,MARGREL1:16
.= 'not'(FALSE '&' 'not'(Valid(q, J).v)) by XBOOLEAN:138;
FALSE '&' 'not'(Valid(q, J).v) = FALSE by MARGREL1:13;
hence Valid(p => ('not' p => q), J).v = TRUE by A2,MARGREL1:11;
end;
theorem Th36:
J,v |= (p => q) => ('not'(q '&' t) => 'not'(p '&' t))
proof
p => q = 'not'(p '&' 'not' q) & 'not'(q '&' t) => 'not'(p '&' t) = 'not'
( 'not'(q '&' t) '&' 'not' 'not' (p '&' t)) by QC_LANG2:def 2;
then
A1: Valid((p => q) => ('not'(q '&' t) => 'not'(p '&' t)), J).v = Valid('not'
('not'(p '&' 'not' q) '&' 'not'('not'('not'(q '&' t) '&' 'not' 'not'(p '&' t)))
), J).v by QC_LANG2:def 2
.= 'not'(Valid('not'(p '&' 'not' q) '&' 'not'('not'('not'(q '&' t) '&'
'not' 'not'(p '&' t))), J).v) by Th10
.= 'not'((Valid('not'(p '&' 'not' q), J).v) '&' (Valid('not'('not'('not'
(q '&' t) '&' 'not' 'not' (p '&' t))), J).v)) by Th12;
A2: Valid('not'(p '&' 'not' q), J).v = 'not'(Valid(p '&' 'not' q, J).v) by Th10
.= 'not'((Valid(p, J).v) '&' (Valid('not' q, J).v)) by Th12
.= 'not'((Valid(p, J).v) '&'('not'(Valid(q, J).v))) by Th10;
Valid('not'('not'('not'(q '&' t) '&' 'not' 'not'(p '&' t))), J).v =
'not'(Valid('not'('not'(q '&' t) '&' 'not' 'not' (p '&' t)), J).v) by Th10
.= 'not' 'not'(Valid('not'(q '&' t) '&' 'not' 'not' (p '&' t), J).v) by
Th10
.= (Valid('not'(q '&' t),J).v) '&' (Valid('not' 'not' (p '&' t), J).v)
by Th12
.= 'not'(Valid(q '&' t,J).v) '&' (Valid('not' 'not' (p '&' t), J).v) by
Th10
.= 'not'(Valid(q '&' t,J).v) '&'('not'(Valid('not' (p '&' t), J).v)) by
Th10
.= 'not'(Valid(q '&' t,J).v) '&'('not' 'not' (Valid(p '&' t, J).v)) by Th10
.= 'not'((Valid(q,J).v) '&' (Valid(t,J).v)) '&' (Valid(p '&' t, J).v) by
Th12
.= 'not'((Valid(q,J).v) '&' (Valid(t,J).v)) '&' ((Valid(p,J).v) '&' (
Valid(t,J).v)) by Th12;
hence
Valid((p => q) => ('not'(q '&' t) => 'not'(p '&' t)), J).v = TRUE by A1,A2
,Lm2;
end;
theorem
J,v |= p & J,v |= (p => q) implies J,v |= q by Th24;
theorem Th38:
J,v |= All(x,p) => p
proof
thus Valid(All(x,p) => p, J).v = TRUE
proof
assume not Valid(All(x,p) => p, J).v = TRUE;
then
A1: Valid(All(x,p) => p, J).v = FALSE by XBOOLEAN:def 3;
Valid(All(x,p) => p, J).v = Valid('not'(All(x,p) '&' 'not' p), J).v by
QC_LANG2:def 2
.= 'not'(Valid(All(x,p) '&' 'not' p, J).v) by Th10
.= 'not'((Valid(All(x,p), J).v) '&' (Valid('not' p, J).v)) by Th12
.= 'not'((Valid(All(x,p), J).v) '&' 'not' (Valid(p, J).v)) by Th10;
then
A2: (Valid(All(x,p), J).v) '&' 'not'(Valid(p, J).v) = TRUE by A1,MARGREL1:11;
then 'not' (Valid(p, J).v) = TRUE by MARGREL1:12;
then
A3: Valid(p, J).v = FALSE by MARGREL1:11;
Valid(All(x,p), J).v=TRUE by A2,MARGREL1:12;
then FOR_ALL(x, Valid(p,J)).v = TRUE by Lm1;
hence thesis by A3,Th25;
end;
end;
theorem
J |= VERUM(Al)
by Th32;
theorem
J |= p '&' q => q '&' p
by Th33;
theorem
J |= ('not' p => p) => p
by Th34;
theorem
J |= p => ('not' p => q)
by Th35;
theorem
J |= (p => q) => ('not'(q '&' t) => 'not'(p '&' t))
by Th36;
theorem
J |= p & J |= (p => q) implies J |= q
proof
assume
A1: J |= p & J |= p => q;
now
let v;
J,v |= p & J,v |= p => q by A1;
hence J,v |= q by Th24;
end;
hence thesis;
end;
theorem
J |= All(x,p) => p
by Th38;
theorem
J |= p => q & not x in still_not-bound_in p implies J |= p => All(x,q)
proof
assume that
A1: for v holds J,v |= p => q and
A2: not x in still_not-bound_in p;
let u;
now
assume
A3: J,u |= p;
now
let w;
assume for y st x<>y holds w.y = u.y;
then
A4: J,w |= p by A2,A3,Th28;
J,w |= p => q by A1;
hence J,w |= q by A4,Th24;
end;
hence J,u |= All(x,q) by Th29;
end;
hence thesis by Th24;
end;
theorem
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
let s be QC-formula of Al;
assume that
A1: p = s.x and
A2: q = s.y and
A3: not x in still_not-bound_in s and
A4: J |= p;
now
assume
A5: x <> y;
A6: now
let u;
consider w being Element of Valuations_in(Al,A) such that
A7: (for z being bound_QC-variable of Al st z <> x holds w.z = u.z) & w.x
= u.y by Lm3;
w.x = w.y by A7;
then
A8: Valid(p,J).w = Valid(q,J).w by A1,A2,Th30;
J,w |= p by A4;
then
A9: Valid(p,J).w = TRUE;
not x in still_not-bound_in q by A2,A3,A5,Th31;
hence Valid(q,J).u = TRUE by A7,A8,A9,Th27;
end;
for v holds J,v |= q by A6;
hence thesis;
end;
hence thesis by A1,A2,A4;
end;