存在公式

在 謂詞演算 中，存在公式是一種前束正規化公式（即，一個公式寫成量詞和約束變數的字串，後跟一個無量詞部分），其中量化變數是存在量化的。

每個存在公式在邏輯上等價於某個全稱公式的否定（反之亦然）。

當存在公式中沒有自由變數（即，當所有變數都被約束時），它被稱為存在語句。