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