:: Propositional Linear Time Temporal Logic with Initial Semantics
:: by Mariusz Giero
::
:: Received October 22, 2015
:: Copyright (c) 2015-2021 Association of Mizar Users

theorem Lm1: :: LTLAXIO5:1

for X being set
for f being FinSequence of X
for i being Nat st 1 <= i & i <= len f holds
f . i = f /. i

proof end;

::#INSERT: LTLB with normal semantics is monotonic

theorem mon2: :: LTLAXIO5:2

for A being Element of LTLB_WFF
for F, G being Subset of LTLB_WFF st F c= G & F |- A holds
G |- A

proof end;

theorem th16: :: LTLAXIO5:3

for A, B, C being Element of LTLB_WFF holds (A => B) => ((B => C) => (A => C)) is LTL_TAUT_OF_PL

proof end;

theorem th17: :: LTLAXIO5:4

for A, B, C being Element of LTLB_WFF holds (A => (B => C)) => ((A => B) => (A => C)) is LTL_TAUT_OF_PL

proof end;

theorem th18: :: LTLAXIO5:5

for A being Element of LTLB_WFF
for F being Subset of LTLB_WFF holds F |- ('G' A) => A

proof end;

theorem th19a: :: LTLAXIO5:6

for A being Element of LTLB_WFF holds {A} |= 'G' ('X' A)

proof end;

theorem th19: :: LTLAXIO5:7

for A being Element of LTLB_WFF
for F being Subset of LTLB_WFF holds F |- ('G' A) => ('G' ('X' A))

proof end;

theorem th20: :: LTLAXIO5:8

for A, B being Element of LTLB_WFF
for F being Subset of LTLB_WFF holds F |- ('G' (A => B)) => (('G' (A => ('X' A))) => ('G' (A => ('G' B))))

proof end;

::#INSERT: A formula A is initially valid in the temporal structure M

definition

let M be LTLModel;
let A be Element of LTLB_WFF ;

::#INSERT: A formula A is initially valid in the temporal structure M

pred M |=0 A means :: LTLAXIO5:def 1
(SAT M) . [0,A] = 1;

end;

:: deftheorem defines |=0 LTLAXIO5:def 1 :
for M being LTLModel
for A being Element of LTLB_WFF holds
( M |=0 A iff (SAT M) . [0,A] = 1 );

::#INSERT: A set F of formulas is initially valid in the temporal structure M

definition

let M be LTLModel;
let F be Subset of LTLB_WFF;

::#INSERT: A set F of formulas is initially valid in the temporal structure M

pred M |=0 F means :: LTLAXIO5:def 2
for A being Element of LTLB_WFF st A in F holds
M |=0 A;

end;

:: deftheorem defines |=0 LTLAXIO5:def 2 :
for M being LTLModel
for F being Subset of LTLB_WFF holds
( M |=0 F iff for A being Element of LTLB_WFF st A in F holds
M |=0 A );

::#INSERT: A formula A is an initial consequence of a set F of formulas

definition

let F be Subset of LTLB_WFF;
let A be Element of LTLB_WFF ;

pred F |=0 A means :: LTLAXIO5:def 3
for M being LTLModel st M |=0 F holds
M |=0 A;

end;

:: deftheorem defines |=0 LTLAXIO5:def 3 :
for F being Subset of LTLB_WFF
for A being Element of LTLB_WFF holds
( F |=0 A iff for M being LTLModel st M |=0 F holds
M |=0 A );

::#INSERT: The numbers 2.6.1-2.6.8, put in comments in the article,
::#INSERT: correspond to the ones in: Kroeger, Merz. Temporal Logic and State
::#INSERT: Systems. 2008. Springer-Verlag.
::#INSERT: 2.6.1a-trivial: M |= A implies M |=0 A

theorem Th1: :: LTLAXIO5:9

for F being Subset of LTLB_WFF
for M being LTLModel st M |= F holds
M |=0 F

proof end;

::#INSERT: 2.6.1b

theorem th261b: :: LTLAXIO5:10

for A being Element of LTLB_WFF
for M being LTLModel holds
( M |= A iff M |=0 'G' A )

proof end;

::#INSERT: 2.6.2a

theorem th262a: :: LTLAXIO5:11

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

proof end;

definition

let F be Subset of LTLB_WFF;

func 'G' F -> Subset of LTLB_WFF equals :: LTLAXIO5:def 4
{ ('G' A) where A is Element of LTLB_WFF : A in F } ;

