▶ Here you can easily type logic and mathematics formulas and use them anywhere.

Examples:
forall S forsome P forall x(x elem P <=> x psubset S)∀S ∃P ∀x(x∈P⇔x⊂S)
[](p-)q)-)<>(p-)q)◻(p⊃q)⊃◇(p⊃q)
IPC |/- phi \/ --phiIPC⊬𝜙∨¬𝜙
--phi =- phi -> _|¬𝜙≡𝜙→⊥
Gamma |= phi => Gamma |- phiΓ⊨𝜙⇒Γ⊢𝜙

▶ You can check whether the entered formula(s) make a valid inference by clicking the Evaluate button.