數(shù)理邏輯(數(shù)據(jù)庫)

時間：2022-11-22 22:30:01 | 來源：信息時代

時間：2022-11-22 22:30:01 來源：信息時代

    數(shù)理邏輯 : 一門研究數(shù)學基礎性問題的數(shù)學,它為歷史悠久的宏偉的數(shù)學大廈起奠基與支撐作用。
數(shù)理邏輯發(fā)展于19世紀,在其出現(xiàn)的初期,它的主要目標是研究數(shù)學推理的形式化,這形成了經(jīng)典數(shù)理邏輯時代(或稱傳統(tǒng)數(shù)理邏輯時代),并在以后出現(xiàn)了命題邏輯,一階謂詞邏輯,以及高階邏輯等多種分支。
到20世紀初由于數(shù)學發(fā)展而引發(fā)的眾多基礎性問題而促進了數(shù)理邏輯的發(fā)展并形成了四個分支,它們是: 公理集合論、模型論、證明論及遞歸論。
到了近期,在20世紀70年代后由于應用的促進,非經(jīng)典邏輯得到了發(fā)展,它包括多值邏輯、模態(tài)邏輯、時態(tài)邏輯、非單調(diào)邏輯及模糊邏輯等。
由于數(shù)學基礎問題也是其他眾多學科的基礎性問題,特別是新近興起的計算機科學,迫切需要解決其發(fā)展中的基礎問題。因此,數(shù)理邏輯同樣作為計算機科學中的基礎問題的研究工具而與其發(fā)生了緊密的關系,并且對計算機科學的發(fā)展起到了有力的奠基與推動作用。
在數(shù)據(jù)庫的發(fā)展中,數(shù)理邏輯同樣也起到了重要的作用。E.F.codd在1970年創(chuàng)立關系數(shù)據(jù)庫時,首先利用了關系代數(shù)與關系演算作為數(shù)學模型以建立起關系數(shù)據(jù)庫的基礎理論,為關系數(shù)據(jù)庫發(fā)展奠定了堅實的基礎。在此中即應用了數(shù)理邏輯中的一階謂詞邏輯與集合論理論,在關系數(shù)據(jù)庫標準語言SQL中還大量應用了謂詞、量詞、布爾表達式、集合運算等數(shù)理邏輯中的方法與理論。數(shù)理邏輯在數(shù)據(jù)模型研究中,除了在關系模型外,還在其他模型研究中,如謂詞模型,函數(shù)模型中發(fā)揮作用。在此后的演繹數(shù)據(jù)庫(deductive database)及知識庫(knowledge base)研究中大量地采用了數(shù)據(jù)邏輯中的公理化思想與推理理論,并引入了證明論與模型論理論,為研究演繹數(shù)據(jù)庫及知識庫起到了強有力的推進作用。在時態(tài)數(shù)據(jù)庫、模糊數(shù)據(jù)庫等特種數(shù)據(jù)庫研究中也采用非經(jīng)典邏輯作為其理論工具。在目前,有關數(shù)據(jù)倉庫、OLAP及數(shù)據(jù)挖掘中,均應用了歸納邏輯,模糊邏輯等多種邏輯思想與方法。
在早期的數(shù)理邏輯中是采用數(shù)學的方法研究演繹推理的規(guī)則,所謂數(shù)學方法主要指的是引入一套符號體系進而建立一種形式系統(tǒng),因此,數(shù)理邏輯又稱為符號邏輯。具體地說,形式系統(tǒng)的建立,包括符號、公式、有效公式、公理、推理規(guī)則、證明及定理等若干個過程與步驟,這種形式系統(tǒng)也可稱為公理化系統(tǒng)。
(1)符號: 一個形式系統(tǒng)的基礎是一組確定的,有限個數(shù)的符號。
(2)公式:根據(jù)一定的形成規(guī)則由符號所組成的有限長度的符號串稱公式,也稱形式語言。
(3)有效公式:形式系統(tǒng)中具有肯定性論斷的公式稱有效公式。
(4)公理: 形式系統(tǒng)中部分有效公式稱為公理。
(5)推理規(guī)則:形式系統(tǒng)中具推理功能的規(guī)則稱推理規(guī)則,推理規(guī)則是由某些公式作為前提而獲得另一個公式作為結果的過程。
(6)公理系統(tǒng): 由公理及推理規(guī)則組成公理系統(tǒng)。
(7)證明及定理:證明是有限個公式的序列,這種公式由下面幾部分組成: ①公理是證明中公式;② 由序列前面公式中的若干個為前提,通過推理規(guī)則所得到的結果是證明中公式;③公式序列中的最后一個公式是定理。
(8)形式系統(tǒng): 由公理系統(tǒng)、證明及定理構成一個形式系統(tǒng),形式系統(tǒng)是一種純語法的系統(tǒng),它具有高度抽象性與理論性。
(9)形式系統(tǒng)的不矛盾性、獨立性與完全性:形式系統(tǒng)是需要研究的,研究包括所建系統(tǒng)是否會出現(xiàn)矛盾,是否是最小的以及是否包含所有有效公式,這就是形式系統(tǒng)的不矛盾性、獨立性與完全性。
形式系統(tǒng)的不矛盾性即表示在該系統(tǒng)中若A為定理,則A必不為定理,或者說在該系統(tǒng)中不可能存在A與A均為定理。
形式系統(tǒng)的獨立性即表示在系統(tǒng)中沒有多余的公理與推理規(guī)則,亦即是說只要去掉系統(tǒng)中任一公理或推理規(guī)則系統(tǒng)中的定理即會減少。
形式系統(tǒng)的完全性即表示系統(tǒng)的定理都是有效公式。
一般而言,形式系統(tǒng)的不矛盾性是極端重要的,因為一個矛盾的系統(tǒng)任何公式均可證明為有效,因此,也是無用的系統(tǒng),而形式系統(tǒng)的完全性表示系統(tǒng)是否存在缺陷; 最后形式系統(tǒng)的獨立性,追求的是形式上的完美,一個不具獨立性的系統(tǒng)對整個系統(tǒng)的推理與完全性不受任何影響,因此,一個形式系統(tǒng)必須是不矛盾的同時希望是完全的但并不一定需要是獨立的。
20世紀初數(shù)理邏輯形成了幾種新的分支:
(1)公理集合論(axiom set theory): 在數(shù)學的各分支中其研究對象的概念、定義、定理與證明等均可用集合論形式表示,因此,集合論是數(shù)學研究中的公共基礎; 而集合論的基礎則是有關集合論的公理系統(tǒng),稱為公理集合論,因此,公理集合論是整個數(shù)學基礎中的核心。G.Contor于19世紀末創(chuàng)立了集合論,B.Russell發(fā)現(xiàn)了集合論中的悖論,從而引發(fā)了對公理集合論的研究。E.Zermelo與A.Fraenkel建立了第一個集合論公理系統(tǒng)ZF系統(tǒng),此后尚有P.Baruags和K.Godel所提出的著名的GB系統(tǒng),這些公理系統(tǒng)都為排除集合論中悖論作出了貢獻。
(2)模型論(model thoery):是研究形式系統(tǒng)與對它解釋之間關系的一種理論。我們知道,形式系統(tǒng)是一種語法系統(tǒng),它可以有多種語意上解釋,研究它們之間的關系是模型論的研究目標。模型論研究起源于20世紀20年代,由T.Skolem等人奠定基礎,并于50年代正式形成理論,其代表人物是A.Tarski及A.Robinson等人。
模型論的基本思想是: 一個形式語言的解釋稱為此語言的結構(也稱模型),在模型論中形式語言一般采用一階邏輯語言(或簡稱一階語言),因此,也稱一階模型論。
一階謂詞模型論(以下簡稱為模型論)由三元組(L,∑,M)組成,三元組中L,∑,M的含義分別如下: L表示語言,即指定模型所采用的數(shù)學語言,亦即是一種基于一階謂詞的邏輯語言。它由一些常量、變量、函數(shù)、謂詞等按一階謂詞邏輯公式定義的要求所構成。它的基本組成單元是句子。句子即是一階謂詞邏輯中的公式。如一句子中變量均呈約束狀態(tài),則稱該句子為語句。L-語言為模型論理論提供了書寫的語言?！剖怯肔-語言所寫的一個句子集。一般講,該句子呈語句狀,∑刻畫了所研究對象的普遍性規(guī)律。M是一個解釋,稱為結構或L-結構。在L中常量、函數(shù)、謂詞均可賦值,變量可確定值域。因此,對L中常量、函數(shù)、謂詞的一組賦值,變量的一種定義域指定叫L的一個解釋,或叫一個結構。
L中可以有多個解釋,但是人們最感興趣的解釋是使∑為真的那些解釋。設∑={σ₁,σ₂,…,σ_n},其中σ_i為L的句子,如有解釋M使σ_i為真,則該M是σ_i的一個模型,如有解釋M使所有σ_i(i=1,2,…,n)為真,則該M是∑的一個模型,并可記為:M|=∑。模型論即是研究滿足M|=∑的三元組(L,∑,M)的數(shù)學理論。
(3)證明論(proof theory): 是以數(shù)學證明作為研究對象的一種數(shù)學理論,它特別研究數(shù)學系統(tǒng)的不矛盾性及完全性。證明論出現(xiàn)于20世紀20年代,由D.Hilbert等人在研究了數(shù)論、集合論及數(shù)學分析等數(shù)學系統(tǒng)的不矛盾性而開始。30年代,K.Godel研究了數(shù)學系統(tǒng)的完全性而得到了著名的哥德爾不完全性定理,此后又得到了哥德爾第二不完全性定理。
眾多的證明論研究表明: 雖然形式化方法是一種有效的方法,但是它過于抽象的語法化傾向,從而存在著嚴重的局限性與片面性。
(4)遞歸論(recurse theory): 是研究算法理論的一種數(shù)學,它主要研究算法的一般性規(guī)律以及數(shù)學中一類問題是存在算法介的問題,可稱為判定問題,其詳細介紹可參見算法、可計算性理論。