© 1996-2019

#### 8.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 diﬀerent since they lack a comparable axiom. Therefore, it is especially beneﬁcial 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 and ⊢ Lf ⊃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 fulﬁl 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 ﬁnite time is allowed, then and act as an S4 system. However, with inﬁnite time permitted does not fulﬁl the requirements of S4, or even those of the weaker modal system T, because Axiom T fails. Instead, with inﬁnite time fulﬁls 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 :

 K ⊢ L(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 ﬁnite 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 inﬁnite time is permitted. However, we prefer to work with and since the use of strong chop simpliﬁes 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 deﬁne 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:

 ⊢ LL′f ≡ L′Lf

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 ﬁnal step, recall that EqvChain indicates a chain of equivalences:

 ⊢ f ≡¬¬f Mdef

Proof:

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

qed

 ⊢ (f ⊃g) ⊃f ⊃g BfImpDfImpDf

Proof:

 1 (f ⊃g) ⊃(f ⌢ true) ⊃(g ⌢ true) BfChopImpChop 2 (f ⊃g) ⊃f ⊃g 1, def. of

qed

 ⊢ (¬g ⊃¬f) ⊃( f) ⊃( g) BfContraPosImpDist

Proof:

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

qed

 ⊢ (f ⊃g) ⊃( f) ⊃( g) BfImpDist

Proof:

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

qed

 ⊢ f ⊃g ⇒ ⊢ f ⊃g BfImpBfRule

Proof:

 1 f ⊃g Assump 2 (f ⊃g) 1,BfGen 3 (f ⊃g) ⊃( f) ⊃( g) BfImpDist 4 f ⊃g 2, 3,MP

qed

 ⊢ f ≡ g ⇒ ⊢ f ≡g BfEqvBfRule

Proof:

 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

qed

 ⊢ (f ∧ g) ≡f ∧g BfAndEqv

Proof:

 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

qed

 ⊢ (f ≡ g) ≡(f ⊃g) ∧(g ⊃f) BfEqvSplit

Proof:

 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

qed

 ⊢ (f ≡ f1) ⊃(f ⌢ g) ≡ (f1 ⌢ g) BfChopEqvChop

Proof:

 1 (f ≡ f1) ≡(f ⊃f1) ∧(f1 ⊃f) 2 (f ⊃f1) ⊃(f ⌢ g) ⊃(f1 ⌢ g) BfChopImpChop 3 (f1 ⊃f) ⊃(f1 ⌢ g) ⊃(f ⌢ g) BfChopImpChop 4 (f ≡ f1) ⊃(f ⌢ g) ≡ (f1 ⌢ g) 1 −−3,Prop

qed

 ⊢ (f ≡ g) ⊃f ≡g BfImpDfEqvDf

Proof:

 1 (f ≡ g) ⊃(f ⌢ true) ≡ (g ⌢ true) BfChopEqvChop 2 (f ≡ g) ⊃f ≡g 1, def. of

qed

 ⊢ ﬁnite ⊃(f ≡ g) ⇒ ⊢ f ≡g FiniteImpDfEqvDfRule

Proof:

 1 ﬁnite ⊃(f ≡ g) Assump 2 (f ≡ g) 1,BfFGen 3 (f ≡ g) ⊃f ≡g BfImpDfEqvDf 4 f ≡g 2, 3,MP

qed

 ⊢ f ⊃f BfImpDf

Proof:

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

qed

 ⊢ (f ∨ g) ≡f ∨g DfOrEqv

Proof:

 1 (f ∨ g) ⌢ true ≡ (f ⌢ true) ∨ (g ⌢ true) OrChopEqv 2 (f ∨ g) ≡f ∨g 1, def. of

qed

 ⊢ f ∧ (f1 ⌢ g) ⊃(f ∧ f1) ⌢ g BfAndChopImport

Proof:

 1 f ⊃(f1 ⊃f ∧ f1) 2 f ⊃(f1 ⊃f ∧ f1) 3 (f1 ⊃f ∧ f1) ⊃(f1 ⌢ g) ⊃(f ∧ f1) ⌢ g BfChopImpChop 4 f ∧ (f1 ⌢ g) ⊃(f ∧ f1) ⌢ g 2, 3,Prop

qed

 2019-01-03 Contact | Home | ITL home | Course | Proofs | Algebra | FL