一階邏輯的通用和存在量詞

Question

我正在參加一個Scala編程課程。在一個點指導員說：

功能嗒嗒和bladdy是一階邏輯的全稱和存在 量詞。

有人能翻譯「一階邏輯的普遍性和存在量詞」成英文嗎？

Answer 1

這句話充滿了行話。你可以找到描述universal和邏輯量詞here。

1. A Universal Quantifier是一個邏輯聲明，適用於一個集合的所有元素。
2. Existential Quantifier是一個適用於集合中至少一個元素的邏輯語句。

您還可以查看here以獲取first-order邏輯的快速說明。該術語是指從higher-order邏輯分開first-order：

1. First-order邏輯語句是常使用的;他們對一組成員採取行動。
2. Higher-order邏輯語句作用於其他邏輯語句;把它們看作是元邏輯。

Answer 2

教科書Language Proof and Logic爲Odersky教授提到的普遍量詞和存在量詞提供了這些英語表達。

通用量詞＆forall;

是用來表達普遍的索賠，那些我們用 quantifed短語，如一切，每一件事情，萬物和任何用英文表達。

存在量詞∃

是用來表達生存的權利，那些我們用英文表達使用這樣的短語東西，至少有一點，一個和的。

這些術語的提及可能與使用高階函數的集合相關或導致操作。在Scala中，從邏輯到代碼的轉換對於集合上的forall和exists操作是很自然的。這些與上面給出的普遍和存在定義類似。一些簡單的例子是有幫助的，以顯示這一點：

scala> val l = 1 to 10 
l: scala.collection.immutable.Range.Inclusive = Range(1, 2, 3, 4, 5, 6, 7, 8, 9, 10) 

scala> l.forall(x => x > 0) 
res0: Boolean = true 

scala> l.forall(x => x > 1) 
res1: Boolean = false 

這兩個forall聲明只是要求做這個集合中的所有元素符合標準。

scala> l.exists(x => x < 1) 
res2: Boolean = false 

scala> l.exists(x => x < 2) 
res3: Boolean = true 

這兩個exists聲明只是要求做這個集合的任何元素符合標準。

Answer 3

爲了充分理解這個陳述，你可能需要研究一些邏輯。但這裏的基本要點如下：

「量詞」是如何給邏輯陳述中的變量賦予含義。如果我說「{關於x}」，那其實並沒有太多意義。你必須知道x是說是真是假。但是，如果我說「所有x {一些有關x}」量化變量x或「存在一個x這樣{一些有關x}」，那麼我做一個單獨的語句是真或假。

在我說的是「{一些關於x}」是真「爲所有x」情況下，任何x你可以挑選;這是普遍的量化。例如「對於所有x,x是偶數」是虛假陳述。

在「存在一個x這樣說：」情況下，我說有這樣的x一個可能的選擇使「{一些關於x}」是真實的（我不是說選擇的是什麼，只是有一個）。這是存在量化。作爲一個例子，「存在x這樣x是偶數」是一個真實的陳述。

他們是在對偶「爲所有x {一些有關x}」指的是同樣的事情，「這是不正確的，存在一個x這樣，這是不正確的{一些有關x}」，也「存在x，使得{關於x}」的意思與「對於所有x而言並不是真的，{關於x}有關」）。如果你仔細想想，希望這看起來很直觀。

如果您告訴我們函數blah和bladdy是什麼，我們可以解釋它們與通用量詞和存在量詞的對應方式，這可能會更有助於幫助您理解講師的觀點。