© 1996-2019







2.4 Propositional proof system

In Table 15 we list the propositional axioms and rules for finite and infinite ITL.


Table 15: Propositional Axioms and Rules for finite and infinite ITL.
ChopAssoc
(f0 ; f1) ; f2 f0 ; (f1 ; f2)
OrChopImp
(f0 f1) ; f2 (f0 ; f2) (f1 ; f2)
ChopOrImp
f0 ; (f1 f2) (f0 ; f1) (f0 ; f2)
EmptyChop
empty ; f f
ChopEmpty
f ; empty f
BiBoxChopImpChop
(f0 f1) (f2 f3) (f0 ; f2) (f1 ; f3)
StateImpBi
w w
NextImpNotNextNot
f ¬¬f
BoxInduct
f (f f) f
InfChop
(f inf) ; g (f inf)
ChopStarEqv
f(empty ((f more) ; f))
ChopstarInduct
(inf f (f (g fmore) ; f)) g
MP
f0 f1, f0 ⇒ ⊢ f1
BoxGen
f0 ⇒ ⊢ f0
BiGen
f0 ⇒ ⊢ f0







2019-05-10
Contact | Home | ITL home | Course | Proofs | Algebra | FL