1. A sequent with only atoms is valid iff some formula occurs on
2. A, ¬ϕ ⇒ B iff A ⇒ B, ϕ
3. A ⇒ B, ¬ϕ iff A, ϕ ⇒ B
4. A, ϕ ∧ ψ ⇒ B iff A, ϕ, ψ ⇒ B
5. A ⇒ B, ϕ ∧ ψ iff both A ⇒ B, ϕ and A ⇒ B, ψ
These are facts about modal sequents...
How do we prove them?
For example 2. A, ¬ϕ ⇒ B iff A ⇒ B, ϕ
Where A and B = finite sets of wwfs
We suppose A, ¬ϕ ⇒ B first. Can we prove it without using contradiction method?
Supposing A not ⇒ B, ϕ and showing contradiction.
February 4th 2011, 12:26 AM
Welcome to the forum.
A, ¬ϕ ⇒ B iff A ⇒ B, ϕ
The sequent A, ¬ϕ ⇒ B is true, by definition, if is true and A ⇒ B, ϕ is true iff is true. Here denotes the conjunction of all formulas in A, and denotes the disjunction of formulas in B. In the following, however, let's pretend that A is and B is .
So, assume that is true; we need to show . Assume A. If is true, then the conclusion is true and we are done. If is true, then the first assumption implies B, so again the conclusion is true.
For the converse, assume is true; we need to show that is true. Assume A and . Then the first assumption implies . However, since is true, B is also true, as required.
Ultimately, each of the equivalences in your question corresponds to a tautology, which can be verified using a truth table. For example, (5) corresponds to .
Why do you refer to these sequents as "modal"? They seem to come from regular, not modal logic.