6 Axiom system for PITL with finite and infinite time

Substitution instances of valid PTL formulas VPTL
(f ⌢ g) ⌢ h f ⌢ (g ⌢ h) ChopAssoc
(f0 f1) ⌢ g (f0 ⌢ g) (f1 ⌢ g) OrChopImp
f ⌢ (g0 g1) (f ⌢ g0) (f ⌢ g1) ChopOrImp
empty ⌢ f f EmptyChop
finite (f ⌢ empty f) FiniteImpChopEmpty
w w StateImpBf
(f0 f1) (g0 g1) (f0 ⌢ g0) (f1 ⌢ g1) BfAndBoxImpChopImpChop
f empty (f more) ⌢ f SChopStarEqv
f (f (g more) ⌢ f) gω ChopOmegaInduct
f g, f ⇒ ⊢ g MP
finite f ⇒ ⊢ f BfFGen
f ⇒ ⊢ f BoxGen
((fin P) g) f ⇒ ⊢ f BfAux

In BfAux, propositional variable P must not occur in f and g.

f1 f2, ,…, fn1 fn ⇒ ⊢ f1 fn ImpChain
f1 f2, ,…, fn1 fn ⇒ ⊢ f1 fn EqvChain
f1,f2,…,fn ⇒ ⊢ g, Prop
where the formula f1 f2 …fn g
is a substitution instance of a propositional tautology

2023-09-12
Contact | Home | ITL home | Course | Proofs | Algebra | FL
© 1996-2023