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