存在公式

在 谓词演算 中，存在公式是一种前束范式公式（即，一个公式写成量词和约束变量的字符串，后跟一个无量词部分），其中量化变量是存在量化的。

每个存在公式在逻辑上等价于某个全称公式的否定（反之亦然）。

当存在公式中没有自由变量（即，当所有变量都被约束时），它被称为存在语句。