Fitch 证明编辑器

量词和联结词可输入 ∀ ∃ ¬ ∧ ∨ → ↔，也可输入 任意 存在 非 且 或 蕴含 当且仅当。

还可使用小写反斜线命令 \forall \exists \not \and \or \implies \iff，例如 \forall x(P(x) \implies Q(x))。等号输入 =；不等号可输入 ≠ 或 \neq。同时支持常见别名 \neg \lnot \land \wedge \lor \vee \to \rightarrow \leftrightarrow \ne。 命令后若紧接字母，须用空格隔开。

二元联结词没有默认的优先级或结合方向。仅整个二元公式最外层的一对括号可省略； 嵌套的二元公式必须用括号明确分组。请写 (p ∧ q) → r 或 p ∧ (q → r)，不能写 p ∧ q → r。 否定词或量词若辖制二元公式，也须加括号，例如 ¬(p ∨ q)、 ∀x(P(x) → Q(x))。多余但正确配对的圆括号仍可使用。

变量使用 x y z，常元使用 a b c，函项使用 f g h，命题常元使用 p q r，谓词使用大写字母；均可带 _10 形式的下标。谓词与函项名称后须紧接左括号；它们的元数以首次出现为准。

否定引入和反证法所引用的子证明，末行须为 φ ∧ ¬φ 或 ¬φ ∧ φ 形式的公式。

引用示例：1, 3 或 4-7。子证明引用须写出从假设到末行的完整范围。 当前证明及所有外层证明中先前可用的行都可引用。