lambda演算中的量詞

Question

我在學習lambda演算，但是我對lambda演算中的量詞很困惑。據我所知，諸如「∃」之類的量詞是一階邏輯（FOL）的概念，lambda演算不需要這些概念。此外，我沒有發現任何關於我讀過的任何教程中的量詞。

但是，我發現this paper（Lambda Dependency-Based Compositional Semantics ），在第一頁中，作者在lambda演算中使用了量詞。那麼，在lambda演算中使用量詞嗎？如果是這樣，它們是什麼意思？和FOL一樣嗎？

Answer 1

您引用的論文使用量詞有點非正式，與使用謂詞相同。如果你已經有了一個lambda演算，你至少可以在紙面上用任何你想要的正式符號擴展它，包括FOL的量詞。在這種情況下，量詞被添加到微積分中，而不是其中的一部分。

但量化器可以在中定義 lambda微積分。在簡單的輸入設置中，您有基本的功能類型，但這些可以推廣到通用量詞和dependent function/Pi types。在這種情況下，lambda表達式表示含義和普遍量化的證明，這意味着它們是建立在可以給予lambda表達式的語義解釋上的。存在量詞可以被定義爲;

∃a：t。 P a：=∀Q。 （∀a：t。P a→Q）→Q

它與普通產品類型具有相同的數據。