一阶逻辑推理系统F下量词的性质及运算规律

Character and Operation Rule of the Classifier in First Logic Reasoning System F

量词在一阶逻辑推理中起着重要作用,然而它的性质及运算规律比较繁杂,关于它的一些等值式和蕴涵式不能像在命题逻辑中那样用真值表来验证,本文将给出一系列的论证.

The classifier is playing the vital role in first logic reasoning. However its poeration rule is more comples. Some of equivalent types and the implication type can＇t be proved by the matrix unlike propositional logic. This article will summarize them and give a series of proofs.