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


introelim
  
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
introelim
 
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.

[Back to Fitch, 1st-order]