2.4 Propositional proof system

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

Table 7: Propositional Axioms and Rules for finite 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
ChopStarEqv
f(empty ((f more) ; f))
MP
f0 f1, f0 ⇒ ⊢ f1
BoxGen
f0 ⇒ ⊢ f0
BiGen
f0 ⇒ ⊢ f0

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