FitchVIZIER

FitchVIZIER

🏁 Exercise target:

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

FitchVIZIER WebUI

The WebUI tries to save your proofs in the local storage, but always save your proofs as .txt files if you don't want to loose them!

To input logical symbols like ∧ and ∀ use the legend above, e.g. type out `and' for producing ∧.

The WebUI also supports the following key bindings:

Ctrl S: (re)format the proof

Ctrl -/=: decrease/increase font size

Enter: insert a new line with a fresh line number

Shift Enter: insert a new line without a fresh line number

Tab/Shift Tab: increase/decrease the subproof depth

If you wish, you can also try a much more spartan SimpleUI.

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))

Settings

Appearance

Automatic Light Dark

Automatic follows your system appearance setting.

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: