Proving IMPLIES IDENTITY in David Beaver’s dynamic semantics

Question

Consider this principle, the Beaver analogue of the validity “if φ, then φ”: σ[φ implies φ]σ

L0:{atom, not, and, implies} L1: {atom, not, and, implies, ∂} L2:{atom,not,and,implies,□,♢}

Prove IMPLIES ID holds in L0. Prove that it does not hold in L2 by generating a counter example. Determine if IMPLIES ID holds in L1. If it does hold, prove it. If it does not, provide a counterexample.