摘要
构造基本命题逻辑BPL带标的矢列演算系统,该系统G_(3BPL)只有公理和逻辑规则,没有结构规则,结构规则被吸收在公理和逻辑规则中,并且所有的规则都是保持高度可逆的。证明弱化规则、收缩规则在G_(3BPL)中是保持高度可允许的,并证明切割消去定理,该系统具有弱子公式性质。
A label sequence calculus G3 BPLfor basic propositional logic is developed in the present paper.This system has axioms, logical rules and mathematical rule only. The structural rules are absorbed in these ax-ioms and logical rules. In addition, all the rules of G3 BPlare height-preserving invertible and the rules of weak-ening and contraction are height-preserving admissible. We proved the cut-elimination theorem holds forG3 BPL, this system has weak sub-formula property.
