Biconditional elimination: is p↔q, p ⊨ q valid?
The two sides of p ↔ q always carry the same truth value, so p gives you q — and q would give you p. A biconditional works in both directions.
Valid
p↔q, p ⊨ qEvery branch of the tableau closes, so nothing makes the premises true and the conclusion false at once.
Proof (semantic tableau)
- 1True: p↔qpremise
- 2True: ppremise
- 3False: qnegated conclusion
- 4True: pfrom line 1
- 5True: qfrom line 1
Branch closed: line 5 contradicts line 3.
- 6False: pfrom line 1
Branch closed: line 6 contradicts line 2.
closed branch