© 1996-2018

15 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

Contact | Home | ITL home | Course | Proofs | Algebra | FL