:: Weak Completeness Theorem for Propositional Linear Time Temporal Logic
:: by Mariusz Giero
::
:: Received May 7, 2012
:: Copyright (c) 2012-2021 Association of Mizar Users

set l = LTLB_WFF ;

set pairs = [:(LTLB_WFF **),(LTLB_WFF **):];

deffunc H₁( FinSequence of LTLB_WFF ) -> Element of LTLB_WFF = 'not' ((con (nega $1)) /. (len (con (nega $1))));

deffunc H₂( FinSequence of LTLB_WFF ) -> Element of LTLB_WFF = (con $1) /. (len (con $1));

definition

let X be finite set ;
:: original: Enumeration
redefine mode Enumeration of X -> one-to-one FinSequence of X;
coherence
for b₁ being Enumeration of X holds b₁ is one-to-one FinSequence of X

proof end;

end;

definition

let E be set ;
let F be finite Subset of E;
:: original: Enumeration
redefine mode Enumeration of F -> one-to-one FinSequence of E;
coherence
for b₁ being Enumeration of F holds b₁ is one-to-one FinSequence of E

proof end;

end;

registration

let D be set ;

cluster non empty functional finite FinSequence-membered for FinSequenceSet of D;

existence
ex b₁ being FinSequenceSet of D st
( not b₁ is empty & b₁ is finite )

proof end;

end;

theorem Th1: :: LTLAXIO4:1

for X being set
for G being non empty finite FinSequenceSet of X ex A being FinSequence st
( A in G & ( for B being FinSequence st B in G holds
len B <= len A ) )

proof end;

definition

let T be DecoratedTree;
let n be Element of NAT ;
let t be Node of T;
:: original: |
redefine func t | n -> Node of T;
correctness
coherence
t | n is Node of T;

proof end;

end;

theorem Th2: :: LTLAXIO4:2

for p being Element of LTLB_WFF holds p is FinSequence of NAT

proof end;

notation

let A be Element of LTLB_WFF ;
synonym s-until A for conjunctive ;

end;

definition

let A be Element of LTLB_WFF ;
assume A1: A is s-until ;

func rarg A -> Element of LTLB_WFF means :Def1: :: LTLAXIO4:def 1
ex p being Element of LTLB_WFF st p 'U' it = A;

existence
ex b₁, p being Element of LTLB_WFF st p 'U' b₁ = A

proof end;

uniqueness
for b₁, b₂ being Element of LTLB_WFF st ex p being Element of LTLB_WFF st p 'U' b₁ = A & ex p being Element of LTLB_WFF st p 'U' b₂ = A holds
b₁ = b₂ by HILBERT2:19;

end;

:: deftheorem Def1 defines rarg LTLAXIO4:def 1 :
for A being Element of LTLB_WFF st A is s-until holds
for b₂ being Element of LTLB_WFF holds
( b₂ = rarg A iff ex p being Element of LTLB_WFF st p 'U' b₂ = A );

definition

let A be Element of LTLB_WFF ;

attr A is satisfiable means :: LTLAXIO4:def 2
ex M being LTLModel ex n being Element of NAT st (SAT M) . [n,A] = 1;

end;

:: deftheorem defines satisfiable LTLAXIO4:def 2 :
for A being Element of LTLB_WFF holds
( A is satisfiable iff ex M being LTLModel ex n being Element of NAT st (SAT M) . [n,A] = 1 );

theorem Th3: :: LTLAXIO4:3

for A being Element of LTLB_WFF holds
( {} LTLB_WFF |= A iff not 'not' A is satisfiable )

proof end;

theorem Th4: :: LTLAXIO4:4

for A being Element of LTLB_WFF st TVERUM '&&' A is satisfiable holds
A is satisfiable

proof end;

theorem Th5: :: LTLAXIO4:5

for p, q being Element of LTLB_WFF
for M being LTLModel
for i being Element of NAT holds
( (SAT M) . [i,(p 'U' q)] = 1 iff ex j being Element of NAT st
( j > i & (SAT M) . [j,q] = 1 & ( for k being Element of NAT st i < k & k < j holds
(SAT M) . [k,p] = 1 ) ) )

