ITL
© 1996-2018







17.2 Some Properties of involving the Modal System K and Axiom D

The two pairs of operators and and and obey various standard properties of modal logics. Axiom VPTL helps streamline reasoning involving and . The situation with and is quite different since they lack a comparable axiom. Therefore, it is especially beneficial to review some conventional modal systems which assist in organising various useful deductions involving and .

Table 5 summarises some relevant modal systems, various associated axioms and inference rules.


System
Axiom or inference rule
Axiom or rule name




K: Mf ¬L¬f M-def
plus L(f g) (Lf Lg) K
plus f ⇒ ⊢ Lf N
T: K plus Lf f T
S4: T plus Lf LLf 4
KD4: K plus 4 andLf Mf D

Table 5: Some standard modal systems

Within PITL, as in PTL, the operator can be regarded as the conventional unary necessity modality L and the operator as the dual possibility operator M. The two operators together fulfil the requirements of the modal system S4. We do not need to explicitly prove versions of the S4 axioms in Table 5 for and . Rather, any PITL formula which is a substitution instance of a valid S4 formula involving and can be readily deduced using the PITL proof system’s Axiom VPTL. Similarly, inference rules based on S4 can be obtained with Axiom VPTL, Inference Rule BoxGen (which corresponds to the inference rule N of S4) and modus ponens. Moreover, the PITL proof system’s Axiom VPTL permits using any PITL formula which is a substitution instance of some valid PTL formula which can also contain the PTL operator . In view of all this, we do not give much further consideration to aspects of S4 with and .

In contrast to , the PITL operator does not have a comprehensive axiom analogous to VPTL. Therefore, we need to explicitly prove in the PITL axiom system various modal properties of and its dual . If only finite time is allowed, then and act as an S4 system. However, with infinite time permitted does not fulfil the requirements of S4, or even those of the weaker modal system T, because Axiom T fails. Instead, with infinite time fulfils the requirements of the modal system KD4 which is strictly weaker than S4.

Here is a list of KD4’s axioms and inference rules and related PITL proofs for :

KL(f g) (Lf Lg)Theorem BfImpDist
N f ⇒ ⊢ Lf Derived Inf. Rule BfGen
D Lf Mf Theorem BfImpDf
4 Lf LLf Theorem BfImpBfBf

If only finite time is allowed, then the implication D does not need to be regarded as an explicit axiom since it can be inferred from any proof system for S4.

It is also worth noting that the related operators and obey the modal system S4 even when infinite time is permitted. However, we prefer to work with and since the use of strong chop simplifies the overall PITL completeness proof.

Conventional model logics usually take L, not M, to be primitive. When we deduce standard modal properties for and in our PITL axiom system, we let M, which corresponds to , be primitive and define L to be M’s dual (i.e., LA ¬M¬f). This M-based approach goes well with the PITL axioms for chop. Chellas discusses some alternative axiomatisations of modal systems with M as the primitive although none correspond directly to ours. For the system K, we can deduce implication LImpMImpM below for and (see Theorem BfImpDfImpDf later on) and then obtain from it together some other reasoning the more standard axiom K just presented which only mentions L:


L(f g) (Mf Mg) LImpMImpM


The operators and together yield a multi-modal logic with two necessity constructs L and Lwhich are commutative:

LLf LLf

This corresponds to our Theorem BfBoxEqvBoxBf given later on.

Below are various theorems and derived inference rules about and for obtaining the axioms M-def (Theorem Mdef) and K (Theorem BfImpDist) found in the modal system K. The associated inference rule N was already proved above as Derived Inference Rule BfGen. We also prove the modal axiom D (Theorem BfImpDf).

In the next proof’s final step, recall that EqvChain indicates a chain of equivalences:


f ≡¬¬f Mdef


1
f ≡¬¬f
2
f ¬¬f
3
¬¬f ≡¬¬¬¬f
4
¬¬f ≡¬¬f
3, def. of 
5
f ≡¬¬f


(f g) f g BfImpDfImpDf


1
(f g) (f true) (g true)
2
(f g) f g
1, def. of 


(¬g ¬f) ( f) ( g) BfContraPosImpDist


1
(¬g ¬f) ( ¬g) ( ¬f)
2
(¬g ¬f) (¬¬f) (¬¬g)
1,Prop
3
(¬g ¬f) ( f) ( g)
2, def. of 


(f g) ( f) ( g) BfImpDist


1
(f g) (¬g ¬f)
2
¬(¬g ¬f) ¬(f g)
1,Prop
3
(¬(¬g ¬f) ¬(f g))
4
(¬(¬g ¬f) ¬(f g))
(f g) (¬g ¬f)
5
(f g) (¬g ¬f)
3, 4,MP
6
(¬g ¬f) ( f) ( g)
7
(f g) ( f) ( g)
5, 6,ImpChain


f g ⇒ ⊢ f g BfImpBfRule


1
f g
Assump
2
(f g)
3
(f g) ( f) ( g)
4
f g
2, 3,MP


f g ⇒ ⊢ f g BfEqvBfRule


1
f g
Assump
2
f g
1,Prop
3
f g
4
g f
1,Prop
5
g f
6
f g
3, 5,Prop


(f g) f g BfAndEqv


1
(f g) f
2
(f g) f
3
(f g) g
4
(f g) g
5
f (g (f g))
6
f (g (f g))
7
(g (f g)) ( g (f g))
8
f g (f g)
6, 7,Prop
9
(f g) f g
2, 4, 8,Prop


(f g) (f g) (g f) BfEqvSplit


1
(f g) (f g) (g f)
2
(f g) ((f g) (g f))
3
((f g) (g f)) (f g) (g f)
4
(f g) (f g) (g f)
2, 3,EqvChain


(f f1) (f g) (f1 g) BfChopEqvChop


1
(f f1) (f f1) (f1 f)
2
(f f1) (f g) (f1 g)
3
(f1 f) (f1 g) (f g)
4
(f f1) (f g) (f1 g)
1 −−3,Prop


(f g) f g BfImpDfEqvDf


1
(f g) (f true) (g true)
2
(f g) f g
1, def. of 


finite (f g) ⇒ ⊢ f g FiniteImpDfEqvDfRule


1
finite (f g)
Assump
2
(f g)
3
(f g) f g
4
f g
2, 3,MP


f f BfImpDf


1
f (empty f)
2
f (empty f)
3
(empty f) ( empty f)
4
f ( empty f)
2, 3,ImpChain
5
empty
6
f f
4, 5,Prop


(f g) f g DfOrEqv


1
(f g) true (f true) (g true)
2
(f g) f g
1, def. of 


f (f1 g) (f f1) g BfAndChopImport


1
f (f1 f f1)
2
f (f1 f f1)
3
(f1 f f1) (f1 g) (f f1) g
4
f (f1 g) (f f1) g
2, 3,Prop







2018-02-26
Contact | Home | ITL home | Course | Proofs | Algebra | FL