|
|
樓主 |
發表於 2012-7-22 12:40:05
|
顯示全部樓層
回復 deal1wak #55 的帖子
喂你條７頭自己睇!
在邏輯中，特別是數理邏輯中，推理規則(推論規則)是構造有效推論的方案。這些方案建立在一組叫做前提的公式和叫做結論的斷言之間的語法關係。這些語法關係用於推理過程中，新的真的斷言從其他已知的斷言得出。規則也適用於非形式邏輯和邏輯論證，但是形式化更加困難和有爭議。
按照規定，推理規則的應用純粹是語法過程。儘管如此它必須是有效的，或者更精確地說保持有效性。為了使保持有效性的要求有意義，某種形式的語義與推理規則有關和推理規則自身的斷言是必需的。對於在推理規則和和語義之間相互關係的討論請參見命題邏輯。
命題邏輯中推理規則的顯著例子是肯定前件和否定後件規則。對於一階謂詞邏輯，推理規則需要處理邏輯量詞。對這種論證的更詳細的描述請參見有效性。在一階謂詞邏輯中把所有推理規則作為一個單一規則來統一處理請參見一階歸結。
注意有很多不同的形式邏輯系統，每個都帶有合式公式、推理規則和語義的自己的集合。參見時間邏輯、 模態邏輯或直覺邏輯的實例。量子邏輯也是一種不同尋常形式的邏輯。參見證明論。在謂詞演算中，需要一個補充的推理規則。它叫做普遍化。
在形式邏輯的設置(和很多有關領域)中，推理規則通常用如下形式給出:
前提#1
前提#2
...
前提#n
結論
這個表達式聲稱，在某個邏輯推導期間已經獲得了給定前提，同樣可以認可特定結論。用來描述前提和結論二者的的精確的形式語言依賴於推導的實際上下文。在一個簡單的情況下，你可以使用邏輯公式，比如
A→B
A
B
它是命題邏輯的肯定前件規則。推理規則通常通過使用全稱變數而公式化為規則模式。在上面的規則(模式)中，A 和 B 可以被實例化為論域(有時約定為某種受限制的子集比如命題) 的任何元素，來形成推理規則的無限集合。
證明系統形成自一組規則，它們可以被連結在一起形成證明或推導。任何推導都只有一個最終結論，它是要證明或推導的陳述。如果在推導中留下了未滿足的前提，則推導就是假言陳述: "如果前提成立，那麼結論成立"。
[编辑] 可接納性和可推導性
在規則的集合中，一個推理規則可能是多餘的，在它是「可接納的」或「可推導的」的意義上。一個可推導規則是可以使用其他規則從它的前提推導出它的結論的規則。可接納規則是只要前提成立結論就成立的規則。所有可推導規則都是可接納規則。要鑒別它們的區別，考慮定義自然數的下列規則集合(判斷 n\,\,\mathsf{nat} 斷言 n 是自然數的事實):
\begin{matrix} \frac{}{\mathbf{0} \,\,\mathsf{nat}} & \frac{n \,\,\mathsf{nat}}{\mathbf{s(}n\mathbf{)} \,\,\mathsf{nat}} \\ \end{matrix}
第一個規則聲稱 0 是自然數，第二個聲稱 s(n) 是自然數，如果 n 是自然數。在這個證明系統中，下列規則示範了自然數的第二個後繼者也是自然數，是可推導的:
\frac{n \,\,\mathsf{nat}}{\mathbf{s(s(}n\mathbf{))} \,\,\mathsf{nat}}
它的推導只是上述後繼規則的兩次使用的複合。下列規則斷言任何非零自然數有前驅者存在，只是可接納的:
\frac{\mathbf{s(}n\mathbf{)} \,\,\mathsf{nat}}{n \,\,\mathsf{nat}}
這是自然數的事實，並可以通過數學歸納法證明。(要證明這個規則是可接納的，你可以假定這個前提的一個推導，並在其上歸納出生成 n \,\,\mathsf{nat} 的推導)。但是，它不是可推導的，因為它依賴於前提的推導的結構。為此「可推導性」在增加到證明系統下是穩定的，而「可接納性」不是。要看出區別，假設下列無意義規則被增加到證明系統:
\frac{}{\mathbf{s(-3)} \,\,\mathsf{nat}}
在這個新系統中，雙後繼規則仍是可推導的。但是，找到前驅者的規則不再是可接納的，因為沒有方式來得到 \mathbf{-3} \,\,\mathsf{nat}。可接受性的脆弱來自它被證明的方式: 因為這個證明可以歸納於前提的推導的結構上，對系統的擴展向這個證明增加了新情況，而它可能不再成立。
可接納規則可以被認為是一個證明系統的定理。例如，在相繼式演算中切消成立，「切」規則是可接納的。
[编辑] 其他考慮
推理規則也可以用如下形式陳述: (1) 某些(可能為零)前提，(2)十字轉門(turnstile)符號 \vdash ，它意味著"推出"、"證明"或"得出"，(3) 一個結論。十字轉門符號化了執行能力。蘊涵符號 \rightarrow 沒有這種能力: 它只指示潛在的推理。 \rightarrow 是另一個邏輯運算符，它運算於真值之上。 \vdash 不是邏輯運算符。它是一個催化劑，代謝真陳述來建立新陳述。
推理規則必須區別於一個理論的公理，它是被假定為真而無須證明的斷言。依據語義，公理是有效的斷言。公理通常被當作應用推理規則和生成一組結論的起點。注意在推理規則和公理之間沒有明確的區別，在規則可以被人工編碼為公理或反之的意義上。例如，一個規則的前提的集合可以為空，所以結論總是為真。反過來說，一個公理通常假定是一個單一子句，但是實際上你可以指定生成一個公理的無限集合的模式，它淺薄的有著和推理規則有一樣的形式。
或者用更少的技術術語:
規則是關於系統的陳述，公理是系統內的陳述。例如:
* 規則從 \vdash p 推出 \vdash Provable(p) 是個陳述，聲稱如果你已經證明了 p 則 p 是可證明的(通常是合理的主張)。
* 公理 p \to Provable(p) 將意味著所有真的陳述都是可證明的(通常不是個合理的主張)。
在證明論中，推理規則在邏輯演算比如相繼式演算和自然演繹的規定中扮演了關鍵角色。 |
|
樓主: pdick
在線雷達
發表於 2012-7-11 14:30:43
發表於 2012-7-21 20:11:23