correctness
coherence
{ ('G' A) where A is Element of LTLB_WFF : A in F } is Subset of LTLB_WFF;

proof end;

end;

:: deftheorem defines 'G' LTLAXIO5:def 4 :
for F being Subset of LTLB_WFF holds 'G' F = { ('G' A) where A is Element of LTLB_WFF : A in F } ;

theorem th261bq: :: LTLAXIO5:12

for F being Subset of LTLB_WFF
for M being LTLModel holds
( M |= F iff M |=0 'G' F )

proof end;

::#INSERT: 2.6.2b

theorem th262b: :: LTLAXIO5:13

for A being Element of LTLB_WFF
for F being Subset of LTLB_WFF holds
( F |= A iff 'G' F |=0 A )

proof end;

theorem th262ac1: :: LTLAXIO5:14

for n being Element of NAT holds
( {(prop n)} |= 'X' (prop n) & not {(prop n)} |=0 'X' (prop n) )

proof end;

::#INSERT: The converse of 2.6.2a does not hold in general

theorem :: LTLAXIO5:15

ex F being Subset of LTLB_WFF ex A being Element of LTLB_WFF st
( F |= A & not F |=0 A )

proof end;

theorem th21: :: LTLAXIO5:16

for A being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F |=0 'G' A holds
F |= A

proof end;

theorem th21cp: :: LTLAXIO5:17

for i being Element of NAT holds
( {(prop i)} |= prop i & not {(prop i)} |=0 'G' (prop i) )

proof end;

theorem :: LTLAXIO5:18

ex F being Subset of LTLB_WFF ex A being Element of LTLB_WFF st
( F |= A & not F |=0 'G' A )

proof end;

theorem th263pa: :: LTLAXIO5:19

for F, G being Subset of LTLB_WFF
for M being LTLModel holds
( ( M |=0 F & M |=0 G ) iff M |=0 F \/ G )

proof end;

theorem th263pb: :: LTLAXIO5:20

for A being Element of LTLB_WFF
for M being LTLModel holds
( M |=0 A iff M |=0 {A} )

proof end;

::#INSERT: 2.6.3
::#INSERT: In compare to normal consequence (LTLAXIO1:30), the relationship
::#INSERT: between implication and initial consequence holds in the classical
::#INSERT: form

theorem th263: :: LTLAXIO5:21

for A, B being Element of LTLB_WFF
for F being Subset of LTLB_WFF holds
( F \/ {A} |=0 B iff F |=0 A => B )

proof end;

theorem th264p: :: LTLAXIO5:22

'G' ({} LTLB_WFF) = {} LTLB_WFF

proof end;

::#INSERT: Universal validity concepts are equaivalent as far as
::#INSERT: initial and normal semantics is concerned:
::#INSERT: 2.6.4: one line proof:
::#INSERT: {}LTLB_WFF |= A iff {}LTLB_WFF |=0 A by th262b,th264p
::#INSERT: 2.1.8

theorem th218: :: LTLAXIO5:23

for A being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F |= A & ( for B being Element of LTLB_WFF st B in F holds
{} LTLB_WFF |= B ) holds
{} LTLB_WFF |= A

proof end;

::#INSERT: 2.6.5

theorem th265: :: LTLAXIO5:24

for A being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F |= A & ( for B being Element of LTLB_WFF st B in F holds
{} LTLB_WFF |=0 B ) holds
{} LTLB_WFF |=0 A

proof end;

theorem :: LTLAXIO5:25

for A being Element of LTLB_WFF st {} LTLB_WFF |=0 A holds
{} LTLB_WFF |=0 'X' A

proof end;

::#INSERT: Axioms

definition

func LTL0_axioms -> Subset of LTLB_WFF equals :: LTLAXIO5:def 5
'G' LTL_axioms;

correctness
coherence
'G' LTL_axioms is Subset of LTLB_WFF;
;

end;

:: deftheorem defines LTL0_axioms LTLAXIO5:def 5 :
LTL0_axioms = 'G' LTL_axioms;

::#INSERT: Derivation rules

definition

let p, q be Element of LTLB_WFF ;

pred p REFL0_rule q means :: LTLAXIO5:def 6
p = 'G' q;

pred p NEX0_rule q means :: LTLAXIO5:def 7
ex A being Element of LTLB_WFF st
( p = 'G' A & q = 'G' ('X' A) );

let r be Element of LTLB_WFF ;

