let Al be QC-alphabet ; for p being Element of CQC-WFF Al
for X being Subset of (CQC-WFF Al) st p is_formal_provable_from X holds
X |= p
let p be Element of CQC-WFF Al; for X being Subset of (CQC-WFF Al) st p is_formal_provable_from X holds
X |= p
let X be Subset of (CQC-WFF Al); ( p is_formal_provable_from X implies X |= p )
assume
p is_formal_provable_from X
; X |= p
then consider f being FinSequence of CQC-WFF Al such that
A1:
rng (Ant f) c= X
and
A2:
Suc f = p
and
A3:
|- f
;
consider PR being FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] such that
A4:
PR is a_proof
and
A5:
f = (PR . (len PR)) `1
by A3;
PR <> {}
by A4;
then A6:
1 <= len PR
by FINSEQ_1:20;
defpred S1[ Nat] means ( $1 <= len PR implies for m being Nat st 1 <= m & m <= $1 holds
ex g being FinSequence of CQC-WFF Al st
( g = (PR . m) `1 & Ant g |= Suc g ) );
A7:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A8:
S1[
k]
;
S1[k + 1]
assume A9:
k + 1
<= len PR
;
for m being Nat st 1 <= m & m <= k + 1 holds
ex g being FinSequence of CQC-WFF Al st
( g = (PR . m) `1 & Ant g |= Suc g )
A10:
k <= k + 1
by NAT_1:11;
let m be
Nat;
( 1 <= m & m <= k + 1 implies ex g being FinSequence of CQC-WFF Al st
( g = (PR . m) `1 & Ant g |= Suc g ) )
assume that A11:
1
<= m
and A12:
m <= k + 1
;
ex g being FinSequence of CQC-WFF Al st
( g = (PR . m) `1 & Ant g |= Suc g )
A13:
m <= len PR
by A9, A12, XXREAL_0:2;
A14:
now ( m = k + 1 implies ex g being object st
( g = (PR . m) `1 & ex g being FinSequence of CQC-WFF Al st
( g = (PR . m) `1 & Ant g |= Suc g ) ) )assume A15:
m = k + 1
;
ex g being object st
( g = (PR . m) `1 & ex g being FinSequence of CQC-WFF Al st
( g = (PR . m) `1 & Ant g |= Suc g ) )take g =
(PR . m) `1 ;
( g = (PR . m) `1 & ex g being FinSequence of CQC-WFF Al st
( g = (PR . m) `1 & Ant g |= Suc g ) )thus
g = (PR . m) `1
;
ex g being FinSequence of CQC-WFF Al st
( g = (PR . m) `1 & Ant g |= Suc g )reconsider g =
(PR . m) `1 as
FinSequence of
CQC-WFF Al by A11, A13, Lm3;
A16:
PR,
m is_a_correct_step
by A4, A11, A13;
now Ant g |= Suc g
not not
(PR . m) `2 = 0 & ... & not
(PR . m) `2 = 9
by A11, A13, Th31;
per cases then
( (PR . m) `2 = 0 or (PR . m) `2 = 1 or (PR . m) `2 = 2 or (PR . m) `2 = 3 or (PR . m) `2 = 4 or (PR . m) `2 = 5 or (PR . m) `2 = 6 or (PR . m) `2 = 7 or (PR . m) `2 = 8 or (PR . m) `2 = 9 )
;
suppose
(PR . m) `2 = 2
;
Ant g |= Suc gthen consider i being
Nat,
f,
f1 being
FinSequence of
CQC-WFF Al such that A17:
1
<= i
and A18:
i < m
and A19:
(
Ant f is_Subsequence_of Ant f1 &
Suc f = Suc f1 &
(PR . i) `1 = f &
(PR . m) `1 = f1 )
by A16, Def7;
i <= k
by A15, A18, NAT_1:13;
then
ex
h being
FinSequence of
CQC-WFF Al st
(
h = (PR . i) `1 &
Ant h |= Suc h )
by A8, A9, A10, A17, XXREAL_0:2;
hence
Ant g |= Suc g
by A19, Th16;
verum end; suppose
(PR . m) `2 = 3
;
Ant g |= Suc gthen consider i,
j being
Nat,
f,
f1 being
FinSequence of
CQC-WFF Al such that A20:
1
<= i
and A21:
i < m
and A22:
1
<= j
and A23:
j < i
and A24:
(
len f > 1 &
len f1 > 1 &
Ant (Ant f) = Ant (Ant f1) &
'not' (Suc (Ant f)) = Suc (Ant f1) &
Suc f = Suc f1 &
f = (PR . j) `1 &
f1 = (PR . i) `1 )
and A25:
(Ant (Ant f)) ^ <*(Suc f)*> = (PR . m) `1
by A16, Def7;
A26:
(
Ant g = Ant (Ant f) &
Suc g = Suc f )
by A25, Th5;
A27:
i <= k
by A15, A21, NAT_1:13;
then
j <= k
by A23, XXREAL_0:2;
then A28:
ex
h1 being
FinSequence of
CQC-WFF Al st
(
h1 = (PR . j) `1 &
Ant h1 |= Suc h1 )
by A8, A9, A10, A22, XXREAL_0:2;
ex
h being
FinSequence of
CQC-WFF Al st
(
h = (PR . i) `1 &
Ant h |= Suc h )
by A8, A9, A10, A20, A27, XXREAL_0:2;
hence
Ant g |= Suc g
by A24, A28, A26, Th18;
verum end; suppose
(PR . m) `2 = 4
;
Ant g |= Suc gthen consider i,
j being
Nat,
f,
f1 being
FinSequence of
CQC-WFF Al,
p being
Element of
CQC-WFF Al such that A29:
1
<= i
and A30:
i < m
and A31:
1
<= j
and A32:
j < i
and A33:
(
len f > 1 &
Ant f = Ant f1 &
Suc (Ant f) = 'not' p &
'not' (Suc f) = Suc f1 &
f = (PR . j) `1 &
f1 = (PR . i) `1 )
and A34:
(Ant (Ant f)) ^ <*p*> = (PR . m) `1
by A16, Def7;
A35:
(
Ant g = Ant (Ant f) &
Suc g = p )
by A34, Th5;
A36:
i <= k
by A15, A30, NAT_1:13;
then
j <= k
by A32, XXREAL_0:2;
then A37:
ex
h1 being
FinSequence of
CQC-WFF Al st
(
h1 = (PR . j) `1 &
Ant h1 |= Suc h1 )
by A8, A9, A10, A31, XXREAL_0:2;
ex
h being
FinSequence of
CQC-WFF Al st
(
h = (PR . i) `1 &
Ant h |= Suc h )
by A8, A9, A10, A29, A36, XXREAL_0:2;
hence
Ant g |= Suc g
by A33, A37, A35, Th19;
verum end; suppose
(PR . m) `2 = 5
;
Ant g |= Suc gthen consider i,
j being
Nat,
f,
f1 being
FinSequence of
CQC-WFF Al such that A38:
1
<= i
and A39:
i < m
and A40:
1
<= j
and A41:
j < i
and A42:
(
Ant f = Ant f1 &
f = (PR . j) `1 &
f1 = (PR . i) `1 )
and A43:
(Ant f) ^ <*((Suc f) '&' (Suc f1))*> = (PR . m) `1
by A16, Def7;
A44:
(
Ant g = Ant f &
Suc g = (Suc f) '&' (Suc f1) )
by A43, Th5;
A45:
i <= k
by A15, A39, NAT_1:13;
then
j <= k
by A41, XXREAL_0:2;
then A46:
ex
h1 being
FinSequence of
CQC-WFF Al st
(
h1 = (PR . j) `1 &
Ant h1 |= Suc h1 )
by A8, A9, A10, A40, XXREAL_0:2;
ex
h being
FinSequence of
CQC-WFF Al st
(
h = (PR . i) `1 &
Ant h |= Suc h )
by A8, A9, A10, A38, A45, XXREAL_0:2;
hence
Ant g |= Suc g
by A42, A46, A44, Th20;
verum end; suppose
(PR . m) `2 = 6
;
Ant g |= Suc gthen consider i being
Nat,
f being
FinSequence of
CQC-WFF Al,
p,
q being
Element of
CQC-WFF Al such that A47:
1
<= i
and A48:
i < m
and A49:
(
p '&' q = Suc f &
f = (PR . i) `1 )
and A50:
(Ant f) ^ <*p*> = (PR . m) `1
by A16, Def7;
i <= k
by A15, A48, NAT_1:13;
then A51:
ex
h being
FinSequence of
CQC-WFF Al st
(
h = (PR . i) `1 &
Ant h |= Suc h )
by A8, A9, A10, A47, XXREAL_0:2;
(
Ant g = Ant f &
Suc g = p )
by A50, Th5;
hence
Ant g |= Suc g
by A49, A51, Th21;
verum end; suppose
(PR . m) `2 = 7
;
Ant g |= Suc gthen consider i being
Nat,
f being
FinSequence of
CQC-WFF Al,
p,
q being
Element of
CQC-WFF Al such that A52:
1
<= i
and A53:
i < m
and A54:
(
p '&' q = Suc f &
f = (PR . i) `1 )
and A55:
(Ant f) ^ <*q*> = (PR . m) `1
by A16, Def7;
i <= k
by A15, A53, NAT_1:13;
then A56:
ex
h being
FinSequence of
CQC-WFF Al st
(
h = (PR . i) `1 &
Ant h |= Suc h )
by A8, A9, A10, A52, XXREAL_0:2;
(
Ant g = Ant f &
Suc g = q )
by A55, Th5;
hence
Ant g |= Suc g
by A54, A56, Th22;
verum end; suppose
(PR . m) `2 = 8
;
Ant g |= Suc gthen consider i being
Nat,
f being
FinSequence of
CQC-WFF Al,
p being
Element of
CQC-WFF Al,
x,
y being
bound_QC-variable of
Al such that A57:
1
<= i
and A58:
i < m
and A59:
(
Suc f = All (
x,
p) &
f = (PR . i) `1 )
and A60:
(Ant f) ^ <*(p . (x,y))*> = (PR . m) `1
by A16, Def7;
i <= k
by A15, A58, NAT_1:13;
then A61:
ex
h being
FinSequence of
CQC-WFF Al st
(
h = (PR . i) `1 &
Ant h |= Suc h )
by A8, A9, A10, A57, XXREAL_0:2;
(
Ant g = Ant f &
Suc g = p . (
x,
y) )
by A60, Th5;
hence
Ant g |= Suc g
by A59, A61, Th25;
verum end; suppose
(PR . m) `2 = 9
;
Ant g |= Suc gthen consider i being
Nat,
f being
FinSequence of
CQC-WFF Al,
p being
Element of
CQC-WFF Al,
x,
y being
bound_QC-variable of
Al such that A62:
1
<= i
and A63:
i < m
and A64:
(
Suc f = p . (
x,
y) & not
y in still_not-bound_in (Ant f) & not
y in still_not-bound_in (All (x,p)) &
f = (PR . i) `1 )
and A65:
(Ant f) ^ <*(All (x,p))*> = (PR . m) `1
by A16, Def7;
i <= k
by A15, A63, NAT_1:13;
then A66:
ex
h being
FinSequence of
CQC-WFF Al st
(
h = (PR . i) `1 &
Ant h |= Suc h )
by A8, A9, A10, A62, XXREAL_0:2;
(
Ant g = Ant f &
Suc g = All (
x,
p) )
by A65, Th5;
hence
Ant g |= Suc g
by A64, A66, Th29;
verum end; hence
ex
g being
FinSequence of
CQC-WFF Al st
(
g = (PR . m) `1 &
Ant g |= Suc g )
;
verum end;
(
m <= k implies ex
g being
FinSequence of
CQC-WFF Al st
(
g = (PR . m) `1 &
Ant g |= Suc g ) )
by A8, A9, A11, A10, XXREAL_0:2;
hence
ex
g being
FinSequence of
CQC-WFF Al st
(
g = (PR . m) `1 &
Ant g |= Suc g )
by A12, A14, NAT_1:8;
verum
end;
A67:
S1[ 0 ]
;
for k being Nat holds S1[k]
from NAT_1:sch 2(A67, A7);
then consider g being FinSequence of CQC-WFF Al such that
A68:
g = (PR . (len PR)) `1
and
A69:
Ant g |= Suc g
by A6;
let A be non empty set ; CALCUL_1:def 12 for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) st J,v |= X holds
J,v |= p
let J be interpretation of Al,A; for v being Element of Valuations_in (Al,A) st J,v |= X holds
J,v |= p
let v be Element of Valuations_in (Al,A); ( J,v |= X implies J,v |= p )
assume
J,v |= X
; J,v |= p
then
for p being Element of CQC-WFF Al st p in rng (Ant f) holds
J,v |= p
by A1;
then
J,v |= rng (Ant f)
;
then
J,v |= Ant g
by A5, A68;
hence
J,v |= p
by A2, A5, A68, A69; verum