:: Propositional Linear Time Temporal Logic with Initial Semantics
:: by Mariusz Giero
::
:: Received October 22, 2015
:: Copyright (c) 2015-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies FINSEQ_1, CARD_1, ORDINAL4, SUBSET_1, NUMBERS, ARYTM_3, TARSKI,
RELAT_1, XBOOLE_0, FUNCT_1, XBOOLEAN, MODELC_2, CQC_THE1, NAT_1,
XXREAL_0, ARYTM_1, PARTFUN1, MARGREL1, HILBERT2, ZFMISC_1, ZF_MODEL,
FINSET_1, RFINSEQ, LTLAXIO1, LTLAXIO5;
notations TARSKI, XBOOLE_0, ZFMISC_1, DOMAIN_1, SUBSET_1, ORDINAL1, PARTFUN1,
XCMPLX_0, NUMBERS, NAT_1, XXREAL_0, NAT_D, FUNCT_1, RELSET_1, FUNCT_2,
FINSET_1, FINSEQ_1, RFINSEQ, HILBERT1, HILBERT2, XBOOLEAN, MARGREL1,
LTLAXIO1;
constructors NAT_D, RELSET_1, HILBERT2, RFINSEQ, DOMAIN_1, LTLAXIO1;
registrations SUBSET_1, ORDINAL1, NAT_1, XBOOLEAN, RELSET_1, MARGREL1,
XBOOLE_0, XREAL_0, HILBERT1, FINSET_1, LTLAXIO1;
requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
begin
theorem :: LTLAXIO5:1
for X be set,f be FinSequence of X,i be Nat st 1 <= i & i <= len f holds
f.i=f/.i;
reserve A,B,C,D,p,q,r for Element of LTLB_WFF,
F,G,X for Subset of LTLB_WFF,
M for LTLModel,
i,j,n for Element of NAT,
f,f1,f2,g for FinSequence of LTLB_WFF;
::#INSERT: LTLB with normal semantics is monotonic
theorem :: LTLAXIO5:2
F c= G & F |- A implies G |- A;
theorem :: LTLAXIO5:3
(A => B) => ((B => C) => (A => C)) is LTL_TAUT_OF_PL;
theorem :: LTLAXIO5:4
(A => (B => C)) => ((A => B) => (A => C)) is LTL_TAUT_OF_PL;
theorem :: LTLAXIO5:5
F |- ('G' A) => A;
theorem :: LTLAXIO5:6
{A} |= 'G' 'X' A;
theorem :: LTLAXIO5:7
F |- ('G' A) => 'G' 'X' A;
theorem :: LTLAXIO5:8
F |- ('G' (A => B)) => (('G' (A => 'X' A)) => ('G' (A => 'G' B)));
begin
::#INSERT: A formula A is initially valid in the temporal structure M
definition let M,A;
pred M |=0 A means
:: LTLAXIO5:def 1
(SAT M).[0,A]=1;
end;
::#INSERT: A set F of formulas is initially valid in the temporal structure M
definition let M,F;
pred M |=0 F means
:: LTLAXIO5:def 2
for A st A in F holds M |=0 A;
end;
::#INSERT: A formula A is an initial consequence of a set F of formulas
definition let F,A;
pred F |=0 A means
:: LTLAXIO5:def 3
for M st M |=0 F holds M |=0 A;
end;
begin
::#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 :: LTLAXIO5:9
M |= F implies M |=0 F;
::#INSERT: 2.6.1b
theorem :: LTLAXIO5:10
M |= A iff M |=0 'G' A;
::#INSERT: 2.6.2a
theorem :: LTLAXIO5:11
F |=0 A implies F |= A;
definition let F;
func 'G' F -> Subset of LTLB_WFF equals
:: LTLAXIO5:def 4
{'G' A where A is Element of LTLB_WFF: A in F};
end;
theorem :: LTLAXIO5:12
M |= F iff M |=0 ('G' F);
::#INSERT: 2.6.2b
theorem :: LTLAXIO5:13
F |= A iff 'G' F |=0 A;
theorem :: LTLAXIO5:14
{prop n} |= 'X' prop n & not {prop n} |=0 'X' prop n;
::#INSERT: The converse of 2.6.2a does not hold in general
theorem :: LTLAXIO5:15
ex F,A st F |= A & not F |=0 A;
theorem :: LTLAXIO5:16
F |=0 'G' A implies F |= A;
theorem :: LTLAXIO5:17
{prop i} |= prop i & not {prop i} |=0 'G' prop i;
theorem :: LTLAXIO5:18
ex F, A st (F |= A & not F |=0 'G' A);
theorem :: LTLAXIO5:19
M |=0 F & M |=0 G iff M |=0 F\/G;
theorem :: LTLAXIO5:20
M |=0 A iff M |=0 {A};
::#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 :: LTLAXIO5:21 :: 2.6.3
F\/{A} |=0 B iff F|=0 A=>B;
theorem :: LTLAXIO5:22
'G' {}LTLB_WFF = {}LTLB_WFF;
::#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 :: LTLAXIO5:23
F |= A & (for B st B in F holds {}LTLB_WFF |= B)
implies {}LTLB_WFF |= A;
::#INSERT: 2.6.5
theorem :: LTLAXIO5:24
F |= A & (for B st B in F holds {}LTLB_WFF |=0 B)
implies {}LTLB_WFF |=0 A;
theorem :: LTLAXIO5:25
{}LTLB_WFF |=0 A implies {}LTLB_WFF |=0 'X' A;
begin
::#INSERT: Axioms
definition
func LTL0_axioms -> Subset of LTLB_WFF equals
:: LTLAXIO5:def 5
'G' LTL_axioms;
end;
::#INSERT: Derivation rules
definition let p,q;
pred p REFL0_rule q means
:: LTLAXIO5:def 6
p = 'G' q;
pred p NEX0_rule q means
:: LTLAXIO5:def 7
ex A st p = 'G' A & q = 'G' 'X' A;
let r;
pred p,q MP0_rule r means
:: LTLAXIO5:def 8
ex A,B st p='G' A & q= 'G' (A=>B) & r='G' B;
pred p,q IND0_rule r means
:: LTLAXIO5:def 9
ex A,B st p='G' (A=>B) & q= 'G' (A=>('X' A)) & r='G' (A=>('G' B));
end;
::#INSERT: Definition of derivation step
definition let i be Nat,f,X;
pred prc0 f,X,i means
:: LTLAXIO5:def 10
f.i in LTL0_axioms or f.i in X
or (ex j,k be Nat st 1<=j & j* & 1<=len f1 &
for i be Nat st 1<=i & i<=len f1 holds prc0 f1,X,i) &
prc0 f,X,len f implies (for i be Nat st 1<=i & i<=len f holds prc0 f,X,i) &
X |-0 p;
begin
::#INSERT: Axioms are sound
theorem :: LTLAXIO5:29
A in LTL0_axioms implies F |=0 A;
::#INSERT: MP_rule is sound
theorem :: LTLAXIO5:30
F |=0 A & F |=0 A=>B implies F |=0 B;
::#INSERT: MP0_rule is sound
theorem :: LTLAXIO5:31
F |=0 'G' A & F |=0 'G' (A=>B) implies F |=0 'G' B;
::#INSERT: NEX0_rule is sound
theorem :: LTLAXIO5:32
F |=0 'G' A implies F |=0 'G' 'X' A;
::#INSERT: REFL0_rule is sound
theorem :: LTLAXIO5:33
F |=0 'G' A implies F |=0 A;
::#INSERT: IND0_rule is sound
theorem :: LTLAXIO5:34
F |=0 'G' (A=>B) & F |=0 'G' (A=>('X' A)) implies F |=0 'G' (A=>('G' B));
::#INSERT: 2.6.6
::$N Soundness Theorem for LTLB with initial semantics.
theorem :: LTLAXIO5:35
F |-0 A implies F |=0 A;
begin
::#INSERT: Axioms and premises are derivable
theorem :: LTLAXIO5:36
A in LTL0_axioms or A in F implies F|-0 A;
::#INSERT: REFL0_rule is derivable
theorem :: LTLAXIO5:37
F |-0 'G' A implies F |-0 A;
::#INSERT: NEX0_rule is derivable
theorem :: LTLAXIO5:38
F |-0 'G' A implies F |-0 'G' 'X' A;
::#INSERT: MP_rule is derivable
theorem :: LTLAXIO5:39
F |-0 A & F |-0 A => B implies F |-0 B;
::#INSERT: MP0_rule is derivable
theorem :: LTLAXIO5:40
F |-0 'G' A & F |-0 'G' (A => B) implies F |-0 'G' B;
::#INSERT: IND0_rule is derivable
theorem :: LTLAXIO5:41
F |-0 'G' (A=>B) & F |-0 'G' (A => 'X' A) implies F |-0 'G' (A => 'G' B);
theorem :: LTLAXIO5:42
A in LTL_axioms implies F|-0 A;
theorem :: LTLAXIO5:43
A in LTL0_axioms implies F |- A;
::#INSERT: 2.6.7
::#INSERT: auxilliary theorem to prove completeness theorem
theorem :: LTLAXIO5:44
{}LTLB_WFF |- A implies {}LTLB_WFF |-0 A;
::#INSERT: Generalized theorem 2.6.7 does not hold, i.e.,
::#INSERT: not for F,A holds (F |- A implies F |-0 A);
theorem :: LTLAXIO5:45
{prop i} |- 'X' prop i & not {prop i} |-0 'X' prop i;
::#INSERT: LTLB with initial semantics is monotonic
theorem :: LTLAXIO5:46
F c= G & F |-0 A implies G |-0 A;
definition let f,A;
func implications(f,A) -> FinSequence of LTLB_WFF means
:: LTLAXIO5:def 12
len it = len f & it.1 = f/.1 => A & for i st
1 <= i & i < len f holds it.(i+1) = f/.(i+1) => it/.i if len f > 0
otherwise it = <*> LTLB_WFF;
end;
::#INSERT: 2.6.8
::$N Weak Completeness Theorem for LTLB with initial semantics
theorem :: LTLAXIO5:47
for F be finite Subset of LTLB_WFF holds F |=0 A implies F |-0 A;
begin
::#INSERT: Deduction theorem holds in the classical form compared with
::#INSERT: Deduction theorem for LTLB with normal semantics (see LTLAXIO1:57)
theorem :: LTLAXIO5:48
F \/ {A} |-0 B implies F |-0 A => B;
:: Converse of Deduction Theorem
theorem :: LTLAXIO5:49
F |-0 A => B implies F \/ {A} |-0 B;
begin
registration let F be finite Subset of LTLB_WFF;
cluster 'G' F -> finite;
end;
theorem :: LTLAXIO5:50
for F be finite Subset of LTLB_WFF holds (F |- A iff 'G' F |-0 A);
theorem :: LTLAXIO5:51
for F be finite Subset of LTLB_WFF holds (F |-0 A implies F |- A);
::#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
{prop i} |- 'G' prop i & not {prop i} |-0 'G' prop i;
theorem :: LTLAXIO5:53
for F be finite Subset of LTLB_WFF holds (F |-0 'G' A implies F |- A);
::#INSERT: The converse of the above theorem does not hold
theorem :: LTLAXIO5:54
{prop i} |- prop i & not {prop i} |-0 'G' prop i;
*