pred p,q MP0_rule r means :: LTLAXIO5:def 8
ex A, B being Element of LTLB_WFF st
( p = 'G' A & q = 'G' (A => B) & r = 'G' B );

pred p,q IND0_rule r means :: LTLAXIO5:def 9
ex A, B being Element of LTLB_WFF st
( p = 'G' (A => B) & q = 'G' (A => ('X' A)) & r = 'G' (A => ('G' B)) );

end;

:: deftheorem defines REFL0_rule LTLAXIO5:def 6 :
for p, q being Element of LTLB_WFF holds
( p REFL0_rule q iff p = 'G' q );

:: deftheorem defines NEX0_rule LTLAXIO5:def 7 :
for p, q being Element of LTLB_WFF holds
( p NEX0_rule q iff ex A being Element of LTLB_WFF st
( p = 'G' A & q = 'G' ('X' A) ) );

:: deftheorem defines MP0_rule LTLAXIO5:def 8 :
for p, q, r being Element of LTLB_WFF holds
( p,q MP0_rule r iff ex A, B being Element of LTLB_WFF st
( p = 'G' A & q = 'G' (A => B) & r = 'G' B ) );

:: deftheorem defines IND0_rule LTLAXIO5:def 9 :
for p, q, r being Element of LTLB_WFF holds
( p,q IND0_rule r iff ex A, B being Element of LTLB_WFF st
( p = 'G' (A => B) & q = 'G' (A => ('X' A)) & r = 'G' (A => ('G' B)) ) );

::#INSERT: Definition of derivation step

definition

let i be Nat;
let f be FinSequence of LTLB_WFF ;
let X be Subset of LTLB_WFF;

::#INSERT: Definition of derivation step

pred prc0 f,X,i means :Def29: :: LTLAXIO5:def 10
( f . i in LTL0_axioms or f . i in X or ex j, k being Nat st
( 1 <= j & j < i & 1 <= k & k < i & ( f /. j,f /. k MP_rule f /. i or f /. j,f /. k MP0_rule f /. i or f /. j,f /. k IND0_rule f /. i ) ) or ex j being Nat st
( 1 <= j & j < i & ( f /. j NEX0_rule f /. i or f /. j REFL0_rule f /. i ) ) );

end;

:: deftheorem Def29 defines prc0 LTLAXIO5:def 10 :
for i being Nat
for f being FinSequence of LTLB_WFF
for X being Subset of LTLB_WFF holds
( prc0 f,X,i iff ( f . i in LTL0_axioms or f . i in X or ex j, k being Nat st
( 1 <= j & j < i & 1 <= k & k < i & ( f /. j,f /. k MP_rule f /. i or f /. j,f /. k MP0_rule f /. i or f /. j,f /. k IND0_rule f /. i ) ) or ex j being Nat st
( 1 <= j & j < i & ( f /. j NEX0_rule f /. i or f /. j REFL0_rule f /. i ) ) ) );

::#INSERT: Properties of derivation step prc0 - analogue of "prc" from LTLAXIO1

theorem Th38: :: LTLAXIO5:26

for X being Subset of LTLB_WFF
for f, f2 being FinSequence of LTLB_WFF
for i, n being Nat st n + (len f) <= len f2 & ( for k being Nat st 1 <= k & k <= len f holds
f . k = f2 . (k + n) ) & 1 <= i & i <= len f & prc0 f,X,i holds
prc0 f2,X,i + n

proof end;

theorem Th39: :: LTLAXIO5:27

for X being Subset of LTLB_WFF
for f, f1, f2 being FinSequence of LTLB_WFF st f2 = f ^ f1 & 1 <= len f & 1 <= len f1 & ( for i being Nat st 1 <= i & i <= len f holds
prc0 f,X,i ) & ( for i being Nat st 1 <= i & i <= len f1 holds
prc0 f1,X,i ) holds
for i being Nat st 1 <= i & i <= len f2 holds
prc0 f2,X,i

proof end;

:: Derivability

definition

let X be Subset of LTLB_WFF;
let p be Element of LTLB_WFF ;

pred X |-0 p means :: LTLAXIO5:def 11
ex f being FinSequence of LTLB_WFF st
( f . (len f) = p & 1 <= len f & ( for i being Nat st 1 <= i & i <= len f holds
prc0 f,X,i ) );

end;