proof end;

theorem Th6: :: LTLAXIO4:6

for M being LTLModel
for n being Element of NAT
for f being FinSequence of LTLB_WFF holds
( (SAT M) . [n,((con f) /. (len (con f)))] = 1 iff for i being Nat st i in dom f holds
(SAT M) . [n,(f /. i)] = 1 )

proof end;

theorem Th7: :: LTLAXIO4:7

for A being Element of LTLB_WFF holds [(<*> LTLB_WFF),<*A*>] ^ = TVERUM '&&' ('not' A)

proof end;

theorem Th8: :: LTLAXIO4:8

for A, B being Element of LTLB_WFF
for P being complete PNPair st untn (A,B) in rng P holds
( A in rng P & B in rng P & A 'U' B in rng P )

proof end;

theorem Th9: :: LTLAXIO4:9

for P being PNPair holds rng P c= union (Subt (rng P))

proof end;

definition

let F be Subset of [:(LTLB_WFF **),(LTLB_WFF **):];

func F ^ -> Subset of LTLB_WFF equals :: LTLAXIO4:def 3
{ (P ^) where P is Element of [:(LTLB_WFF **),(LTLB_WFF **):] : P in F } ;

coherence
{ (P ^) where P is Element of [:(LTLB_WFF **),(LTLB_WFF **):] : P in F } is Subset of LTLB_WFF

proof end;

end;

:: deftheorem defines ^ LTLAXIO4:def 3 :
for F being Subset of [:(LTLB_WFF **),(LTLB_WFF **):] holds F ^ = { (P ^) where P is Element of [:(LTLB_WFF **),(LTLB_WFF **):] : P in F } ;

registration

let F be non empty Subset of [:(LTLB_WFF **),(LTLB_WFF **):];

cluster F ^ -> non empty ;

coherence
not F ^ is empty

proof end;

end;

registration

let F be finite Subset of [:(LTLB_WFF **),(LTLB_WFF **):];

cluster F ^ -> finite ;

coherence
F ^ is finite

proof end;

end;

theorem Th10: :: LTLAXIO4:10

for F, G being Subset of [:(LTLB_WFF **),(LTLB_WFF **):] holds (F \/ G) ^ = (F ^) \/ (G ^)

proof end;

theorem Th11: :: LTLAXIO4:11

{[(<*> LTLB_WFF),(<*> LTLB_WFF)]} ^ = {(TVERUM '&&' TVERUM)}

proof end;

definition

let F be finite Subset of LTLB_WFF;

func comp F -> non empty finite Subset of [:(LTLB_WFF **),(LTLB_WFF **):] equals :: LTLAXIO4:def 4
{ Q where Q is PNPair : ( rng Q = tau F & rng (Q `1) misses rng (Q `2) ) } ;

coherence
{ Q where Q is PNPair : ( rng Q = tau F & rng (Q `1) misses rng (Q `2) ) } is non empty finite Subset of [:(LTLB_WFF **),(LTLB_WFF **):]

proof end;

end;

:: deftheorem defines comp LTLAXIO4:def 4 :
for F being finite Subset of LTLB_WFF holds comp F = { Q where Q is PNPair : ( rng Q = tau F & rng (Q `1) misses rng (Q `2) ) } ;

registration

let F be finite Subset of LTLB_WFF;

cluster -> complete for Element of comp F;

coherence
for b₁ being Element of comp F holds b₁ is complete

proof end;

end;

theorem Th12: :: LTLAXIO4:12

comp ({} LTLB_WFF) = {[(<*> LTLB_WFF),(<*> LTLB_WFF)]}

proof end;

definition

let P, Q be PNPair;

pred Q is_completion_of P means :: LTLAXIO4:def 5
( rng (P `1) c= rng (Q `1) & rng (P `2) c= rng (Q `2) & tau (rng P) = rng Q );

end;

