How to prove, in modal logic, that □A→A is valid (T axiom) iff R is reflexive? I'm not sure how to prove axiom in reverse?
3 Answers
You are asking for a proof that the T axiom □A → A holds if and only if the corresponding frame condition R is reflexive. Note that since A is an arbitrary well-formed formula here, □A → A is logically equivalent by contraposition to A → ◇A.
Firstly, to show that if R is reflexive then A → ◇A holds, observe that for any P, if P is true at w, P is always true at some world accessible to w, namely at w itself, so A → ◇A holds.
Secondly, to show that if □A → A holds then R is reflexive, we can proceed by reductio. If it were not so, there would be some world w with an irreflexive frame, such that for some P, P holds in all worlds accessible to w, but not in w itself. But this would make □P true and P false at w, and hence □P → P would be false at w, contradicting the T axiom.
If by "in reverse" you mean proving that if R is not reflexive, then the T axiom isn't valid, it seems like what we need is to provide a model where R isn't reflexive, and there is a world in □A is true but A is false.
What you want to show is that every for every frame F = (W, R) it holds that: If the T-axiom is valid in F, then R is reflexive. It is possible to prove this by contraposition, but it is more common in logic to prefer direct proofs where they are available and so I will provide a direct one.
Let p be a propositional variable, assume that □p → p is valid in F = (W, R) and let w be any member of W. Take a valuation V that sends every variable q distinct from p to the empty set and that sends p to the set of R-successors of w; i.e. the set of exactly those members u of W such that wRu. Let M := (F, V). Take any v from W with wRv. Then v is a R-successor of w and we have that p is true in (M, v). Since v was arbitrary it follows that □p is true in (M, w). Since by assumption □p → p is true in (M, w), p is true in (M, w). So, w is a R-successor of w and so wRw. As w was arbitrary, R is reflexive.
To get the general result for arbitrary formulas A, we simply instantiate A with the variable p.