:: deftheorem defines |-0 LTLAXIO5:def 11 :
for X being Subset of LTLB_WFF
for p being Element of LTLB_WFF holds
( X |-0 p iff ex f being FinSequence of LTLB_WFF st
( f . (len f) = p & 1 <= len f & ( for i being Nat st 1 <= i & i <= len f holds
prc0 f,X,i ) ) );

:: Properties of derivation sequences

theorem Th40: :: LTLAXIO5:28

for p being Element of LTLB_WFF
for X being Subset of LTLB_WFF
for f, f1 being FinSequence of LTLB_WFF st f = f1 ^ <*p*> & 1 <= len f1 & ( for i being Nat st 1 <= i & i <= len f1 holds
prc0 f1,X,i ) & prc0 f,X, len f holds
( ( for i being Nat st 1 <= i & i <= len f holds
prc0 f,X,i ) & X |-0 p )

proof end;

::#INSERT: Axioms are sound

theorem Th2: :: LTLAXIO5:29

for A being Element of LTLB_WFF
for F being Subset of LTLB_WFF st A in LTL0_axioms holds
F |=0 A

proof end;

::#INSERT: MP_rule is sound

theorem Th3: :: LTLAXIO5:30

for A, B being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F |=0 A & F |=0 A => B holds
F |=0 B

proof end;

::#INSERT: MP0_rule is sound

theorem Th4: :: LTLAXIO5:31

for A, B being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F |=0 'G' A & F |=0 'G' (A => B) holds
F |=0 'G' B

proof end;

::#INSERT: NEX0_rule is sound

theorem Th5: :: LTLAXIO5:32

for A being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F |=0 'G' A holds
F |=0 'G' ('X' A)

proof end;

::#INSERT: REFL0_rule is sound

theorem Th6: :: LTLAXIO5:33

for A being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F |=0 'G' A holds
F |=0 A

proof end;

::#INSERT: IND0_rule is sound

theorem Th7: :: LTLAXIO5:34

for A, B being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F |=0 'G' (A => B) & F |=0 'G' (A => ('X' A)) holds
F |=0 'G' (A => ('G' B))

proof end;

::#INSERT: 2.6.6
:: Soundness Theorem for LTLB with initial semantics.

theorem th266: :: LTLAXIO5:35

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

proof end;

::#INSERT: Axioms and premises are derivable

theorem th10: :: LTLAXIO5:36

for A being Element of LTLB_WFF
for F being Subset of LTLB_WFF st ( A in LTL0_axioms or A in F ) holds
F |-0 A

proof end;

::#INSERT: REFL0_rule is derivable

theorem th9: :: LTLAXIO5:37

for A being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F |-0 'G' A holds
F |-0 A

proof end;

::#INSERT: NEX0_rule is derivable

theorem th12: :: LTLAXIO5:38

for A being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F |-0 'G' A holds
F |-0 'G' ('X' A)

proof end;

::#INSERT: MP_rule is derivable

theorem th11a: :: LTLAXIO5:39

for A, B being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F |-0 A & F |-0 A => B holds
F |-0 B

proof end;

::#INSERT: MP0_rule is derivable

theorem th11: :: LTLAXIO5:40

for A, B being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F |-0 'G' A & F |-0 'G' (A => B) holds
F |-0 'G' B

proof end;

::#INSERT: IND0_rule is derivable

theorem th13: :: LTLAXIO5:41

for A, B being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F |-0 'G' (A => B) & F |-0 'G' (A => ('X' A)) holds
F |-0 'G' (A => ('G' B))

proof end;

theorem th15: :: LTLAXIO5:42

for A being Element of LTLB_WFF
for F being Subset of LTLB_WFF st A in LTL_axioms holds
F |-0 A

proof end;

theorem :: LTLAXIO5:43

for A being Element of LTLB_WFF
for F being Subset of LTLB_WFF st A in LTL0_axioms holds
F |- A

proof end;

::#INSERT: 2.6.7
::#INSERT: auxilliary theorem to prove completeness theorem

theorem th267: :: LTLAXIO5:44

for A being Element of LTLB_WFF st {} LTLB_WFF |- A holds
{} LTLB_WFF |-0 A

proof end;

::#INSERT: Generalized theorem 2.6.7 does not hold, i.e.,
::#INSERT: not for F,A holds (F |- A implies F |-0 A);

theorem th14: :: LTLAXIO5:45

for i being Element of NAT holds
( {(prop i)} |- 'X' (prop i) & not {(prop i)} |-0 'X' (prop i) )

