Abstract

This study seeks to reveal the proper source of the (correct) rules of natural deduction (and their associated rules of the sequent calculus). Perhaps surprisingly, this source consists of just the familiar truth tables (deriving from Frege). These tables can be construed inferentially. The primitive steps of value-computation correspond to primitive steps of ‘inference’. We shall call them, however, primitive steps (or rules) of evaluation. These can be steps of verification or of falsification. The rules of evaluation constitute the inductive clauses in a metalinguistic co-inductive definition of model-relative verifications and falsifications.We then show how the rules of evaluation can be ‘morphed’ into rules of natural deduction. Rules of verification thereby become introduction rules, and rules of falsification become elimination rules. The morphing produces model-invariant rules in the simplest way possible. It preserves, for natural deduction, the feature of relevance that is involved in truth-tabular computation. This makes for a system of natural deduction (and a directly corresponding sequent calculus) that is relevant.