let A be Element of LTLB_WFF ; for P being consistent PNPair holds
( A in rng P or [((P `1) ^^ <*A*>),(P `2)] is consistent or [(P `1),((P `2) ^^ <*A*>)] is consistent )
let P be consistent PNPair; ( A in rng P or [((P `1) ^^ <*A*>),(P `2)] is consistent or [(P `1),((P `2) ^^ <*A*>)] is consistent )
set fpa = (P `1) ^^ <*A*>;
set fma = (P `2) ^^ <*A*>;
set Pl = [((P `1) ^^ <*A*>),(P `2)];
set Pr = [(P `1),((P `2) ^^ <*A*>)];
set np = 'not' (P ^);
set npl = 'not' ([((P `1) ^^ <*A*>),(P `2)] ^);
set npr = 'not' ([(P `1),((P `2) ^^ <*A*>)] ^);
set na = <*('not' A)*>;
assume A1:
not A in rng P
; ( [((P `1) ^^ <*A*>),(P `2)] is consistent or [(P `1),((P `2) ^^ <*A*>)] is consistent )
then
not A in rng (P `1)
by XBOOLE_0:def 3;
then
rng (P `1) misses {A}
by ZFMISC_1:50;
then
rng (P `1) misses rng <*A*>
by FINSEQ_1:39;
then A2:
(P `1) ^^ <*A*> = (P `1) ^ <*A*>
by Def3;
not A in rng (P `2)
by A1, XBOOLE_0:def 3;
then
rng (P `2) misses {A}
by ZFMISC_1:50;
then
rng (P `2) misses rng <*A*>
by FINSEQ_1:39;
then
(P `2) ^^ <*A*> = (P `2) ^ <*A*>
by Def3;
then A3:
nega ((P `2) ^^ <*A*>) = (nega (P `2)) ^ <*('not' A)*>
by LTLAXIO2:15;
('not' ([((P `1) ^^ <*A*>),(P `2)] ^)) => (('not' ([(P `1),((P `2) ^^ <*A*>)] ^)) => ('not' (P ^))) is ctaut
proof
let g be
Function of
LTLB_WFF,
BOOLEAN;
LTLAXIO1:def 16 (VAL g) . (('not' ([((P `1) ^^ <*A*>),(P `2)] ^)) => (('not' ([(P `1),((P `2) ^^ <*A*>)] ^)) => ('not' (P ^)))) = 1
set v =
VAL g;
set vf =
(VAL g) . TFALSUM;
A4:
(VAL g) . TFALSUM = 0
by LTLAXIO1:def 15;
set p =
(((VAL g) . (P ^)) '&' ((VAL g) . A)) => ((VAL g) . TFALSUM);
set q =
(((VAL g) . (P ^)) '&' (((VAL g) . A) => ((VAL g) . TFALSUM))) => ((VAL g) . TFALSUM);
A5:
(
(VAL g) . A = 1 or
(VAL g) . A = 0 )
by XBOOLEAN:def 3;
A6:
(VAL g) . ([(P `1),((P `2) ^^ <*A*>)] ^) =
((VAL g) . H2(P `1 )) '&' ((VAL g) . H2( nega ((P `2) ^^ <*A*>)))
by LTLAXIO1:31
.=
((VAL g) . H2(P `1 )) '&' (((VAL g) . H2( nega (P `2))) '&' ((VAL g) . H2(<*('not' A)*>)))
by LTLAXIO2:17, A3
.=
(((VAL g) . H2(P `1 )) '&' ((VAL g) . H2( nega (P `2)))) '&' ((VAL g) . H2(<*('not' A)*>))
.=
((VAL g) . (P ^)) '&' ((VAL g) . H2(<*('not' A)*>))
by LTLAXIO1:31
.=
((VAL g) . (P ^)) '&' ((VAL g) . ('not' A))
by LTLAXIO2:11
.=
((VAL g) . (P ^)) '&' (((VAL g) . A) => ((VAL g) . TFALSUM))
by LTLAXIO1:def 15
;
A7:
(VAL g) . ([((P `1) ^^ <*A*>),(P `2)] ^) =
((VAL g) . H2((P `1) ^^ <*A*>)) '&' ((VAL g) . H2( nega (P `2)))
by LTLAXIO1:31
.=
(((VAL g) . H2(P `1 )) '&' ((VAL g) . H2(<*A*>))) '&' ((VAL g) . H2( nega (P `2)))
by LTLAXIO2:17, A2
.=
(((VAL g) . H2(P `1 )) '&' ((VAL g) . A)) '&' ((VAL g) . H2( nega (P `2)))
by LTLAXIO2:11
.=
(((VAL g) . H2(P `1 )) '&' ((VAL g) . H2( nega (P `2)))) '&' ((VAL g) . A)
.=
((VAL g) . (P ^)) '&' ((VAL g) . A)
by LTLAXIO1:31
;
A8:
(
(VAL g) . (P ^) = 1 or
(VAL g) . (P ^) = 0 )
by XBOOLEAN:def 3;
thus (VAL g) . (('not' ([((P `1) ^^ <*A*>),(P `2)] ^)) => (('not' ([(P `1),((P `2) ^^ <*A*>)] ^)) => ('not' (P ^)))) =
((VAL g) . ('not' ([((P `1) ^^ <*A*>),(P `2)] ^))) => ((VAL g) . (('not' ([(P `1),((P `2) ^^ <*A*>)] ^)) => ('not' (P ^))))
by LTLAXIO1:def 15
.=
((VAL g) . ('not' ([((P `1) ^^ <*A*>),(P `2)] ^))) => (((VAL g) . ('not' ([(P `1),((P `2) ^^ <*A*>)] ^))) => ((VAL g) . ('not' (P ^))))
by LTLAXIO1:def 15
.=
((((VAL g) . (P ^)) '&' ((VAL g) . A)) => ((VAL g) . TFALSUM)) => (((VAL g) . ('not' ([(P `1),((P `2) ^^ <*A*>)] ^))) => ((VAL g) . ('not' (P ^))))
by A7, LTLAXIO1:def 15
.=
((((VAL g) . (P ^)) '&' ((VAL g) . A)) => ((VAL g) . TFALSUM)) => (((((VAL g) . (P ^)) '&' (((VAL g) . A) => ((VAL g) . TFALSUM))) => ((VAL g) . TFALSUM)) => ((VAL g) . ('not' (P ^))))
by A6, LTLAXIO1:def 15
.=
1
by A8, A5, A4, LTLAXIO1:def 15
;
verum
end;
then
('not' ([((P `1) ^^ <*A*>),(P `2)] ^)) => (('not' ([(P `1),((P `2) ^^ <*A*>)] ^)) => ('not' (P ^))) in LTL_axioms
by LTLAXIO1:def 17;
then A9:
{} LTLB_WFF |- ('not' ([((P `1) ^^ <*A*>),(P `2)] ^)) => (('not' ([(P `1),((P `2) ^^ <*A*>)] ^)) => ('not' (P ^)))
by LTLAXIO1:42;
assume that
A10:
[((P `1) ^^ <*A*>),(P `2)] is Inconsistent
and
A11:
[(P `1),((P `2) ^^ <*A*>)] is Inconsistent
; contradiction
{} LTLB_WFF |- 'not' ([((P `1) ^^ <*A*>),(P `2)] ^)
by A10;
then A12:
{} LTLB_WFF |- ('not' ([(P `1),((P `2) ^^ <*A*>)] ^)) => ('not' (P ^))
by A9, LTLAXIO1:43;
{} LTLB_WFF |- 'not' ([(P `1),((P `2) ^^ <*A*>)] ^)
by A11;
hence
contradiction
by A12, Def10, LTLAXIO1:43; verum