proof end;

::#INSERT: LTLB with initial semantics is monotonic

theorem mon: :: LTLAXIO5:46

for A being Element of LTLB_WFF
for F, G being Subset of LTLB_WFF st F c= G & F |-0 A holds
G |-0 A

proof end;

definition

let f be FinSequence of LTLB_WFF ;
let A be Element of LTLB_WFF ;

func implications (f,A) -> FinSequence of LTLB_WFF means :imps: :: LTLAXIO5:def 12
( len it = len f & it . 1 = (f /. 1) => A & ( for i being Element of NAT st 1 <= i & i < len f holds
it . (i + 1) = (f /. (i + 1)) => (it /. i) ) ) if len f > 0
otherwise it = <*> LTLB_WFF;

existence
( ( len f > 0 implies ex b₁ being FinSequence of LTLB_WFF st
( len b₁ = len f & b₁ . 1 = (f /. 1) => A & ( for i being Element of NAT st 1 <= i & i < len f holds
b₁ . (i + 1) = (f /. (i + 1)) => (b₁ /. i) ) ) ) & ( not len f > 0 implies ex b₁ being FinSequence of LTLB_WFF st b₁ = <*> LTLB_WFF ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of LTLB_WFF holds
( ( len f > 0 & len b₁ = len f & b₁ . 1 = (f /. 1) => A & ( for i being Element of NAT st 1 <= i & i < len f holds
b₁ . (i + 1) = (f /. (i + 1)) => (b₁ /. i) ) & len b₂ = len f & b₂ . 1 = (f /. 1) => A & ( for i being Element of NAT st 1 <= i & i < len f holds
b₂ . (i + 1) = (f /. (i + 1)) => (b₂ /. i) ) implies b₁ = b₂ ) & ( not len f > 0 & b₁ = <*> LTLB_WFF & b₂ = <*> LTLB_WFF implies b₁ = b₂ ) )

proof end;

consistency
for b₁ being FinSequence of LTLB_WFF holds verum ;

end;

:: deftheorem imps defines implications LTLAXIO5:def 12 :
for f being FinSequence of LTLB_WFF
for A being Element of LTLB_WFF
for b₃ being FinSequence of LTLB_WFF holds
( ( len f > 0 implies ( b₃ = implications (f,A) iff ( len b₃ = len f & b₃ . 1 = (f /. 1) => A & ( for i being Element of NAT st 1 <= i & i < len f holds
b₃ . (i + 1) = (f /. (i + 1)) => (b₃ /. i) ) ) ) ) & ( not len f > 0 implies ( b₃ = implications (f,A) iff b₃ = <*> LTLB_WFF ) ) );

::#INSERT: 2.6.8
:: Weak Completeness Theorem for LTLB with initial semantics

theorem th268: :: LTLAXIO5:47

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

proof end;

::#INSERT: Deduction theorem holds in the classical form compared with
::#INSERT: Deduction theorem for LTLB with normal semantics (see LTLAXIO1:57)

theorem :: LTLAXIO5:48

for A, B being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F \/ {A} |-0 B holds
F |-0 A => B

proof end;

:: Converse of Deduction Theorem

theorem :: LTLAXIO5:49

for A, B being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F |-0 A => B holds
F \/ {A} |-0 B

proof end;

registration

let F be finite Subset of LTLB_WFF;

cluster 'G' F -> finite ;

coherence
'G' F is finite

proof end;

end;

theorem :: LTLAXIO5:50

for A being Element of LTLB_WFF
for F being finite Subset of LTLB_WFF holds
( F |- A iff 'G' F |-0 A )

proof end;

theorem :: LTLAXIO5:51

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

proof end;

::#INSERT: The counterexample that "for F,A holds (F |- A implies F |-0 A)"
::#INSERT: is not true. Another counterexample see above for theorem "th14".

theorem :: LTLAXIO5:52

for i being Element of NAT holds
( {(prop i)} |- 'G' (prop i) & not {(prop i)} |-0 'G' (prop i) )

proof end;

theorem :: LTLAXIO5:53

for A being Element of LTLB_WFF
for F being finite Subset of LTLB_WFF st F |-0 'G' A holds
F |- A

proof end;

::#INSERT: The converse of the above theorem does not hold

theorem :: LTLAXIO5:54

for i being Element of NAT holds
( {(prop i)} |- prop i & not {(prop i)} |-0 'G' (prop i) )

proof end;