:: deftheorem defines is_completion_of LTLAXIO4:def 5 :
for P, Q being PNPair holds
( Q is_completion_of P iff ( rng (P `1) c= rng (Q `1) & rng (P `2) c= rng (Q `2) & tau (rng P) = rng Q ) );

theorem Th13: :: LTLAXIO4:13

for P, Q being PNPair st Q is_completion_of P holds
Q is complete by LTLAXIO3:17;

definition

let P be PNPair;

func comp P -> finite Subset of [:(LTLB_WFF **),(LTLB_WFF **):] equals :: LTLAXIO4:def 6
{ Q where Q is consistent PNPair : Q is_completion_of P } ;

coherence
{ Q where Q is consistent PNPair : Q is_completion_of P } is finite Subset of [:(LTLB_WFF **),(LTLB_WFF **):]

proof end;

end;

:: deftheorem defines comp LTLAXIO4:def 6 :
for P being PNPair holds comp P = { Q where Q is consistent PNPair : Q is_completion_of P } ;

registration

let P be consistent PNPair;

cluster comp P -> non empty finite ;

coherence
not comp P is empty

proof end;

end;

registration

let P be consistent PNPair;

cluster -> consistent for Element of comp P;

coherence
for b₁ being Element of comp P holds b₁ is consistent

proof end;

end;

definition

let X be Subset of [:(LTLB_WFF **),(LTLB_WFF **):];

func comp X -> Subset of [:(LTLB_WFF **),(LTLB_WFF **):] equals :: LTLAXIO4:def 7
union { (comp P) where P is Element of [:(LTLB_WFF **),(LTLB_WFF **):] : P in X } ;

coherence
union { (comp P) where P is Element of [:(LTLB_WFF **),(LTLB_WFF **):] : P in X } is Subset of [:(LTLB_WFF **),(LTLB_WFF **):]

proof end;

end;

:: deftheorem defines comp LTLAXIO4:def 7 :
for X being Subset of [:(LTLB_WFF **),(LTLB_WFF **):] holds comp X = union { (comp P) where P is Element of [:(LTLB_WFF **),(LTLB_WFF **):] : P in X } ;

registration

let X be finite Subset of [:(LTLB_WFF **),(LTLB_WFF **):];

cluster comp X -> finite ;

coherence
comp X is finite

proof end;

end;

theorem Th14: :: LTLAXIO4:14

for Q being PNPair
for X being non empty Subset of [:(LTLB_WFF **),(LTLB_WFF **):] st Q in X holds
comp Q c= comp X

proof end;

theorem Th15: :: LTLAXIO4:15

for F being non empty finite Subset of LTLB_WFF ex p being Element of LTLB_WFF st
( p in tau F & tau ((tau F) \ {p}) = (tau F) \ {p} )

proof end;

theorem Th16: :: LTLAXIO4:16

for F being finite Subset of LTLB_WFF
for f being FinSequence of LTLB_WFF st rng f = (comp F) ^ holds
{} LTLB_WFF |- 'not' ((con (nega f)) /. (len (con (nega f))))

proof end;

theorem Th17: :: LTLAXIO4:17

for P being consistent PNPair
for f being FinSequence of LTLB_WFF st rng f = (comp P) ^ holds
{} LTLB_WFF |- (P ^) => ('not' ((con (nega f)) /. (len (con (nega f)))))

proof end;

definition

let X be Subset of LTLB_WFF;

func untn X -> Subset of LTLB_WFF equals :: LTLAXIO4:def 8
{ (untn (A,B)) where A, B is Element of LTLB_WFF : A 'U' B in X } ;

coherence
{ (untn (A,B)) where A, B is Element of LTLB_WFF : A 'U' B in X } is Subset of LTLB_WFF

proof end;

end;

:: deftheorem defines untn LTLAXIO4:def 8 :
for X being Subset of LTLB_WFF holds untn X = { (untn (A,B)) where A, B is Element of LTLB_WFF : A 'U' B in X } ;

registration

let X be finite Subset of LTLB_WFF;

cluster untn X -> finite ;

coherence
untn X is finite

