基本命題邏輯BPLBPL帶標的矢列演算系統(tǒng)

陳鈺

?

基本命題邏輯BPLBPL帶標的矢列演算系統(tǒng)

陳鈺

（西南大學(xué)政治與公共管理學(xué)院，重慶400715）

構(gòu)造基本命題邏輯BPL帶標的矢列演算系統(tǒng)，該系統(tǒng)只有公理和邏輯規(guī)則，沒有結(jié)構(gòu)規(guī)則，結(jié)構(gòu)規(guī)則被吸收在公理和邏輯規(guī)則中，并且所有的規(guī)則都是保持高度可逆的。證明弱化規(guī)則、收縮規(guī)則在中是保持高度可允許的，并證明切割消去定理，該系統(tǒng)具有弱子公式性質(zhì)。

帶標的矢列演算系統(tǒng)；基本命題邏輯；證明論。

1　引言

通過將蘊涵解釋為形式可證，維瑟（A.Visser）提出了形式命題邏輯FPL。［8］在構(gòu)造FPL之前，他首先構(gòu)造了基本命題邏輯BPL，并給出了其自然演繹規(guī)則，證明其相對于傳遞框架是可靠的和完全的。后來，鈴木（Y.Suzuki）&小野（H.Ono）給出了BPL的希爾伯特式公理化系統(tǒng)［7］，石井（K.Ishii）&鹿島（R. Kashima）&菊池（K.Kikuchi）給出了其矢列演算系統(tǒng)，并證明了切割消去定理，而且該系統(tǒng)保證了子公式性質(zhì)。［2］

帶標的演繹系統(tǒng)（Labelled Deductive System）最早由加貝（D.M.Gabbay）系統(tǒng)提出［1］，辛普森（A.Simpson）運用這一方法從證明論的角度研究了直覺主義模態(tài)邏輯。［6］內(nèi)格里（S.Negri）運用帶標的演繹系統(tǒng)研究了模態(tài)邏輯、非經(jīng)典邏輯以及中間邏輯系統(tǒng)。［4］［5］［3］但是，BPL作為比直覺主義邏輯更弱的邏輯，并沒有得到具體的研究。因而，本文將運用這一方法，構(gòu)建BPL帶標的矢列演算系統(tǒng)，并證明其相關(guān)性質(zhì)。

2　BPL的語言和語義

現(xiàn)在介紹鈴木（Y.Suzuki）&小野（H.Ono）給出的基本命題邏輯的公理系統(tǒng)，它包含如下公理模式和推理規(guī)則。［7］

證明：參見［7］.

3　BPL帶標的矢列演算系統(tǒng)

公理

邏輯規(guī)則

數(shù)學(xué)規(guī)則

下面開始討論的一些結(jié)構(gòu)性質(zhì)。在討論之前，需要引入代入的概念及其引理，這在證明的結(jié)構(gòu)性質(zhì)需要用到。

有了這個代入的定義，我們有如下引理。

證明：與內(nèi)格里（S.Negri）［3］類似。

證明：與內(nèi)格里（S.Negri）［3］類似。

定理3.1弱化規(guī)則：

定理3.3收縮規(guī)則：

那么，根據(jù)歸納假設(shè)有

其他聯(lián)結(jié)詞情況類似。

那么，根據(jù)歸納假設(shè)我們有

定理3.4切割規(guī)則：

可以轉(zhuǎn)換成

其他規(guī)則類似。

可以轉(zhuǎn)換成

可以轉(zhuǎn)換成

其他規(guī)則類似。

可以轉(zhuǎn)換成

可以轉(zhuǎn)換成

其中轉(zhuǎn)換后的兩個前提分別由如下推演得到：

切割消去定理至此證畢。

推論3.1（弱子公式性質(zhì)）在一個推演中出現(xiàn)的所有公式或者是最底層的矢列的子公式，或者是形如的關(guān)系原子公式。

4　結(jié)語

注釋：

［1］Gabbay D M.LDS-labelled deductive systems［M］.ICON Group International，1990:11-17.

［2］Ishii K，Kashima R，Kikuchi K.Sequent calculi for Visser's propositional logics［J］.Notre Dame Journal of Formal Logic，2001（1）:1-22.

［3］Negri S，Von Plato J.Proof analysis:a contribution to Hilbert's last problem［M］.Cambridge University Press，2011:185-249.

［4］Negri S.Proof analysis in modal logic［J］.Journal of Philosophical Logic，2005（5-6）:507-544.

［5］Negri S.Proof analysis in non-classical logics［C］//Logic Colloquium.2005:107-128.

［6］Simpson A，Simpson A.The Proof Theory and Semantics of Intu-itionistic Modal Logic［D］.University of Edinburgh，1994:65-84.

［7］Suzuki Y，Ono H.Hibert style proof system for BPL［J］.Research report，1997（10）:1-8.

［8］Visser A.A propositional logic with explicit fixed points［J］.StudiaLogica，1981（2）:155-175.

Sequence Calculus System for Basic Propositional Logic

CHEN Yu
（School of Politics and Public Administration of Southwest University，Beibei，Chongqing400715，China）

A label sequence calculus G3BPLfor 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 axioms and logical rules.In addition，all the rules of G3BPlare height-preserving invertible and the rules of weakening and contraction are height-preserving admissible.We proved the cut-elimination theorem holds for G3BPL，this system has weak sub-formula property.

Label Sequence Calculus；Basic Propositional Logic；Proof Theory.

B81

A

2096-0239（2016）03-0072-07

（責編：彭麟淋責校：明茂修）

2016-04-23

陳鈺（1991- ），男，江西贛州人，西南大學(xué)政治與公共管理學(xué)院研究生。研究方向：現(xiàn)代邏輯。