Fitch

Logica

Tools
for
Thought

Fitch

Undo

Copy

Paste

Load

Save

Library

Help

To apply a rule of inference, check the lines you wish to use as premises and click the button for the rule of inference. Reiteration allows you to repeat an earlier item. To delete one or more lines from a proof, check the desired lines and click Delete. When entering expressions, use Ascii characters only. Use ~ for ¬; use => for ⇒; use A for ∀; and use : for . in quantified sentences. Also, for variables use strings of alphanumeric characters that begin with a capital letter. For example, to write the sentence ∀x.(p(x) ⇒ ¬s(x)), write AX:(p(X)=>~s(X)).

Objects	a, b, c
Functions	f, g

Enter the premise you wish to add to the proof:

Select premises.
Enter your proposed conclusion:

Must be provable from selected premises via truthtable.

Enter the conclusion you wish to add to the proof:

Enter the justification for this conclusion:

Enter the symbol you wish to replace:

Enter the replacement:

Enter the sentence you wish to disjoin to the checked items:

Or Elimination:

φ∨ψ
φ⇒χ
ψ⇒χ

Enter the assumption you wish to make:

Universal Introduction:

Aν:φ_τ⇐ν
where τ is not used in any active assumptions

Enter the placeholder you would like to replace:

τ:

Enter the variable you would like to use:

ν:

Universal Elimination:

Aν:φ

φ_ν⇐τ
where τ is ground

Enter the term you would like to use:

τ:

Existential Introduction:

Eν:φ_τ←ν
where τ is ground

Enter the term you would like to replace:

τ:

Enter the variable you would like to use:

ν:

Existential Elimination:

Eν:φ
Aν(φ=>ψ)

ψ
where ν does not occur free in ψ

Enter the universal conclusion you wish to make: