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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Morphing Rules of Evaluation into Rules of Deduction: Preserving Relevance and Epistemic Gain

  • Neil Tennant

摘要

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.