BetterFitchVIZIER

BetterFitchVIZIER

🏁

∧:and/&/* ∨:or/+ ¬:not/neg/! →:impl/-> ↔:bic ⊥:bot ∀:fa ∃:ex

Example proofs

A ∧ B ⊢ B ∧ A
P(a) ∧ P(b), a=c ∨ b=c ⊢ P(c)
∀x∃y R(x,y) → ∃y∀x R(x,y) ⊢ ∃x(∀y ¬R(x,y) ∨ ∀y R(y,x))

Advanced Settings (do not change unless you really have a good reason)

List of strings that should be recognized as variables (separated by commas):
(For example, using the default settings, having ∀x P(x) is allowed, but having ∀a P(a) is not, because a is not used for variables. With this setting, you can change which strings should be seen as a variable. All other strings that start with a lowercase letter will be seen as a constant or function symbol, depending on the context in which they are found.)

Rotate the proof by 180 degrees:

Fork by Lea Hailey | Source code