Quantifikatoren in Lambda-Kalkül

Question

Ich lerne Lambda-Kalkül, aber ich bin ziemlich verwirrt über die Quantifikatoren in Lambda-Kalkül. Soweit ich weiß, sind Quantoren wie "∃" Konzepte der Logik erster Ordnung (FOL), die von der Lambda-Kalkül nicht benötigt werden. Außerdem habe ich in irgendwelchen Tutorials, die ich gelesen habe, nichts über Quantifier gefunden.

Allerdings finde ich this paper (Lambda Dependency-Based Compositional Semantics ), auf deren erste Seite der Autor Quantifizierer in Lambda-Kalkül verwendet. Also, werden Quantifier im Lambda-Kalkül verwendet? Wenn ja, was meinen sie? Ist es das gleiche wie in FOL?

Answer 1

Das von Ihnen zitierte Papier verwendet Quantifizierer etwas informell, genauso wie es Prädikate verwendet. Wenn Sie bereits einen Lambda-Kalkül haben, können Sie ihn, zumindest auf dem Papier, um jeden gewünschten Satz formeller Symbole erweitern, einschließlich Quantifikatoren aus FOL. In diesem Fall sind die Quantoren etwas, das dem Kalkül hinzugefügt wird, nicht Teil davon.

Quantifikatoren können in typisiert Lambda-Kalkül jedoch definiert werden. In einfach typisierten Einstellungen haben Sie grundlegende Funktionstypen, aber diese können auf universellen Quantifizierer und dependent function/Pi types verallgemeinert werden. In diesem Fall stellen die Lambda-Ausdrücke Beweise für Implikationen und universelle Quantifizierungen dar, was bedeutet, dass sie in semantischen Interpretationen aufgebaut sind, die Sie Lambda-Ausdrücken geben können. Existenzielle Quantoren können dann wie folgt definiert werden:

∃ a: t. Pa: = Q. (∀ a: t. P a → Q) → Q

Die gleichen Daten wie der normale Produkttyp.