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 object constants you wish to add to the vocabulary:
Enter the object constants you wish to delete from the vocabulary:
Enter the function constants you wish to add to the vocabulary:
Enter the function constants you wish to delete from the vocabulary:
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:
Implication Introduction:
φ => (ψ => φ)
Enter values for the meta-variables in the schema:
φ:
ψ:
Implication Distribution:
(φ => (ψ => χ)) => ((φ => ψ) => (φ => χ))
Enter values for the meta-variables in the schema:
φ:
ψ:
χ:
Implication Reversal:
(~ψ => ~φ) => (φ => ψ)
Enter values for the meta-variables in the schema:
φ:
ψ:
Universal Instantiation:
Aν:φ => φ[ν←τ]
where τ is free for ν in φ
Enter values for the meta-variables in the schema:
ν:
φ:
τ:
Substitution:
μ=ν => (φ => φ[μ←ν])
where τ is free for ν in φ
Enter values for the meta-variables in the schema:
μ:
ν:
φ:
Universal Distribution:
Aν:(φ => ψ) => (φ => Aν:ψ)
where ν does not occur free in φ.
Enter values for the meta-variables in the schema:
