中介命题系统MP推理规则的独立性问题

Independent Problem of Inference Rules of Medium Propositional System MP

对于一个形式系统而言 ,在不改变其完备性的前提下 ,形式越简洁 ,使用越方便。现在中介命题系统MP推理规则集 S的简化等价集 S1已经建立 ,其中 S1共有 1 4条推理规则 ,如果这些推理规则中有一条可以由 S1的其余推理规则推导出来 ,那么它就是不独立的 ,可以将其删去而不影响形式系统 S1的效力 ,从而得到形式上更为简洁的系统。为此目的笔者利用值模型法对形式系统 S1的每条推理规则的独立性一一进行了探讨 ,发现一条不独立的规则 。

As to a formal system, the simpler form makes it more convenient to use without altering its perfection. Now the more simple same aggregate S 1 of inference rules of S in the medium prepositional system, with 14 formal inference rules has been established. If one of them can be inferred by the others, then it is not independent, then we can omit it from S 1 without affecting the effect of S 1 , and we will have a simpler system. For this sake, the author discusses the independency of every inferencer Rule of S 1 by constructing different digital models, the author not only finds a dependent inference rule but also proves each of the other 13 inference rules, which is independent with the others.