let Al be QC-alphabet ; for Al2 being Al -expanding QC-alphabet
for PHI being Consistent Subset of (CQC-WFF Al2) st PHI is Subset of (CQC-WFF Al) holds
PHI is Al -Consistent
let Al2 be Al -expanding QC-alphabet ; for PHI being Consistent Subset of (CQC-WFF Al2) st PHI is Subset of (CQC-WFF Al) holds
PHI is Al -Consistent
let PHI be Consistent Subset of (CQC-WFF Al2); ( PHI is Subset of (CQC-WFF Al) implies PHI is Al -Consistent )
assume
PHI is Subset of (CQC-WFF Al)
; PHI is Al -Consistent
for S being Subset of (CQC-WFF Al) st PHI = S holds
S is Consistent
proof
let S be
Subset of
(CQC-WFF Al);
( PHI = S implies S is Consistent )
assume A1:
PHI = S
;
S is Consistent
assume A2:
S is
Inconsistent
;
contradiction
PHI |- 'not' (VERUM Al2)
proof
consider f being
FinSequence of
CQC-WFF Al such that A3:
(
rng f c= S &
|- f ^ <*('not' (VERUM Al))*> )
by A2, GOEDELCP:24, HENMODEL:def 1;
set f2 =
f;
for
x being
object st
x in rng f holds
x in CQC-WFF Al2
then reconsider f2 =
f as
FinSequence of
CQC-WFF Al2 by FINSEQ_1:def 4, TARSKI:def 3;
consider PR being
FinSequence of
[:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] such that A5:
(
PR is
a_proof &
f ^ <*('not' (VERUM Al))*> = (PR . (len PR)) `1 )
by A3, CALCUL_1:def 9;
A6:
(
PR <> {} & ( for
n being
Nat st 1
<= n &
n <= len PR holds
PR,
n is_a_correct_step ) )
by A5, CALCUL_1:def 8;
set PR2 =
PR;
PR is
FinSequence of
[:(set_of_CQC-WFF-seq Al2),Proof_Step_Kinds:]
then reconsider PR2 =
PR as
FinSequence of
[:(set_of_CQC-WFF-seq Al2),Proof_Step_Kinds:] ;
A8:
PR2 is
a_proof
proof
for
n being
Nat st 1
<= n &
n <= len PR2 holds
PR2,
n is_a_correct_step
proof
let n be
Nat;
( 1 <= n & n <= len PR2 implies PR2,n is_a_correct_step )
assume A9:
( 1
<= n &
n <= len PR2 )
;
PR2,n is_a_correct_step
A10:
( ( for
i being
Nat st 1
<= i &
i < n holds
(PR2 . i) `1 in set_of_CQC-WFF-seq Al2 ) &
(PR2 . n) `1 in set_of_CQC-WFF-seq Al2 )
A13:
PR,
n is_a_correct_step
by A5, CALCUL_1:def 8, A9;
not not
(PR . n) `2 = 0 & ... & not
(PR . n) `2 = 9
by CALCUL_1:31, A9;
per cases then
( (PR2 . n) `2 = 0 or (PR2 . n) `2 = 1 or (PR2 . n) `2 = 2 or (PR2 . n) `2 = 3 or (PR2 . n) `2 = 4 or (PR2 . n) `2 = 5 or (PR2 . n) `2 = 6 or (PR2 . n) `2 = 7 or (PR2 . n) `2 = 8 or (PR2 . n) `2 = 9 )
;
suppose A18:
(PR2 . n) `2 = 1
;
PR2,n is_a_correct_step then consider g2 being
FinSequence of
CQC-WFF Al such that A19:
(PR . n) `1 = g2 ^ <*(VERUM Al)*>
by A13, CALCUL_1:def 7;
g2 ^ <*(VERUM Al)*> is
FinSequence of
CQC-WFF Al2
by A10, A19, CALCUL_1:def 6;
then consider gp being
FinSequence of
CQC-WFF Al2 such that A20:
gp = g2 ^ <*(VERUM Al)*>
;
len gp <> 0
by A20;
then consider g being
FinSequence of
CQC-WFF Al2,
v being
Element of
CQC-WFF Al2 such that A21:
gp = g ^ <*v*>
by FINSEQ_2:19;
v = VERUM Al2
by A20, A21, FINSEQ_2:17;
hence
PR2,
n is_a_correct_step
by A18, A19, A20, A21, CALCUL_1:def 7;
verum end; suppose A22:
(PR2 . n) `2 = 2
;
PR2,n is_a_correct_step then consider i being
Nat,
g2,
h2 being
FinSequence of
CQC-WFF Al such that A23:
( 1
<= i &
i < n &
Ant g2 is_Subsequence_of Ant h2 &
Suc g2 = Suc h2 &
(PR2 . i) `1 = g2 &
(PR2 . n) `1 = h2 )
by A13, CALCUL_1:def 7;
(
g2 in set_of_CQC-WFF-seq Al2 &
h2 in set_of_CQC-WFF-seq Al2 )
by A10, A23;
then
(
h2 is
FinSequence of
CQC-WFF Al2 &
g2 is
FinSequence of
CQC-WFF Al2 )
by CALCUL_1:def 6;
then consider g,
h being
FinSequence of
CQC-WFF Al2 such that A24:
(
g = g2 &
h = h2 )
;
A25:
Suc g =
Suc g2
by A24, Th11
.=
Suc h
by A23, A24, Th11
;
consider N being
Subset of
NAT such that A26:
Ant g2 c= Seq ((Ant h2) | N)
by A23, CALCUL_1:def 4;
(Ant h2) | N = (Ant h) | N
by A24, Th11;
then
Ant g c= Seq ((Ant h) | N)
by A24, A26, Th11;
then A27:
Ant g is_Subsequence_of Ant h
by CALCUL_1:def 4;
thus
PR2,
n is_a_correct_step
by A22, A23, A24, A25, A27, CALCUL_1:def 7;
verum end; suppose A28:
(PR2 . n) `2 = 3
;
PR2,n is_a_correct_step then consider i,
j being
Nat,
g,
h being
FinSequence of
CQC-WFF Al such that A29:
( 1
<= i &
i < n & 1
<= j &
j < i &
len g > 1 &
len h > 1 &
Ant (Ant g) = Ant (Ant h) &
'not' (Suc (Ant g)) = Suc (Ant h) &
Suc g = Suc h &
g = (PR2 . j) `1 &
h = (PR2 . i) `1 &
(Ant (Ant g)) ^ <*(Suc g)*> = (PR2 . n) `1 )
by A13, CALCUL_1:def 7;
(
(PR2 . j) `1 = g &
(PR2 . i) `1 = h &
j < n )
by A29, XXREAL_0:2;
then
(
g in set_of_CQC-WFF-seq Al2 &
h in set_of_CQC-WFF-seq Al2 )
by A10, A29;
then
(
h is
FinSequence of
CQC-WFF Al2 &
g is
FinSequence of
CQC-WFF Al2 )
by CALCUL_1:def 6;
then consider g2,
h2 being
FinSequence of
CQC-WFF Al2 such that A30:
(
g2 = g &
h2 = h )
;
A31:
(
Ant g2 = Ant g &
Ant h2 = Ant h )
by A30, Th11;
then A32:
Ant (Ant g2) =
Ant (Ant g)
by Th11
.=
Ant (Ant h2)
by A29, A31, Th11
;
A33:
'not' (Suc (Ant g2)) =
'not' (Al2 -Cast (Suc (Ant g)))
by A31, Th11
.=
Suc (Ant h2)
by A29, A31, Th11
;
A34:
Suc g2 =
Suc g
by A30, Th11
.=
Suc h2
by A29, A30, Th11
;
A35:
(PR2 . n) `1 =
(Ant (Ant g)) ^ <*(Suc g2)*>
by A29, A30, Th11
.=
(Ant (Ant g2)) ^ <*(Suc g2)*>
by A31, Th11
;
thus
PR2,
n is_a_correct_step
by A28, A29, A30, A32, A33, A34, A35, CALCUL_1:def 7;
verum end; suppose A36:
(PR2 . n) `2 = 4
;
PR2,n is_a_correct_step then consider i,
j being
Nat,
g,
h being
FinSequence of
CQC-WFF Al,
p being
Element of
CQC-WFF Al such that A37:
( 1
<= i &
i < n & 1
<= j &
j < i &
len g > 1 &
Ant g = Ant h &
Suc (Ant g) = 'not' p &
'not' (Suc g) = Suc h &
g = (PR2 . j) `1 &
h = (PR2 . i) `1 &
(Ant (Ant g)) ^ <*p*> = (PR2 . n) `1 )
by A13, CALCUL_1:def 7;
(
(PR2 . j) `1 = g &
(PR2 . i) `1 = h &
j < n )
by A37, XXREAL_0:2;
then
(
g in set_of_CQC-WFF-seq Al2 &
h in set_of_CQC-WFF-seq Al2 )
by A10, A37;
then
(
h is
FinSequence of
CQC-WFF Al2 &
g is
FinSequence of
CQC-WFF Al2 )
by CALCUL_1:def 6;
then consider g2,
h2 being
FinSequence of
CQC-WFF Al2 such that A38:
(
g2 = g &
h2 = h )
;
A39:
Ant g2 =
Ant g
by A38, Th11
.=
Ant h2
by A37, A38, Th11
;
Ant g2 = Ant g
by A38, Th11;
then A40:
Suc (Ant g2) = 'not' (Al2 -Cast p)
by A37, Th11;
A41:
'not' (Suc g2) =
'not' (Al2 -Cast (Suc g))
by A38, Th11
.=
Suc h2
by A37, A38, Th11
;
Ant g2 = Ant g
by A38, Th11;
then
(Ant (Ant g2)) ^ <*(Al2 -Cast p)*> = (PR2 . n) `1
by Th11, A37;
hence
PR2,
n is_a_correct_step
by A36, A37, A38, A39, A40, A41, CALCUL_1:def 7;
verum end; suppose A42:
(PR2 . n) `2 = 5
;
PR2,n is_a_correct_step then consider i,
j being
Nat,
g,
h being
FinSequence of
CQC-WFF Al such that A43:
( 1
<= i &
i < n & 1
<= j &
j < i &
Ant g = Ant h &
g = (PR2 . j) `1 &
h = (PR2 . i) `1 &
(Ant g) ^ <*((Suc g) '&' (Suc h))*> = (PR2 . n) `1 )
by A13, CALCUL_1:def 7;
(
(PR2 . j) `1 = g &
(PR2 . i) `1 = h &
j < n )
by A43, XXREAL_0:2;
then
(
g in set_of_CQC-WFF-seq Al2 &
h in set_of_CQC-WFF-seq Al2 )
by A10, A43;
then
(
h is
FinSequence of
CQC-WFF Al2 &
g is
FinSequence of
CQC-WFF Al2 )
by CALCUL_1:def 6;
then consider g2,
h2 being
FinSequence of
CQC-WFF Al2 such that A44:
(
g = g2 &
h = h2 )
;
(
Al2 -Cast (Suc g) = Suc g2 &
Al2 -Cast (Suc h) = Suc h2 )
by A44, Th11;
then A45:
(Ant g2) ^ <*((Suc g2) '&' (Suc h2))*> = (PR2 . n) `1
by A43, A44, Th11;
Ant g2 =
Ant g
by A44, Th11
.=
Ant h2
by A43, A44, Th11
;
hence
PR2,
n is_a_correct_step
by A42, A43, A44, A45, CALCUL_1:def 7;
verum end; suppose A46:
(PR2 . n) `2 = 6
;
PR2,n is_a_correct_step then consider i being
Nat,
g being
FinSequence of
CQC-WFF Al,
p,
q being
Element of
CQC-WFF Al such that A47:
( 1
<= i &
i < n &
p '&' q = Suc g &
g = (PR2 . i) `1 &
(Ant g) ^ <*p*> = (PR2 . n) `1 )
by A13, CALCUL_1:def 7;
g in set_of_CQC-WFF-seq Al2
by A10, A47;
then
g is
FinSequence of
CQC-WFF Al2
by CALCUL_1:def 6;
then consider g2 being
FinSequence of
CQC-WFF Al2 such that A48:
g = g2
;
A49:
Suc g2 = (Al2 -Cast p) '&' (Al2 -Cast q)
by A47, A48, Th11;
(Ant g2) ^ <*p*> = (PR2 . n) `1
by A47, A48, Th11;
hence
PR2,
n is_a_correct_step
by A46, A47, A48, A49, CALCUL_1:def 7;
verum end; suppose A50:
(PR2 . n) `2 = 7
;
PR2,n is_a_correct_step then consider i being
Nat,
g being
FinSequence of
CQC-WFF Al,
p,
q being
Element of
CQC-WFF Al such that A51:
( 1
<= i &
i < n &
p '&' q = Suc g &
g = (PR2 . i) `1 &
(Ant g) ^ <*q*> = (PR2 . n) `1 )
by A13, CALCUL_1:def 7;
g in set_of_CQC-WFF-seq Al2
by A10, A51;
then
g is
FinSequence of
CQC-WFF Al2
by CALCUL_1:def 6;
then reconsider g2 =
g as
FinSequence of
CQC-WFF Al2 ;
A52:
Suc g2 = (Al2 -Cast p) '&' (Al2 -Cast q)
by A51, Th11;
(Ant g2) ^ <*(Al2 -Cast q)*> = (PR2 . n) `1
by A51, Th11;
hence
PR2,
n is_a_correct_step
by A50, A51, A52, CALCUL_1:def 7;
verum end; suppose A53:
(PR2 . n) `2 = 8
;
PR2,n is_a_correct_step then consider i being
Nat,
g being
FinSequence of
CQC-WFF Al,
p being
Element of
CQC-WFF Al,
x,
y being
bound_QC-variable of
Al such that A54:
( 1
<= i &
i < n &
Suc g = All (
x,
p) &
g = (PR2 . i) `1 &
(Ant g) ^ <*(p . (x,y))*> = (PR2 . n) `1 )
by A13, CALCUL_1:def 7;
g in set_of_CQC-WFF-seq Al2
by A10, A54;
then
g is
FinSequence of
CQC-WFF Al2
by CALCUL_1:def 6;
then consider g2 being
FinSequence of
CQC-WFF Al2 such that A55:
g = g2
;
(
p is
Element of
CQC-WFF Al2 &
x is
bound_QC-variable of
Al2 &
y is
bound_QC-variable of
Al2 )
by Th4, Th7, TARSKI:def 3;
then consider q being
Element of
CQC-WFF Al2,
a,
b being
bound_QC-variable of
Al2 such that A56:
(
a = x &
b = y &
q = p )
;
A57:
(PR2 . n) `1 =
(Ant g) ^ <*(q . (a,b))*>
by A54, A56, Th17
.=
(Ant g2) ^ <*(q . (a,b))*>
by A55, Th11
;
Suc g2 = All (
a,
q)
by A54, A55, A56, Th11;
hence
PR2,
n is_a_correct_step
by A53, A54, A55, A57, CALCUL_1:def 7;
verum end; suppose A58:
(PR2 . n) `2 = 9
;
PR2,n is_a_correct_step then consider i being
Nat,
g being
FinSequence of
CQC-WFF Al,
p being
Element of
CQC-WFF Al,
x,
y being
bound_QC-variable of
Al such that A59:
( 1
<= i &
i < n &
Suc g = p . (
x,
y) & not
y in still_not-bound_in (Ant g) & not
y in still_not-bound_in (All (x,p)) &
g = (PR2 . i) `1 &
(Ant g) ^ <*(All (x,p))*> = (PR2 . n) `1 )
by A13, CALCUL_1:def 7;
g in set_of_CQC-WFF-seq Al2
by A10, A59;
then
g is
FinSequence of
CQC-WFF Al2
by CALCUL_1:def 6;
then consider g2 being
FinSequence of
CQC-WFF Al2 such that A60:
g = g2
;
(
p is
Element of
CQC-WFF Al2 &
x is
bound_QC-variable of
Al2 &
y is
bound_QC-variable of
Al2 )
by Th4, Th7, TARSKI:def 3;
then consider q being
Element of
CQC-WFF Al2,
a,
b being
bound_QC-variable of
Al2 such that A61:
(
q = p &
a = x &
b = y )
;
A62:
Suc g2 =
Suc g
by A60, Th11
.=
q . (
a,
b)
by A59, A61, Th17
;
A63:
still_not-bound_in (All (x,p)) =
still_not-bound_in (Al2 -Cast (All (x,p)))
by Th12
.=
still_not-bound_in (All (a,q))
by A61
;
A64:
not
b in still_not-bound_in (Ant g2)
proof
assume
b in still_not-bound_in (Ant g2)
;
contradiction
then consider i being
Nat,
r being
Element of
CQC-WFF Al2 such that A65:
(
i in dom (Ant g2) &
r = (Ant g2) . i &
b in still_not-bound_in r )
by CALCUL_1:def 5;
A66:
dom (Ant g2) = dom (Ant g)
by A60, Th11;
r = (Ant g) . i
by A60, A65, Th11;
then reconsider r =
r as
Element of
CQC-WFF Al by A65, A66, FINSEQ_2:11;
(
i in dom (Ant g) &
Al2 -Cast r = (Ant g) . i &
b in still_not-bound_in (Al2 -Cast r) )
by A60, A65, Th11;
then
(
i in dom (Ant g) &
r = (Ant g) . i &
y in still_not-bound_in r )
by A61, Th12;
hence
contradiction
by A59, CALCUL_1:def 5;
verum
end;
(Ant g2) ^ <*(All (a,q))*> = (PR2 . n) `1
by A59, A60, A61, Th11;
hence
PR2,
n is_a_correct_step
by A58, A59, A60, A61, A62, A63, A64, CALCUL_1:def 7;
verum end; end;
end;
hence
PR2 is
a_proof
by A6, CALCUL_1:def 8;
verum
end;
|- f2 ^ <*('not' (VERUM Al2))*>
by A5, A8, CALCUL_1:def 9;
hence
PHI |- 'not' (VERUM Al2)
by A1, A3, HENMODEL:def 1;
verum
end;
hence
contradiction
by GOEDELCP:24;
verum
end;
hence
PHI is Al -Consistent
; verum