proof end;

end;

definition

let P be PNPair;

func untn P -> non empty finite Subset of [:(LTLB_WFF **),(LTLB_WFF **):] equals :: LTLAXIO4:def 9
{ Q where Q is PNPair : ( rng (Q `1) = untn (rng (P `1)) & rng (Q `2) = untn (rng (P `2)) ) } ;

coherence
{ Q where Q is PNPair : ( rng (Q `1) = untn (rng (P `1)) & rng (Q `2) = untn (rng (P `2)) ) } is non empty finite Subset of [:(LTLB_WFF **),(LTLB_WFF **):]

proof end;

end;

:: deftheorem defines untn LTLAXIO4:def 9 :
for P being PNPair holds untn P = { Q where Q is PNPair : ( rng (Q `1) = untn (rng (P `1)) & rng (Q `2) = untn (rng (P `2)) ) } ;

theorem Th18: :: LTLAXIO4:18

for P being PNPair
for Q being Element of untn P holds {} LTLB_WFF |- (P ^) => ('X' (Q ^))

proof end;

registration

let P be consistent PNPair;

cluster -> consistent for Element of untn P;

coherence
for b₁ being Element of untn P holds b₁ is consistent

proof end;

end;

definition

let P be PNPair;

func compn P -> finite Subset of [:(LTLB_WFF **),(LTLB_WFF **):] equals :: LTLAXIO4:def 10
{ Q where Q is Element of [:(LTLB_WFF **),(LTLB_WFF **):] : Q in comp (untn P) } ;

coherence
{ Q where Q is Element of [:(LTLB_WFF **),(LTLB_WFF **):] : Q in comp (untn P) } is finite Subset of [:(LTLB_WFF **),(LTLB_WFF **):]

proof end;

end;

:: deftheorem defines compn LTLAXIO4:def 10 :
for P being PNPair holds compn P = { Q where Q is Element of [:(LTLB_WFF **),(LTLB_WFF **):] : Q in comp (untn P) } ;

registration

let P be consistent PNPair;

cluster compn P -> non empty finite ;

coherence
not compn P is empty

proof end;

end;

registration

let P be consistent PNPair;

cluster -> consistent for Element of compn P;

coherence
for b₁ being Element of compn P holds b₁ is consistent

proof end;

end;

theorem Th19: :: LTLAXIO4:19

for P, Q, R being PNPair st Q in compn P & R in untn P holds
Q is_completion_of R

proof end;

theorem Th20: :: LTLAXIO4:20

for P, Q being PNPair st Q in compn P holds
Q is complete

proof end;

registration

let P be consistent PNPair;

cluster -> complete for Element of compn P;

coherence
for b₁ being Element of compn P holds b₁ is complete by Th20;

end;

theorem Th21: :: LTLAXIO4:21

for A, B being Element of LTLB_WFF
for P, Q being PNPair st A 'U' B in rng (P `2) & Q in compn P holds
untn (A,B) in rng (Q `2)

proof end;

theorem Th22: :: LTLAXIO4:22

for A, B being Element of LTLB_WFF
for P, Q being PNPair st A 'U' B in rng (P `1) & Q in compn P holds
untn (A,B) in rng (Q `1)

proof end;

theorem Th23: :: LTLAXIO4:23

for P, Q, R being PNPair st R in compn Q & rng Q c= union (Subt (rng P)) holds
rng R c= union (Subt (rng P))

proof end;

theorem Th24: :: LTLAXIO4:24

for A, B being Element of LTLB_WFF
for P being consistent complete PNPair
for Q being Element of compn P st A 'U' B in rng (P `2) holds
( B in rng (Q `2) & ( A in rng (Q `2) or A 'U' B in rng (Q `2) ) )

proof end;

theorem Th25: :: LTLAXIO4:25

for A, B being Element of LTLB_WFF
for P being consistent complete PNPair
for Q being Element of compn P holds
( not A 'U' B in rng (P `1) or B in rng (Q `1) or ( A in rng (Q `1) & A 'U' B in rng (Q `1) ) )

