自然推理系统中的假设前提引入与消去规则

The Rule for Hypotheses and the Rule for Hypotheses Elimination in the System of Natural Inference

形式化的自然推理系统最显著的特点就是引入假设前提。在自然推理中,可以根据需要随时引入假设前提,但是推理的结论不能依赖于假设前提,因此假设前提在其完成了使命后,必须被消去。运用假设前提消去规则进行推理就是按照"如果A1,A2,…,An├B,那么A1,A2,…,An-1├An→B"的规则进行语形变换的过程,但是理解假设前提消去规则何以能够消去假设前提这个问题,涉及到对前提与结论之间真假制约情况的讨论,属于语义解释的范围。

Hypotheses introduction is the most important characteristic of the system of formalized natural inference.In the natural deduction,the hypothetical premise can be introduced at any time when needed,but it must be eliminated finally because the conclusion can not depend on it.It is a process of syntactic transformation to use the rule for hypotheses elimination to do an inference according to the rule＂If A1,A2,…,An├ B,then A1,A2,…,An-1 ├ An→B＂,but to understand the principle of work of the rule for hypotheses elimination relates to the discussion on the truth-value relation between premise and conclusion,which belongs to the range of semantic interpretation.