let p be Element of CQC-WFF ; :: thesis: for X being Subset of CQC-WFF st p is_formal_provable_from X holds
X |= p
let X be Subset of CQC-WFF ; :: thesis: ( p is_formal_provable_from X implies X |= p )
assume
p is_formal_provable_from X
; :: thesis: X |= p
then consider f being FinSequence of CQC-WFF such that
A1:
( rng (Ant f) c= X & Suc f = p & |- f )
by Def10;
consider PR being FinSequence of [:set_of_CQC-WFF-seq ,Proof_Step_Kinds :] such that
A2:
( PR is a_proof & f = (PR . (len PR)) `1 )
by A1, Def9;
let A be non empty set ; :: according to CALCUL_1:def 12 :: thesis: for J being interpretation of A
for v being Element of Valuations_in A st J,v |= X holds
J,v |= p
let J be interpretation of A; :: thesis: for v being Element of Valuations_in A st J,v |= X holds
J,v |= p
let v be Element of Valuations_in A; :: thesis: ( J,v |= X implies J,v |= p )
assume A3:
J,v |= X
; :: thesis: J,v |= p
defpred S1[ Element of NAT ] means ( $1 <= len PR implies for m being Element of NAT st 1 <= m & m <= $1 holds
ex g being FinSequence of CQC-WFF st
( g = (PR . m) `1 & Ant g |= Suc g ) );
A4:
S1[ 0 ]
;
A5:
for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be
Element of
NAT ;
:: thesis: ( S1[k] implies S1[k + 1] )
assume A6:
S1[
k]
;
:: thesis: S1[k + 1]
assume A7:
k + 1
<= len PR
;
:: thesis: for m being Element of NAT st 1 <= m & m <= k + 1 holds
ex g being FinSequence of CQC-WFF st
( g = (PR . m) `1 & Ant g |= Suc g )
let m be
Element of
NAT ;
:: thesis: ( 1 <= m & m <= k + 1 implies ex g being FinSequence of CQC-WFF st
( g = (PR . m) `1 & Ant g |= Suc g ) )
assume A8:
( 1
<= m &
m <= k + 1 )
;
:: thesis: ex g being FinSequence of CQC-WFF st
( g = (PR . m) `1 & Ant g |= Suc g )
A9:
( 1
<= m &
m <= len PR )
by A7, A8, XXREAL_0:2;
A10:
k <= k + 1
by NAT_1:11;
then A11:
(
m <= k implies ex
g being
FinSequence of
CQC-WFF st
(
g = (PR . m) `1 &
Ant g |= Suc g ) )
by A6, A7, A8, XXREAL_0:2;
now assume A12:
m = k + 1
;
:: thesis: ex g being set st
( g = (PR . m) `1 & ex g being FinSequence of CQC-WFF st
( g = (PR . m) `1 & Ant g |= Suc g ) )take g =
(PR . m) `1 ;
:: thesis: ( g = (PR . m) `1 & ex g being FinSequence of CQC-WFF st
( g = (PR . m) `1 & Ant g |= Suc g ) )thus
g = (PR . m) `1
;
:: thesis: ex g being FinSequence of CQC-WFF st
( g = (PR . m) `1 & Ant g |= Suc g )reconsider g =
(PR . m) `1 as
FinSequence of
CQC-WFF by A9, Lm1;
A13:
PR,
m is_a_correct_step
by A2, A9, Def8;
now per cases
( (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 )
by A9, Th31;
suppose
(PR . m) `2 = 2
;
:: thesis: Ant g |= Suc gthen consider i being
Element of
NAT ,
f,
f1 being
FinSequence of
CQC-WFF such that A16:
( 1
<= i &
i < m &
Ant f is_Subsequence_of Ant f1 &
Suc f = Suc f1 &
(PR . i) `1 = f &
(PR . m) `1 = f1 )
by A13, Def7;
( 1
<= i &
i <= k )
by A12, A16, NAT_1:13;
then consider h being
FinSequence of
CQC-WFF such that A17:
(
h = (PR . i) `1 &
Ant h |= Suc h )
by A6, A7, A10, XXREAL_0:2;
thus
Ant g |= Suc g
by A16, A17, Th16;
:: thesis: verum end; suppose
(PR . m) `2 = 3
;
:: thesis: Ant g |= Suc gthen consider i,
j being
Element of
NAT ,
f,
f1 being
FinSequence of
CQC-WFF such that A18:
( 1
<= i &
i < m & 1
<= j &
j < i &
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 &
(Ant (Ant f)) ^ <*(Suc f)*> = (PR . m) `1 )
by A13, Def7;
A19:
( 1
<= i &
i <= k )
by A12, A18, NAT_1:13;
then consider h being
FinSequence of
CQC-WFF such that A20:
(
h = (PR . i) `1 &
Ant h |= Suc h )
by A6, A7, A10, XXREAL_0:2;
( 1
<= j &
j <= k )
by A18, A19, XXREAL_0:2;
then consider h1 being
FinSequence of
CQC-WFF such that A21:
(
h1 = (PR . j) `1 &
Ant h1 |= Suc h1 )
by A6, A7, A10, XXREAL_0:2;
(
Ant g = Ant (Ant f) &
Suc g = Suc f )
by A18, Th5;
hence
Ant g |= Suc g
by A18, A20, A21, Th18;
:: thesis: verum end; suppose
(PR . m) `2 = 4
;
:: thesis: Ant g |= Suc gthen consider i,
j being
Element of
NAT ,
f,
f1 being
FinSequence of
CQC-WFF ,
p being
Element of
CQC-WFF such that A22:
( 1
<= i &
i < m & 1
<= j &
j < i &
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 &
(Ant (Ant f)) ^ <*p*> = (PR . m) `1 )
by A13, Def7;
A23:
( 1
<= i &
i <= k )
by A12, A22, NAT_1:13;
then consider h being
FinSequence of
CQC-WFF such that A24:
(
h = (PR . i) `1 &
Ant h |= Suc h )
by A6, A7, A10, XXREAL_0:2;
( 1
<= j &
j <= k )
by A22, A23, XXREAL_0:2;
then consider h1 being
FinSequence of
CQC-WFF such that A25:
(
h1 = (PR . j) `1 &
Ant h1 |= Suc h1 )
by A6, A7, A10, XXREAL_0:2;
(
Ant g = Ant (Ant f) &
Suc g = p )
by A22, Th5;
hence
Ant g |= Suc g
by A22, A24, A25, Th19;
:: thesis: verum end; suppose
(PR . m) `2 = 5
;
:: thesis: Ant g |= Suc gthen consider i,
j being
Element of
NAT ,
f,
f1 being
FinSequence of
CQC-WFF such that A26:
( 1
<= i &
i < m & 1
<= j &
j < i &
Ant f = Ant f1 &
f = (PR . j) `1 &
f1 = (PR . i) `1 &
(Ant f) ^ <*((Suc f) '&' (Suc f1))*> = (PR . m) `1 )
by A13, Def7;
A27:
( 1
<= i &
i <= k )
by A12, A26, NAT_1:13;
then consider h being
FinSequence of
CQC-WFF such that A28:
(
h = (PR . i) `1 &
Ant h |= Suc h )
by A6, A7, A10, XXREAL_0:2;
( 1
<= j &
j <= k )
by A26, A27, XXREAL_0:2;
then consider h1 being
FinSequence of
CQC-WFF such that A29:
(
h1 = (PR . j) `1 &
Ant h1 |= Suc h1 )
by A6, A7, A10, XXREAL_0:2;
(
Ant g = Ant f &
Suc g = (Suc f) '&' (Suc f1) )
by A26, Th5;
hence
Ant g |= Suc g
by A26, A28, A29, Th20;
:: thesis: verum end; suppose
(PR . m) `2 = 6
;
:: thesis: Ant g |= Suc gthen consider i being
Element of
NAT ,
f being
FinSequence of
CQC-WFF ,
p,
q being
Element of
CQC-WFF such that A30:
( 1
<= i &
i < m &
p '&' q = Suc f &
f = (PR . i) `1 &
(Ant f) ^ <*p*> = (PR . m) `1 )
by A13, Def7;
( 1
<= i &
i <= k )
by A12, A30, NAT_1:13;
then consider h being
FinSequence of
CQC-WFF such that A31:
(
h = (PR . i) `1 &
Ant h |= Suc h )
by A6, A7, A10, XXREAL_0:2;
(
Ant g = Ant f &
Suc g = p )
by A30, Th5;
hence
Ant g |= Suc g
by A30, A31, Th21;
:: thesis: verum end; suppose
(PR . m) `2 = 7
;
:: thesis: Ant g |= Suc gthen consider i being
Element of
NAT ,
f being
FinSequence of
CQC-WFF ,
p,
q being
Element of
CQC-WFF such that A32:
( 1
<= i &
i < m &
p '&' q = Suc f &
f = (PR . i) `1 &
(Ant f) ^ <*q*> = (PR . m) `1 )
by A13, Def7;
( 1
<= i &
i <= k )
by A12, A32, NAT_1:13;
then consider h being
FinSequence of
CQC-WFF such that A33:
(
h = (PR . i) `1 &
Ant h |= Suc h )
by A6, A7, A10, XXREAL_0:2;
(
Ant g = Ant f &
Suc g = q )
by A32, Th5;
hence
Ant g |= Suc g
by A32, A33, Th22;
:: thesis: verum end; suppose
(PR . m) `2 = 8
;
:: thesis: Ant g |= Suc gthen consider i being
Element of
NAT ,
f being
FinSequence of
CQC-WFF ,
p being
Element of
CQC-WFF ,
x,
y being
bound_QC-variable such that A34:
( 1
<= i &
i < m &
Suc f = All x,
p &
f = (PR . i) `1 &
(Ant f) ^ <*(p . x,y)*> = (PR . m) `1 )
by A13, Def7;
( 1
<= i &
i <= k )
by A12, A34, NAT_1:13;
then consider h being
FinSequence of
CQC-WFF such that A35:
(
h = (PR . i) `1 &
Ant h |= Suc h )
by A6, A7, A10, XXREAL_0:2;
(
Ant g = Ant f &
Suc g = p . x,
y )
by A34, Th5;
hence
Ant g |= Suc g
by A34, A35, Th25;
:: thesis: verum end; suppose
(PR . m) `2 = 9
;
:: thesis: Ant g |= Suc gthen consider i being
Element of
NAT ,
f being
FinSequence of
CQC-WFF ,
p being
Element of
CQC-WFF ,
x,
y being
bound_QC-variable such that A36:
( 1
<= i &
i < m &
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 &
(Ant f) ^ <*(All x,p)*> = (PR . m) `1 )
by A13, Def7;
( 1
<= i &
i <= k )
by A12, A36, NAT_1:13;
then consider h being
FinSequence of
CQC-WFF such that A37:
(
h = (PR . i) `1 &
Ant h |= Suc h )
by A6, A7, A10, XXREAL_0:2;
(
Ant g = Ant f &
Suc g = All x,
p )
by A36, Th5;
hence
Ant g |= Suc g
by A36, A37, Th29;
:: thesis: verum end; hence
ex
g being
FinSequence of
CQC-WFF st
(
g = (PR . m) `1 &
Ant g |= Suc g )
;
:: thesis: verum end;
hence
ex
g being
FinSequence of
CQC-WFF st
(
g = (PR . m) `1 &
Ant g |= Suc g )
by A8, A11, NAT_1:8;
:: thesis: verum
end;
A38:
for k being Element of NAT holds S1[k]
from NAT_1:sch 1(A4, A5);
PR <> {}
by A2, Def8;
then
( 1 <= len PR & len PR <= len PR )
by FINSEQ_1:28;
then consider g being FinSequence of CQC-WFF such that
A39:
( g = (PR . (len PR)) `1 & Ant g |= Suc g )
by A38;
for p being Element of CQC-WFF st p in rng (Ant f) holds
J,v |= p
by A1, A3, Def11;
then
J,v |= rng (Ant f)
by Def11;
then
J,v |= Ant g
by A2, A39, Def14;
hence
J,v |= p
by A1, A2, A39, Def15; :: thesis: verum