proof end;

definition

let P be PNPair;

mode pnptree of P -> finite-branching DecoratedTree of [:(LTLB_WFF **),(LTLB_WFF **):] means :Def11: :: LTLAXIO4:def 11
( it . {} = P & ( for t being Element of dom it
for w being Element of [:(LTLB_WFF **),(LTLB_WFF **):] st w = it . t holds
succ (it,t) = the Enumeration of compn w ) );

correctness
existence
ex b₁ being finite-branching DecoratedTree of [:(LTLB_WFF **),(LTLB_WFF **):] st
( b₁ . {} = P & ( for t being Element of dom b₁
for w being Element of [:(LTLB_WFF **),(LTLB_WFF **):] st w = b₁ . t holds
succ (b₁,t) = the Enumeration of compn w ) );

proof end;

end;

:: deftheorem Def11 defines pnptree LTLAXIO4:def 11 :
for P being PNPair
for b₂ being finite-branching DecoratedTree of [:(LTLB_WFF **),(LTLB_WFF **):] holds
( b₂ is pnptree of P iff ( b₂ . {} = P & ( for t being Element of dom b₂
for w being Element of [:(LTLB_WFF **),(LTLB_WFF **):] st w = b₂ . t holds
succ (b₂,t) = the Enumeration of compn w ) ) );

definition

let P be PNPair;
let T be pnptree of P;
let t be Node of T;
:: original: |
redefine func T | t -> pnptree of T . t;
correctness
coherence
T | t is pnptree of T . t;

proof end;

end;

theorem Th26: :: LTLAXIO4:26

for P being PNPair
for T being pnptree of P
for t being Node of T
for n being Nat st t ^ <*n*> in dom T holds
T . (t ^ <*n*>) in compn (T . t)

proof end;

theorem Th27: :: LTLAXIO4:27

for P, Q being PNPair
for T being pnptree of P st Q in rng T holds
rng Q c= union (Subt (rng P))

proof end;

registration

let P be PNPair;
let T be pnptree of P;

cluster rng T -> non empty finite ;

coherence
( not rng T is empty & rng T is finite )

proof end;

end;

registration

let P be consistent PNPair;
let T be pnptree of P;

cluster -> consistent for Element of rng T;

coherence
for b₁ being Element of rng T holds b₁ is consistent

proof end;

end;

registration

let P be consistent complete PNPair;
let T be pnptree of P;

cluster -> complete for Element of rng T;

coherence
for b₁ being Element of rng T holds b₁ is complete

proof end;

end;

registration

let P be consistent complete PNPair;
let T be pnptree of P;
let t be Node of T;

cluster T . t -> consistent complete for PNPair;

coherence
for b₁ being PNPair st b₁ = T . t holds
( not b₁ is Inconsistent & b₁ is complete )

proof end;

end;

registration

let P be consistent PNPair;
let T be pnptree of P;
let t be Element of dom T;

cluster succ t -> non empty ;

coherence
not succ t is empty

proof end;

end;

definition

let P be PNPair;
let T be pnptree of P;

func rngr T -> finite Subset of [:(LTLB_WFF **),(LTLB_WFF **):] equals :: LTLAXIO4:def 12
{ (T . t) where t is Node of T : t <> {} } ;

correctness
coherence
{ (T . t) where t is Node of T : t <> {} } is finite Subset of [:(LTLB_WFF **),(LTLB_WFF **):];

proof end;

end;

:: deftheorem defines rngr LTLAXIO4:def 12 :
for P being PNPair
for T being pnptree of P holds rngr T = { (T . t) where t is Node of T : t <> {} } ;

registration

let P be consistent PNPair;
let T be pnptree of P;

cluster rngr T -> non empty finite ;

coherence
not rngr T is empty

proof end;

end;

theorem Th28: :: LTLAXIO4:28

for P, Q, R being PNPair
for T being pnptree of P st R in rng T & Q in untn R holds
comp Q c= rngr T

proof end;

theorem Th29: :: LTLAXIO4:29

