### Inference rules for Fitch, 1st-order

This brief manual assumes that you have read the help page for Truth Table and Fitch, Propositional in Proofmood.

In what follows, the expression φ(x) does not imply that x occurs in φ as a free variable, nor φ has no free variable other than x. We use the expression φ(t) to denote the formula that is obtained by substituting each free occurrence of x in φ(x) by t. (Provided that the substitution condition is met, of course.) In case there is no free occurrence of x in φ, φ(t) is identical to φ(x).

 intro elim ∀  c is a fresh constant, x is a fresh individual variable. We may use ∀y φ(y) in place of ∀x φ(x). t is free to substitute x in φ ∃ t is free to substitute x in φ  c is a fresh constant and does not occur in θ. x is a fresh free variable and does not occur freely in θ. = t is a term. No variable occurring in t1,t2,s1,s2 cannot occur as a bound variable in α. TautConsq  The conclusion is a tautological consequence of premises. We may use subproofs as premises. Extended Rules intro elim ∀   We may use x1,x2 in place of c1,c2, and ∀x2∀x1 in place of ∀x1∀x2. ∃   We may use x1,x2(or y1,y2) in place of c1,c2, and ∃x2∃x1 in place of ∃x1∃x2. = elim   Symmetricity   = elim for identity   Transitivity ∀= elim We may use ∀x1∀x2(t(x1,x2)=s(x1,x2)) in place of t(x1,x2)=s(x1,x2) as a premise of [= elim] inference. In this case, Proofmood behaves as if the premise t(r1,r2)=s(r1,r2) exists for some suitable terms r1 and r2. For transitivity, we may use such a universal formula for the last premise only. ∀→  We may use {c1,c2} etc. in place of {c}. We use the menu [∀ intro] for this extended rule of inference. We may use ∀x1∀x2 etc. in place of ∀x. We use the menu [∀ elim] for this extended rule of inference. Associative An equation that can be obtained by applying the associativity ∀x∀y∀z(x·y·z = x·(y·z)) and [= elim] several times, e.g., a·(b·c)·(d·e) = a·(b·(c·d))·e can be obtained by applying this rule of inference only once. The associativity axiom ∀x∀y∀z(x·y·z = x·(y·z)) should exist as a premise. Lemmas In the 6 formulas related to dummy, antecedent and consequent, x does not appear in β freely. EquivRepl Line 10, the conclusion is obtained from the last premise(line 9) by replacing suitably chosen terms and subformulas in line 9 by terms and formulas designated as equivalent by the other premises(line 6,7,8). The substitution condition must be met of course. MetaSubst Substitute the formula φ(z), where a metasymbol φ occurs, with some other formula. If there exists a free variable of the substituting formula (¬(z=z)) which is not a free variable of φ,it must appear in the consequence formula (line 4) as a free variable.