let Al be QC-alphabet ; for PHI being Consistent Subset of (CQC-WFF Al) ex Al2 being Al -expanding QC-alphabet ex PSI being Consistent Subset of (CQC-WFF Al2) st
( PHI c= PSI & PSI is with_examples )
let PHI be Consistent Subset of (CQC-WFF Al); ex Al2 being Al -expanding QC-alphabet ex PSI being Consistent Subset of (CQC-WFF Al2) st
( PHI c= PSI & PSI is with_examples )
deffunc H1( Nat) -> Al -expanding QC-alphabet = $1 -th_FCEx Al;
deffunc H2( Nat) -> Subset of (CQC-WFF ($1 -th_FCEx Al)) = $1 -th_EF (Al,PHI);
set Al2 = union { H1(n) where n is Element of NAT : verum } ;
set PSI = union { H2(n) where n is Element of NAT : verum } ;
A1:
PHI c= union { H2(n) where n is Element of NAT : verum }
A2:
( Al c= union { H1(n) where n is Element of NAT : verum } & ( for n being Element of NAT holds H1(n) c= union { H1(n) where n is Element of NAT : verum } ) )
reconsider Al2 = union { H1(n) where n is Element of NAT : verum } as non empty set by A2;
set Al2sym = union { (QC-symbols H1(n)) where n is Element of NAT : verum } ;
( NAT c= union { (QC-symbols H1(n)) where n is Element of NAT : verum } & Al2 = [:NAT,(union { (QC-symbols H1(n)) where n is Element of NAT : verum } ):] )
proof
for
s being
object st
s in Al2 holds
s in [:NAT,(union { (QC-symbols H1(n)) where n is Element of NAT : verum } ):]
proof
let s be
object ;
( s in Al2 implies s in [:NAT,(union { (QC-symbols H1(n)) where n is Element of NAT : verum } ):] )
assume A3:
s in Al2
;
s in [:NAT,(union { (QC-symbols H1(n)) where n is Element of NAT : verum } ):]
consider P being
set such that A4:
(
s in P &
P in { H1(n) where n is Element of NAT : verum } )
by A3, TARSKI:def 4;
consider n being
Element of
NAT such that A5:
P = H1(
n)
by A4;
A6:
for
y being
set st
y in QC-symbols H1(
n) holds
y in union { (QC-symbols H1(n)) where n is Element of NAT : verum }
s in [:NAT,(QC-symbols H1(n)):]
by A5, A4, QC_LANG1:5;
then
ex
k,
y being
object st
(
k in NAT &
y in QC-symbols H1(
n) &
s = [k,y] )
by ZFMISC_1:def 2;
then
ex
k,
y being
set st
(
k in NAT &
y in union { (QC-symbols H1(n)) where n is Element of NAT : verum } &
s = [k,y] )
by A6;
hence
s in [:NAT,(union { (QC-symbols H1(n)) where n is Element of NAT : verum } ):]
by ZFMISC_1:87;
verum
end;
then A8:
Al2 c= [:NAT,(union { (QC-symbols H1(n)) where n is Element of NAT : verum } ):]
;
QC-symbols Al = QC-symbols H1(
0 )
by Def7;
then
QC-symbols Al in { (QC-symbols H1(n)) where n is Element of NAT : verum }
;
then
(
NAT c= QC-symbols Al &
QC-symbols Al c= union { (QC-symbols H1(n)) where n is Element of NAT : verum } )
by QC_LANG1:3, ZFMISC_1:74;
hence
NAT c= union { (QC-symbols H1(n)) where n is Element of NAT : verum }
;
Al2 = [:NAT,(union { (QC-symbols H1(n)) where n is Element of NAT : verum } ):]
for
x being
object st
x in [:NAT,(union { (QC-symbols H1(n)) where n is Element of NAT : verum } ):] holds
x in Al2
proof
let x be
object ;
( x in [:NAT,(union { (QC-symbols H1(n)) where n is Element of NAT : verum } ):] implies x in Al2 )
assume A9:
x in [:NAT,(union { (QC-symbols H1(n)) where n is Element of NAT : verum } ):]
;
x in Al2
consider m,
y being
object such that A10:
(
m in NAT &
y in union { (QC-symbols H1(n)) where n is Element of NAT : verum } &
x = [m,y] )
by A9, ZFMISC_1:def 2;
consider P being
set such that A11:
(
y in P &
P in { (QC-symbols H1(n)) where n is Element of NAT : verum } )
by A10, TARSKI:def 4;
consider n being
Element of
NAT such that A12:
P = QC-symbols H1(
n)
by A11;
[m,y] in [:NAT,(QC-symbols H1(n)):]
by A10, A11, A12, ZFMISC_1:87;
then A13:
[m,y] in H1(
n)
by QC_LANG1:5;
H1(
n)
c= Al2
by A2;
hence
x in Al2
by A10, A13;
verum
end;
then
[:NAT,(union { (QC-symbols H1(n)) where n is Element of NAT : verum } ):] c= Al2
;
hence
Al2 = [:NAT,(union { (QC-symbols H1(n)) where n is Element of NAT : verum } ):]
by A8, XBOOLE_0:def 10;
verum
end;
then reconsider Al2 = Al2 as QC-alphabet by QC_LANG1:def 1;
reconsider Al2 = Al2 as Al -expanding QC-alphabet by A2, QC_TRANS:def 1;
for p being object st p in union { H2(n) where n is Element of NAT : verum } holds
p in CQC-WFF Al2
then reconsider PSI = union { H2(n) where n is Element of NAT : verum } as Subset of (CQC-WFF Al2) by TARSKI:def 3;
PSI is Consistent
then reconsider PSI = PSI as Consistent Subset of (CQC-WFF Al2) ;
set S = { H1(n) where n is Element of NAT : verum } ;
H1( 0 ) in { H1(n) where n is Element of NAT : verum }
;
then reconsider S = { H1(n) where n is Element of NAT : verum } as non empty set ;
A39:
for a, b being set st a in S & b in S holds
ex c being set st
( a \/ b c= c & c in S )
A43:
for p being Element of CQC-WFF Al2 ex n being Element of NAT st p is Element of CQC-WFF H1(n)
proof
defpred S1[
Element of
CQC-WFF Al2]
means ex
n being
Element of
NAT st $1 is
Element of
CQC-WFF H1(
n);
A44:
S1[
VERUM Al2]
A45:
for
k being
Nat for
P being
QC-pred_symbol of
k,
Al2 for
l being
CQC-variable_list of
k,
Al2 holds
S1[
P ! l]
proof
let k be
Nat;
for P being QC-pred_symbol of k,Al2
for l being CQC-variable_list of k,Al2 holds S1[P ! l]let P be
QC-pred_symbol of
k,
Al2;
for l being CQC-variable_list of k,Al2 holds S1[P ! l]let l be
CQC-variable_list of
k,
Al2;
S1[P ! l]
ex
n being
Element of
NAT st
(
rng l c= bound_QC-variables H1(
n) &
P is
QC-pred_symbol of
k,
H1(
n) )
proof
A46:
(
rng l c= bound_QC-variables Al2 &
{P} c= QC-pred_symbols Al2 )
by ZFMISC_1:31;
(
bound_QC-variables Al2 c= QC-variables Al2 &
QC-variables Al2 c= [:NAT,(QC-symbols Al2):] )
by QC_LANG1:4;
then A47:
(
bound_QC-variables Al2 c= [:NAT,(QC-symbols Al2):] &
QC-pred_symbols Al2 c= [:NAT,(QC-symbols Al2):] )
by QC_LANG1:6;
then
(
rng l c= [:NAT,(QC-symbols Al2):] &
{P} c= [:NAT,(QC-symbols Al2):] )
by A46;
then
(
rng l c= Al2 &
{P} c= Al2 )
by QC_LANG1:5;
then
(
(rng l) \/ {P} c= union S &
(rng l) \/ {P} is
finite )
by XBOOLE_1:8;
then consider a being
set such that A48:
(
a in S &
(rng l) \/ {P} c= a )
by A39, COHSP_1:6, COHSP_1:13;
consider n being
Element of
NAT such that A49:
a = H1(
n)
by A48;
take
n
;
( rng l c= bound_QC-variables H1(n) & P is QC-pred_symbol of k,H1(n) )
A50:
(
rng l c= (rng l) \/ {P} &
{P} c= (rng l) \/ {P} )
by XBOOLE_1:7;
for
s being
object st
s in rng l holds
s in bound_QC-variables H1(
n)
proof
let s be
object ;
( s in rng l implies s in bound_QC-variables H1(n) )
assume A51:
s in rng l
;
s in bound_QC-variables H1(n)
s in bound_QC-variables Al2
by A51;
then
s in [:{4},(QC-symbols Al2):]
by QC_LANG1:def 4;
then consider s1,
s2 being
object such that A52:
(
s1 in {4} &
s2 in QC-symbols Al2 &
s = [s1,s2] )
by ZFMISC_1:def 2;
(
rng l c= H1(
n) &
{P} c= H1(
n) )
by A48, A49, A50;
then
s in H1(
n)
by A51;
then
s in [:NAT,(QC-symbols H1(n)):]
by QC_LANG1:5;
then consider s3,
s4 being
object such that A53:
(
s3 in NAT &
s4 in QC-symbols H1(
n) &
s = [s3,s4] )
by ZFMISC_1:def 2;
s = [s1,s4]
by A52, A53, XTUPLE_0:1;
then
s in [:{4},(QC-symbols H1(n)):]
by A52, A53, ZFMISC_1:def 2;
hence
s in bound_QC-variables H1(
n)
by QC_LANG1:def 4;
verum
end;
hence
rng l c= bound_QC-variables H1(
n)
;
P is QC-pred_symbol of k,H1(n)
thus
P is
QC-pred_symbol of
k,
H1(
n)
verumproof
P in [:NAT,(QC-symbols Al2):]
by A47;
then consider p1,
p2 being
object such that A54:
(
p1 in NAT &
p2 in QC-symbols Al2 &
P = [p1,p2] )
by ZFMISC_1:def 2;
(
rng l c= H1(
n) &
P in H1(
n) )
by A48, A49, A50, ZFMISC_1:31;
then
P in [:NAT,(QC-symbols H1(n)):]
by QC_LANG1:5;
then reconsider p2 =
p2 as
QC-symbol of
H1(
n)
by A54, ZFMISC_1:87;
A55:
P `1 =
(the_arity_of P) + 7
by QC_LANG1:def 8
.=
k + 7
by QC_LANG1:11
;
reconsider p1 =
p1 as
Element of
NAT by A54;
(
P `1 = 7
+ (the_arity_of P) &
P `1 = p1 )
by A54, QC_LANG1:def 8;
then
7
<= p1
by NAT_1:11;
then
[p1,p2] in { [m,x] where m is Nat, x is QC-symbol of H1(n) : 7 <= m }
;
then reconsider P =
P as
QC-pred_symbol of
H1(
n)
by A54, QC_LANG1:def 7;
the_arity_of P = k
by A55, QC_LANG1:def 8;
then
P in { Q where Q is QC-pred_symbol of H1(n) : the_arity_of Q = k }
;
hence
P is
QC-pred_symbol of
k,
H1(
n)
by QC_LANG1:def 9;
verum
end;
end;
then consider n being
Element of
NAT such that A56:
(
rng l c= bound_QC-variables H1(
n) &
P is
QC-pred_symbol of
k,
H1(
n) )
;
l is
CQC-variable_list of
k,
H1(
n)
by A56, FINSEQ_1:def 4, XBOOLE_1:1;
then consider l2 being
CQC-variable_list of
k,
H1(
n),
P2 being
QC-pred_symbol of
k,
H1(
n)
such that A57:
(
l2 = l &
P = P2 )
by A56;
reconsider Al2 =
Al2 as
H1(
n)
-expanding QC-alphabet by A2, QC_TRANS:def 1;
A58:
(
Al2 -Cast P2 = P &
Al2 -Cast l2 = l )
by A57, QC_TRANS:def 5, QC_TRANS:def 6;
P2 ! l2 =
Al2 -Cast (P2 ! l2)
by QC_TRANS:def 3
.=
P ! l
by A58, QC_TRANS:8
;
hence
S1[
P ! l]
;
verum
end;
A59:
for
r being
Element of
CQC-WFF Al2 st
S1[
r] holds
S1[
'not' r]
A62:
for
r,
s being
Element of
CQC-WFF Al2 st
S1[
r] &
S1[
s] holds
S1[
r '&' s]
for
x being
bound_QC-variable of
Al2 for
r being
Element of
CQC-WFF Al2 st
S1[
r] holds
S1[
All (
x,
r)]
proof
let x be
bound_QC-variable of
Al2;
for r being Element of CQC-WFF Al2 st S1[r] holds
S1[ All (x,r)]let r be
Element of
CQC-WFF Al2;
( S1[r] implies S1[ All (x,r)] )
(
x in QC-variables Al2 &
QC-variables Al2 c= [:NAT,(QC-symbols Al2):] )
by QC_LANG1:4;
then
(
x in [:NAT,(QC-symbols Al2):] &
Al2 = [:NAT,(QC-symbols Al2):] )
by QC_LANG1:5;
then
(
{x} c= union S &
{x} is
finite )
by ZFMISC_1:31;
then consider a being
set such that A68:
(
a in S &
{x} c= a )
by A39, COHSP_1:6, COHSP_1:13;
consider n being
Element of
NAT such that A69:
a = H1(
n)
by A68;
assume
S1[
r]
;
S1[ All (x,r)]
then consider m being
Element of
NAT such that A70:
r is
Element of
CQC-WFF H1(
m)
;
x in bound_QC-variables Al2
;
then
x in [:{4},(QC-symbols Al2):]
by QC_LANG1:def 4;
then consider x1,
x2 being
object such that A71:
(
x1 in {4} &
x2 in QC-symbols Al2 &
x = [x1,x2] )
by ZFMISC_1:def 2;
A72:
x in H1(
n)
by A68, A69, ZFMISC_1:31;
per cases
( n <= m or not n <= m )
;
suppose A73:
n <= m
;
S1[ All (x,r)]then reconsider Sm =
H1(
m) as
H1(
n)
-expanding QC-alphabet by Th6, QC_TRANS:def 1;
H1(
n)
c= H1(
m)
by A73, Th6;
then
x in H1(
m)
by A72;
then
x in [:NAT,(QC-symbols H1(m)):]
by QC_LANG1:5;
then consider x3,
x4 being
object such that A74:
(
x3 in NAT &
x4 in QC-symbols H1(
m) &
x = [x3,x4] )
by ZFMISC_1:def 2;
x = [x1,x4]
by A71, A74, XTUPLE_0:1;
then
x in [:{4},(QC-symbols Sm):]
by A71, A74, ZFMISC_1:def 2;
then
x is
bound_QC-variable of
Sm
by QC_LANG1:def 4;
then consider x2 being
bound_QC-variable of
Sm,
r2 being
Element of
CQC-WFF Sm such that A75:
(
x2 = x &
r2 = r )
by A70;
reconsider Al2 =
Al2 as
Sm -expanding QC-alphabet by A2, QC_TRANS:def 1;
A76:
(
r = Al2 -Cast r2 &
x = Al2 -Cast x2 )
by A75, QC_TRANS:def 3, QC_TRANS:def 4;
All (
x2,
r2) =
Al2 -Cast (All (x2,r2))
by QC_TRANS:def 3
.=
All (
x,
r)
by A76, QC_TRANS:8
;
hence
S1[
All (
x,
r)]
;
verum end; suppose
not
n <= m
;
S1[ All (x,r)]then reconsider Sn =
H1(
n) as
H1(
m)
-expanding QC-alphabet by Th6, QC_TRANS:def 1;
x in [:NAT,(QC-symbols Sn):]
by A72, QC_LANG1:5;
then consider x3,
x4 being
object such that A77:
(
x3 in NAT &
x4 in QC-symbols Sn &
x = [x3,x4] )
by ZFMISC_1:def 2;
x = [x1,x4]
by A71, A77, XTUPLE_0:1;
then
x in [:{4},(QC-symbols Sn):]
by A71, A77, ZFMISC_1:def 2;
then
(
x is
bound_QC-variable of
Sn &
r is
Element of
CQC-WFF Sn )
by A70, QC_TRANS:7, QC_LANG1:def 4;
then consider x2 being
bound_QC-variable of
Sn,
r2 being
Element of
CQC-WFF Sn such that A78:
(
x2 = x &
r2 = r )
;
reconsider Al2 =
Al2 as
Sn -expanding QC-alphabet by A2, QC_TRANS:def 1;
A79:
(
r = Al2 -Cast r2 &
x = Al2 -Cast x2 )
by A78, QC_TRANS:def 3, QC_TRANS:def 4;
All (
x2,
r2) =
Al2 -Cast (All (x2,r2))
by QC_TRANS:def 3
.=
All (
x,
r)
by A79, QC_TRANS:8
;
hence
S1[
All (
x,
r)]
;
verum end; end;
end;
then A80:
for
r,
s being
Element of
CQC-WFF Al2 for
x being
bound_QC-variable of
Al2 for
k being
Nat for
l being
CQC-variable_list of
k,
Al2 for
P being
QC-pred_symbol of
k,
Al2 holds
(
S1[
VERUM Al2] &
S1[
P ! l] & (
S1[
r] implies
S1[
'not' r] ) & (
S1[
r] &
S1[
s] implies
S1[
r '&' s] ) & (
S1[
r] implies
S1[
All (
x,
r)] ) )
by A44, A45, A59, A62;
for
p being
Element of
CQC-WFF Al2 holds
S1[
p]
from CQC_LANG:sch 1(A80);
hence
for
p being
Element of
CQC-WFF Al2 ex
n being
Element of
NAT st
p is
Element of
CQC-WFF H1(
n)
;
verum
end;
PSI is with_examples
proof
for
x being
bound_QC-variable of
Al2 for
p being
Element of
CQC-WFF Al2 ex
y being
bound_QC-variable of
Al2 st
PSI |- ('not' (Ex (x,p))) 'or' (p . (x,y))
proof
let x be
bound_QC-variable of
Al2;
for p being Element of CQC-WFF Al2 ex y being bound_QC-variable of Al2 st PSI |- ('not' (Ex (x,p))) 'or' (p . (x,y))let p be
Element of
CQC-WFF Al2;
ex y being bound_QC-variable of Al2 st PSI |- ('not' (Ex (x,p))) 'or' (p . (x,y))
ex
n being
Element of
NAT st
(
x is
bound_QC-variable of
H1(
n) &
p is
Element of
CQC-WFF H1(
n) )
proof
consider m being
Element of
NAT such that A81:
p is
Element of
CQC-WFF H1(
m)
by A43;
(
x in QC-variables Al2 &
QC-variables Al2 c= [:NAT,(QC-symbols Al2):] )
by QC_LANG1:4;
then
(
x in [:NAT,(QC-symbols Al2):] &
Al2 = [:NAT,(QC-symbols Al2):] )
by QC_LANG1:5;
then
(
{x} c= union S &
{x} is
finite )
by ZFMISC_1:31;
then consider a being
set such that A82:
(
a in S &
{x} c= a )
by A39, COHSP_1:6, COHSP_1:13;
consider n being
Element of
NAT such that A83:
a = H1(
n)
by A82;
x in bound_QC-variables Al2
;
then
x in [:{4},(QC-symbols Al2):]
by QC_LANG1:def 4;
then consider x1,
x2 being
object such that A84:
(
x1 in {4} &
x2 in QC-symbols Al2 &
x = [x1,x2] )
by ZFMISC_1:def 2;
A85:
x in H1(
n)
by A82, A83, ZFMISC_1:31;
per cases
( n <= m or not n <= m )
;
suppose A86:
n <= m
;
ex n being Element of NAT st
( x is bound_QC-variable of H1(n) & p is Element of CQC-WFF H1(n) )then reconsider Sm =
H1(
m) as
H1(
n)
-expanding QC-alphabet by Th6, QC_TRANS:def 1;
H1(
n)
c= H1(
m)
by A86, Th6;
then
x in H1(
m)
by A85;
then
x in [:NAT,(QC-symbols H1(m)):]
by QC_LANG1:5;
then consider x3,
x4 being
object such that A87:
(
x3 in NAT &
x4 in QC-symbols H1(
m) &
x = [x3,x4] )
by ZFMISC_1:def 2;
x = [x1,x4]
by A84, A87, XTUPLE_0:1;
then
x in [:{4},(QC-symbols Sm):]
by A84, A87, ZFMISC_1:def 2;
then
x is
bound_QC-variable of
Sm
by QC_LANG1:def 4;
hence
ex
n being
Element of
NAT st
(
x is
bound_QC-variable of
H1(
n) &
p is
Element of
CQC-WFF H1(
n) )
by A81;
verum end; suppose
not
n <= m
;
ex n being Element of NAT st
( x is bound_QC-variable of H1(n) & p is Element of CQC-WFF H1(n) )then reconsider Sn =
H1(
n) as
H1(
m)
-expanding QC-alphabet by Th6, QC_TRANS:def 1;
x in [:NAT,(QC-symbols H1(n)):]
by A85, QC_LANG1:5;
then consider x3,
x4 being
object such that A88:
(
x3 in NAT &
x4 in QC-symbols H1(
n) &
x = [x3,x4] )
by ZFMISC_1:def 2;
x = [x1,x4]
by A84, A88, XTUPLE_0:1;
then
x in [:{4},(QC-symbols Sn):]
by A84, A88, ZFMISC_1:def 2;
then
(
x is
bound_QC-variable of
Sn &
p is
Element of
CQC-WFF Sn )
by A81, QC_TRANS:7, QC_LANG1:def 4;
hence
ex
n being
Element of
NAT st
(
x is
bound_QC-variable of
H1(
n) &
p is
Element of
CQC-WFF H1(
n) )
;
verum end; end;
end;
then consider n being
Element of
NAT such that A89:
(
x is
bound_QC-variable of
H1(
n) &
p is
Element of
CQC-WFF H1(
n) )
;
A90:
FCEx H1(
n)
= H1(
n + 1)
by Th5;
A91:
H2(
n + 1)
= H2(
n)
\/ (Example_Formulae_of H1(n))
by Def9;
consider x2 being
bound_QC-variable of
H1(
n),
p2 being
Element of
CQC-WFF H1(
n)
such that A92:
(
x2 = x &
p2 = p )
by A89;
Example_Formula_of (
p2,
x2)
in Example_Formulae_of H1(
n)
;
then A93:
Example_Formula_of (
p2,
x2)
in H2(
n + 1)
by A91, XBOOLE_0:def 3;
H1(
n)
c= H1(
n + 1)
by Th6, NAT_1:11;
then reconsider Sn1 =
H1(
n + 1) as
H1(
n)
-expanding QC-alphabet by QC_TRANS:def 1;
set y2 =
Example_of (
p2,
x2);
reconsider y2 =
Example_of (
p2,
x2) as
bound_QC-variable of
Sn1 by Th5;
reconsider Al2 =
Al2 as
Sn1 -expanding QC-alphabet by A2, QC_TRANS:def 1;
y2 is
bound_QC-variable of
Al2
by TARSKI:def 3, QC_TRANS:4;
then consider y being
bound_QC-variable of
Al2 such that A94:
y = y2
;
A95:
(
Sn1 -Cast p2 = p &
Sn1 -Cast x2 = x )
by A92, QC_TRANS:def 3, QC_TRANS:def 4;
then A96:
(
Al2 -Cast (Sn1 -Cast p2) = p &
Al2 -Cast (Sn1 -Cast x2) = x )
by QC_TRANS:def 3, QC_TRANS:def 4;
A97:
Al2 -Cast (Ex ((Sn1 -Cast x2),(Sn1 -Cast p2))) = Ex (
x,
p)
by A96, Th7;
reconsider p =
p as
Element of
CQC-WFF Al2 ;
reconsider x =
x as
bound_QC-variable of
Al2 ;
A98:
(Sn1 -Cast p2) . (
(Sn1 -Cast x2),
y2)
= p . (
x,
y)
by A94, A95, QC_TRANS:17;
A99:
Example_Formula_of (
p2,
x2) =
Al2 -Cast (('not' (Ex ((Sn1 -Cast x2),(Sn1 -Cast p2)))) 'or' ((Sn1 -Cast p2) . ((Sn1 -Cast x2),y2)))
by A90, QC_TRANS:def 3
.=
(Al2 -Cast ('not' (Ex ((Sn1 -Cast x2),(Sn1 -Cast p2))))) 'or' (Al2 -Cast ((Sn1 -Cast p2) . ((Sn1 -Cast x2),y2)))
by Th7
.=
('not' (Al2 -Cast (Ex ((Sn1 -Cast x2),(Sn1 -Cast p2))))) 'or' (Al2 -Cast ((Sn1 -Cast p2) . ((Sn1 -Cast x2),y2)))
by QC_TRANS:8
.=
('not' (Ex (x,p))) 'or' (p . (x,y))
by A97, A98, QC_TRANS:def 3
;
set example =
('not' (Ex (x,p))) 'or' (p . (x,y));
reconsider example =
('not' (Ex (x,p))) 'or' (p . (x,y)) as
Element of
CQC-WFF Al2 ;
reconsider PSI =
PSI as
Consistent Subset of
(CQC-WFF Al2) ;
H2(
n + 1)
in { H2(m) where m is Element of NAT : verum }
;
then
H2(
n + 1)
c= PSI
by ZFMISC_1:74;
hence
ex
y being
bound_QC-variable of
Al2 st
PSI |- ('not' (Ex (x,p))) 'or' (p . (x,y))
by A93, A99, GOEDELCP:21;
verum
end;
hence
PSI is
with_examples
by GOEDELCP:def 2;
verum
end;
hence
ex Al2 being Al -expanding QC-alphabet ex PSI being Consistent Subset of (CQC-WFF Al2) st
( PHI c= PSI & PSI is with_examples )
by A1; verum