for P being consistent complete PNPair
for T being pnptree of P
for f being FinSequence of LTLB_WFF st rng f = (rngr T) ^ holds
{} LTLB_WFF |- ('not' ((con (nega f)) /. (len (con (nega f))))) => ('X' ('not' ((con (nega f)) /. (len (con (nega f))))))

proof end;

definition

let P be consistent PNPair;
let T be pnptree of P;

mode path of T -> sequence of (dom T) means :Def13: :: LTLAXIO4:def 13
( it . 0 = {} & ( for k being Nat holds it . (k + 1) in succ (it . k) ) );

existence
ex b₁ being sequence of (dom T) st
( b₁ . 0 = {} & ( for k being Nat holds b₁ . (k + 1) in succ (b₁ . k) ) )

proof end;

end;

:: deftheorem Def13 defines path LTLAXIO4:def 13 :
for P being consistent PNPair
for T being pnptree of P
for b₃ being sequence of (dom T) holds
( b₃ is path of T iff ( b₃ . 0 = {} & ( for k being Nat holds b₃ . (k + 1) in succ (b₃ . k) ) ) );

definition

let P be consistent complete PNPair;
let T be pnptree of P;
let t be path of T;
let i be Nat;
:: original: .
redefine func t . i -> Node of T;
coherence
t . i is Node of T

proof end;

end;

theorem Th30: :: LTLAXIO4:30

for A, B being Element of LTLB_WFF
for i being Nat
for P being consistent complete PNPair
for T being pnptree of P
for t being path of T st A 'U' B in rng ((T . (t . i)) `2) holds
for j being Element of NAT holds
( not j > i or B in rng ((T . (t . j)) `2) or ex k being Element of NAT st
( i < k & k < j & A in rng ((T . (t . k)) `2) ) )

proof end;

theorem Th31: :: LTLAXIO4:31

for A, B being Element of LTLB_WFF
for P being consistent complete PNPair
for T being pnptree of P st A 'U' B in rng (P `1) & ( for Q being Element of rngr T holds not B in rng (Q `1) ) holds
for Q being Element of rngr T holds
( B in rng (Q `2) & A 'U' B in rng (Q `1) )

proof end;

theorem Th32: :: LTLAXIO4:32

for A, B being Element of LTLB_WFF
for P being consistent complete PNPair
for T being pnptree of P st A 'U' B in rng (P `1) holds
ex R being Element of rngr T st B in rng (R `1)

proof end;

definition

let P be consistent PNPair;
let T be pnptree of P;
let t be path of T;

attr t is complete means :Def14: :: LTLAXIO4:def 14
for A, B being Element of LTLB_WFF
for i being Nat st A 'U' B in rng ((T . (t . i)) `1) holds
ex j being Element of NAT st
( j > i & B in rng ((T . (t . j)) `1) & ( for k being Element of NAT st i < k & k < j holds
A in rng ((T . (t . k)) `1) ) );

end;

:: deftheorem Def14 defines complete LTLAXIO4:def 14 :
for P being consistent PNPair
for T being pnptree of P
for t being path of T holds
( t is complete iff for A, B being Element of LTLB_WFF
for i being Nat st A 'U' B in rng ((T . (t . i)) `1) holds
ex j being Element of NAT st
( j > i & B in rng ((T . (t . j)) `1) & ( for k being Element of NAT st i < k & k < j holds
A in rng ((T . (t . k)) `1) ) ) );

registration

let P be consistent complete PNPair;
let T be pnptree of P;

cluster Relation-like omega -defined dom T -valued Function-like V36( omega , dom T) complete for path of T;

existence
ex b₁ being path of T st b₁ is complete

proof end;

end;

registration

let P be consistent PNPair;

cluster P ^ -> satisfiable ;

coherence
P ^ is satisfiable

proof end;

end;

:: Completeness theorem for Propositional Linear Temporal Logic

theorem :: LTLAXIO4:33

for A being Element of LTLB_WFF
for F being finite Subset of LTLB_WFF st F |= A holds
F |- A

proof end;