摘要：基于廣義謝弗豎這種新算子,本文構(gòu)造了模態(tài)邏輯GL的模態(tài)表列和分析性模態(tài)公理系統(tǒng)。廣義謝弗豎是一種n元算子,為模態(tài)邏輯的表達(dá)式提供一種新記法,使分析性模態(tài)公理系統(tǒng)的陳述直接明了。由于謝弗豎是一種新算子,基于它的模態(tài)表列規(guī)則與通常的基于模態(tài)詞和聯(lián)結(jié)詞的表列規(guī)則有所不同。分析性模態(tài)公理系統(tǒng)中的內(nèi)定理證明很簡(jiǎn)單。因?yàn)榉治鲂阅B(tài)公理系統(tǒng)與模態(tài)表列之間存在某種對(duì)應(yīng)關(guān)系,所以GL的分析性模態(tài)公理系統(tǒng)的完全性由GL的模態(tài)表列的完全性結(jié)果易證。GL的模態(tài)系統(tǒng)的完全性證明比較特殊,無(wú)法直接應(yīng)用證明模態(tài)邏輯完全性的一般方法——典范模型方法,需要用一種過(guò)濾的方法挑出一些可能世界構(gòu)造有窮模型。