Theorem modal5

The analogue in our predicate calculus of axiom (5) of modal logic S5. See also hbe1. (Contributed by NM, 5-Oct-2005.)

Conclusion

\( \vdash \neg \forall x \, \neg \varphi \rightarrow \forall x \, \neg \forall x \, \neg \varphi \)

Proof

hbn1