let Al be QC-alphabet ; for CX being Consistent Subset of (CQC-WFF Al)
for JH being Henkin_interpretation of CX
for n being Nat st ( for p being Element of CQC-WFF Al st QuantNbr p <= n & CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= p iff CX |- p ) ) holds
for p being Element of CQC-WFF Al st QuantNbr p <= n + 1 & CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= p iff CX |- p )
let CX be Consistent Subset of (CQC-WFF Al); for JH being Henkin_interpretation of CX
for n being Nat st ( for p being Element of CQC-WFF Al st QuantNbr p <= n & CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= p iff CX |- p ) ) holds
for p being Element of CQC-WFF Al st QuantNbr p <= n + 1 & CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= p iff CX |- p )
let JH be Henkin_interpretation of CX; for n being Nat st ( for p being Element of CQC-WFF Al st QuantNbr p <= n & CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= p iff CX |- p ) ) holds
for p being Element of CQC-WFF Al st QuantNbr p <= n + 1 & CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= p iff CX |- p )
let n be Nat; ( ( for p being Element of CQC-WFF Al st QuantNbr p <= n & CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= p iff CX |- p ) ) implies for p being Element of CQC-WFF Al st QuantNbr p <= n + 1 & CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= p iff CX |- p ) )
assume A1:
for p being Element of CQC-WFF Al st QuantNbr p <= n & CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= p iff CX |- p )
; for p being Element of CQC-WFF Al st QuantNbr p <= n + 1 & CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= p iff CX |- p )
let p be Element of CQC-WFF Al; ( QuantNbr p <= n + 1 & CX is negation_faithful & CX is with_examples implies ( JH, valH Al |= p iff CX |- p ) )
assume that
A2:
QuantNbr p <= n + 1
and
A3:
CX is negation_faithful
and
A4:
CX is with_examples
; ( JH, valH Al |= p iff CX |- p )
A5:
( QuantNbr p <= n implies ( JH, valH Al |= p iff CX |- p ) )
by A1, A3, A4;
now ( QuantNbr p = n + 1 implies ( JH, valH Al |= p iff CX |- p ) )assume A6:
QuantNbr p = n + 1
;
( JH, valH Al |= p iff CX |- p )then consider q being
Element of
CQC-WFF Al such that A7:
q is_subformula_of p
and A8:
QuantNbr q = 1
by NAT_1:11, SUBSTUT2:34;
set L = the
PATH of
q,
p;
A9:
1
<= len the
PATH of
q,
p
by A7, SUBSTUT2:def 5;
defpred S1[
Nat]
means ( 1
<= $1 & $1
<= len the
PATH of
q,
p implies ex
p1 being
Element of
CQC-WFF Al st
(
p1 = the
PATH of
q,
p . $1 &
QuantNbr q <= QuantNbr p1 & (
CX |- p1 implies
JH,
valH Al |= p1 ) & (
JH,
valH Al |= p1 implies
CX |- p1 ) ) );
A10:
S1[
0 ]
;
A11:
for
k being
Nat st
S1[
k] holds
S1[
k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A12:
S1[
k]
;
S1[k + 1]
assume that A13:
1
<= k + 1
and A14:
k + 1
<= len the
PATH of
q,
p
;
ex p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . (k + 1) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- p1 ) )
set j =
k + 1;
A15:
now ( k = 0 implies ex q, p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . (k + 1) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- p1 ) ) )assume
k = 0
;
ex q, p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . (k + 1) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- p1 ) )then A16:
the
PATH of
q,
p . (k + 1) = q
by A7, SUBSTUT2:def 5;
take q =
q;
ex p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . (k + 1) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- p1 ) )
(
JH,
valH Al |= q iff
CX |- q )
by A3, A4, A8, Th15;
hence
ex
p1 being
Element of
CQC-WFF Al st
(
p1 = the
PATH of
q,
p . (k + 1) &
QuantNbr q <= QuantNbr p1 & (
CX |- p1 implies
JH,
valH Al |= p1 ) & (
JH,
valH Al |= p1 implies
CX |- p1 ) )
by A16;
verum end;
now ( k <> 0 implies ex s, p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . (k + 1) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- p1 ) ) )assume
k <> 0
;
ex s, p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . (k + 1) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- p1 ) )then
0 < k
by NAT_1:3;
then A17:
0 + 1
<= k
by NAT_1:13;
k < len the
PATH of
q,
p
by A14, NAT_1:13;
then consider G1,
H1 being
Element of
QC-WFF Al such that A18:
the
PATH of
q,
p . k = G1
and A19:
the
PATH of
q,
p . (k + 1) = H1
and A20:
G1 is_immediate_constituent_of H1
by A7, A17, SUBSTUT2:def 5;
consider p1 being
Element of
CQC-WFF Al such that A21:
QuantNbr q <= QuantNbr p1
and A22:
p1 = the
PATH of
q,
p . k
and A23:
(
CX |- p1 iff
JH,
valH Al |= p1 )
by A12, A14, A17, NAT_1:13;
A24:
ex
F3 being
QC-formula of
Al st
(
F3 = the
PATH of
q,
p . (k + 1) &
F3 is_subformula_of p )
by A7, A13, A14, SUBSTUT2:27;
reconsider s =
H1 as
Element of
CQC-WFF Al by A7, A13, A14, A19, SUBSTUT2:28;
take s =
s;
ex p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . (k + 1) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- p1 ) )A25:
now ( s = 'not' p1 implies ex p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . (k + 1) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- p1 ) ) )assume A26:
s = 'not' p1
;
ex p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . (k + 1) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- p1 ) )then A27:
QuantNbr q <= QuantNbr s
by A21, CQC_SIM1:16;
(
CX |- s iff
JH,
valH Al |= s )
by A3, A23, A26, HENMODEL:def 2, VALUAT_1:17;
hence
ex
p1 being
Element of
CQC-WFF Al st
(
p1 = the
PATH of
q,
p . (k + 1) &
QuantNbr q <= QuantNbr p1 & (
CX |- p1 implies
JH,
valH Al |= p1 ) & (
JH,
valH Al |= p1 implies
CX |- p1 ) )
by A19, A27;
verum end; A28:
QuantNbr s <= n + 1
by A6, A19, A24, SUBSTUT2:30;
A29:
now ( ex F1 being QC-formula of Al st s = p1 '&' F1 implies ex p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . (k + 1) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- p1 ) ) )given F1 being
QC-formula of
Al such that A30:
s = p1 '&' F1
;
ex p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . (k + 1) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- p1 ) )reconsider F1 =
F1 as
Element of
CQC-WFF Al by A30, CQC_LANG:9;
A31:
QuantNbr s = (QuantNbr p1) + (QuantNbr F1)
by A30, CQC_SIM1:17;
then
1
+ (QuantNbr F1) <= QuantNbr s
by A8, A21, XREAL_1:6;
then
1
+ (QuantNbr F1) <= n + 1
by A28, XXREAL_0:2;
then
((QuantNbr F1) + 1) + (- 1) <= (n + 1) + (- 1)
by XREAL_1:6;
then
(
CX |- F1 iff
JH,
valH Al |= F1 )
by A1, A3, A4;
then A32:
(
CX |- s iff
JH,
valH Al |= s )
by A23, A30, Th6, VALUAT_1:18;
QuantNbr p1 <= QuantNbr s
by A31, NAT_1:11;
then
QuantNbr q <= QuantNbr s
by A21, XXREAL_0:2;
hence
ex
p1 being
Element of
CQC-WFF Al st
(
p1 = the
PATH of
q,
p . (k + 1) &
QuantNbr q <= QuantNbr p1 & (
CX |- p1 implies
JH,
valH Al |= p1 ) & (
JH,
valH Al |= p1 implies
CX |- p1 ) )
by A19, A32;
verum end; A33:
now ( ex F1 being QC-formula of Al st s = F1 '&' p1 implies ex p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . (k + 1) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- p1 ) ) )given F1 being
QC-formula of
Al such that A34:
s = F1 '&' p1
;
ex p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . (k + 1) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- p1 ) )reconsider F1 =
F1 as
Element of
CQC-WFF Al by A34, CQC_LANG:9;
A35:
QuantNbr s = (QuantNbr p1) + (QuantNbr F1)
by A34, CQC_SIM1:17;
then
1
+ (QuantNbr F1) <= QuantNbr s
by A8, A21, XREAL_1:6;
then
1
+ (QuantNbr F1) <= n + 1
by A28, XXREAL_0:2;
then
((QuantNbr F1) + 1) + (- 1) <= (n + 1) + (- 1)
by XREAL_1:6;
then
(
CX |- F1 iff
JH,
valH Al |= F1 )
by A1, A3, A4;
then A36:
(
CX |- s iff
JH,
valH Al |= s )
by A23, A34, Th6, VALUAT_1:18;
QuantNbr p1 <= QuantNbr s
by A35, NAT_1:11;
then
QuantNbr q <= QuantNbr s
by A21, XXREAL_0:2;
hence
ex
p1 being
Element of
CQC-WFF Al st
(
p1 = the
PATH of
q,
p . (k + 1) &
QuantNbr q <= QuantNbr p1 & (
CX |- p1 implies
JH,
valH Al |= p1 ) & (
JH,
valH Al |= p1 implies
CX |- p1 ) )
by A19, A36;
verum end; now ( ex x being bound_QC-variable of Al st s = All (x,p1) implies ex p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . (k + 1) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- p1 ) ) )given x being
bound_QC-variable of
Al such that A37:
s = All (
x,
p1)
;
ex p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . (k + 1) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- p1 ) )A38:
QuantNbr s = (QuantNbr p1) + 1
by A37, CQC_SIM1:18;
then
QuantNbr p1 < n + 1
by A28, NAT_1:13;
then
QuantNbr p1 <= n
by NAT_1:13;
then A39:
QuantNbr ('not' p1) <= n
by CQC_SIM1:16;
A40:
QuantNbr q <= QuantNbr s
by A21, A38, NAT_1:13;
A41:
now ( JH, valH Al |= Ex (x,('not' p1)) implies CX |- Ex (x,('not' p1)) )assume
JH,
valH Al |= Ex (
x,
('not' p1))
;
CX |- Ex (x,('not' p1))then consider y being
bound_QC-variable of
Al such that A42:
JH,
valH Al |= ('not' p1) . (
x,
y)
by Th10;
QuantNbr (('not' p1) . (x,y)) <= n
by A39, Th14;
then
CX |- ('not' p1) . (
x,
y)
by A1, A3, A4, A42;
hence
CX |- Ex (
x,
('not' p1))
by A4, Th3;
verum end; now ( CX |- Ex (x,('not' p1)) implies JH, valH Al |= Ex (x,('not' p1)) )assume
CX |- Ex (
x,
('not' p1))
;
JH, valH Al |= Ex (x,('not' p1))then consider y being
bound_QC-variable of
Al such that A43:
CX |- ('not' p1) . (
x,
y)
by A4, Th3;
QuantNbr (('not' p1) . (x,y)) <= n
by A39, Th14;
then
JH,
valH Al |= ('not' p1) . (
x,
y)
by A1, A3, A4, A43;
hence
JH,
valH Al |= Ex (
x,
('not' p1))
by Th10;
verum end; then
(
JH,
valH Al |= 'not' (Ex (x,('not' p1))) iff
CX |- 'not' (Ex (x,('not' p1))) )
by A3, A41, HENMODEL:def 2, VALUAT_1:17;
then
(
JH,
valH Al |= s iff
CX |- s )
by A37, Th11, Th12;
hence
ex
p1 being
Element of
CQC-WFF Al st
(
p1 = the
PATH of
q,
p . (k + 1) &
QuantNbr q <= QuantNbr p1 & (
CX |- p1 implies
JH,
valH Al |= p1 ) & (
JH,
valH Al |= p1 implies
CX |- p1 ) )
by A19, A40;
verum end; hence
ex
p1 being
Element of
CQC-WFF Al st
(
p1 = the
PATH of
q,
p . (k + 1) &
QuantNbr q <= QuantNbr p1 & (
CX |- p1 implies
JH,
valH Al |= p1 ) & (
JH,
valH Al |= p1 implies
CX |- p1 ) )
by A18, A20, A22, A25, A29, A33, QC_LANG2:def 19;
verum end;
hence
ex
p1 being
Element of
CQC-WFF Al st
(
p1 = the
PATH of
q,
p . (k + 1) &
QuantNbr q <= QuantNbr p1 & (
CX |- p1 implies
JH,
valH Al |= p1 ) & (
JH,
valH Al |= p1 implies
CX |- p1 ) )
by A15;
verum
end;
for
k being
Nat holds
S1[
k]
from NAT_1:sch 2(A10, A11);
then
ex
p1 being
Element of
CQC-WFF Al st
(
p1 = the
PATH of
q,
p . (len the PATH of q,p) &
QuantNbr q <= QuantNbr p1 & (
CX |- p1 implies
JH,
valH Al |= p1 ) & (
JH,
valH Al |= p1 implies
CX |- p1 ) )
by A9;
hence
(
JH,
valH Al |= p iff
CX |- p )
by A7, SUBSTUT2:def 5;
verum end;
hence
( JH, valH Al |= p iff CX |- p )
by A2, A5, NAT_1:8; verum