Ｆａｓｃｉｎａｔｉｏｎ Ｎ−Ｄ−Ｆｉｌｅ　論理式

論理式（ろんりしき、英: Formula）とは、数理論理学における命題を表す形式的文法を有する式のこと。命題の真偽はその論理式の自由変項の値に依存する。

論理式の正確な定義は、対象とする形式論理に依存するが、典型的な例（一階述語論理）では以下のようになる。論理式は、特定の言語として定義され、その言語は個体定項、関数記号、述語記号などの集合であり、関数および述語記号はとりうるアリティー（引数）が決まっている。

ここで、項は以下のように帰納的に定義される。

1. 変項
2. 個体定項
3. f(t₁,...,t_n)、ここで、f はアリティー n の関数記号で、t₁,...,t_n も項である。

さらに、論理式は以下のように帰納的に定義される。

1. t₁=t₂、ここで、t₁ と t₂ は項
2. R(t₁,...,t_n)、ここで R はアリティー n の述語記号で、t₁,...,t_n は項
3. (¬φ)、ここで φ は論理式
4. (φ∧ψ)、ここで φ と ψ は論理式
5. (∃x)(φ)、ここで x は変項、φ は論理式

これらの定義のうち、最初の2つは原子論理式と呼ばれる。また、原子論理式およびその否定をリテラルと呼ぶ。