Terminology 39: We will state inference rules (or just rules), each taking as premises finitely many inferences of one of the forms \vdash \phi \hspace{5mm} \textup{or} \hspace{5mm} \phi \vdash \psi (i.e. that a statement \phi holds or entails another statement \psi ), yielding one such inference as the conclusion. We may express this using the notation \cfrac{\textup{Premise A} \quad \textup{Premise B} \quad \cdots \quad \textup{Premise Z}}{\textup{Conclusion}} Some inference rules will be declared. We accept that given inferences fitting such a rule’s premises, when each inference is already justified or of the form \vdash \phi where \phi is an assumption, the corresponding conclusion is also justified. Additional inference rules will be verified using these declared rules.