論理式（ろんりしき、formula、well-formed formula、wff）とは、論理学において所定の形式文法から生成される形式言語の一部をなす文字列、すなわち、与えられたアルファベットに含まれる記号（シンボル）の列を意味する。整式、整論理式とも。形式言語はその論理式の集合全体と合致するとみなすことができる。論理式は統語論上の形式的オブジェクトであり、意味論は非形式的に与えることができる。論理式は主に命題論理や一階述語論理に代表される述語論理で使われている。その文脈において論理式は記号列 φ であり、φ の中の自由変数に値を設定したとき「φ は真か?」という問いが意味を持つ。形式論理において証明はある特性を持つ一連の論理式で表現され、その並びの最後の論理式は証明結果を意味する。「論理式」という用語は（紙や黒板などに）書かれた記号列を意味するが、より正確にはその記号列が表現しているものを指していると理解され、記号列は論理式の具体的トークンと理解すべきである。具体的トークンがなくとも論理式は存在しうる。したがって形式言語にはトークン実体の有無に関わらず無限個の論理式が存在する。さらに言えば、1つの論理式は複数のトークン実体を持ちうる。特に命題論理における論理式は命題と解釈されることが多い。しかし論理式は統語論的実体であり、形式言語における論理式は解釈とは無関係に存在する。論理式は、何かの名前、形容詞、副詞、接置詞、句、節、命令節、一連の節、一連の名前などに解釈される。ある形式言語の記号群を適当に並べれば、意味を持たない論理式となることもある。さらに言えば、論理式はどんな解釈をされる必要もない。命題論理の論理式はとも呼ばれ、例えば formula_1 といった形で表現される。命題論理式は、と論理演算を表す記号と括弧で定義され、命題変数を表すアルファベットは論理演算記号や括弧を含まないものとされる。論理式はそれらを並べたものである。論理式は次のように再帰的に定義される。この定義をバッカス・ナウア記法で形式文法として記述することもできる。変数の種類は有限とすると、次ようになる。この文法を使って次のような記号列が記述できる。これは、文法的に正しいので論理式である。一方、こちらは文法に従っていないので論理式ではない。複雑な論理式、特に括弧を多用した論理式は理解するのが難しい。この問題を緩和するため、数学における演算子の優先順位のように結合子間の優先順位を設けることもできる。例えば、優先される順に formula_3 、formula_6、formula_4、formula_5 とする。するとという論理式は次のようにも表現できる。ただし、これは論理式の記述を簡略化するための単なる取り決めである。したがって例えば、左結合性で優先順を formula_3、formula_4、formula_5、formula_6 と取り決めれば、上の括弧のない論理式は次のように解釈される。一階述語論理 formula_46 における論理式の定義は、その理論のに左右される。シグネチャとは、当該理論の非論理記号である定数記号、述語記号、関数記号を指定するもので、同時に関数記号や述語記号のアリティ（引数の数）の定義もシグネチャに含まれる。論理式の定義はいくつかの部分から構成される。まず、項 (term) が再帰的に定義される。項とは、議論領域の対象物を表現したものである。次に原子論理式が定義される。最後に論理式は、原子論理式の集合を含む最小の集合として次のように定義される。何らかの変数 formula_53 があるとき、formula_62 あるいは formula_63 が全く出現しない論理式は「量化子のない論理式」(quantifier-free formula) と呼ばれる。量化子のない論理式の前に存在量化がある論理式を「存在論理式」(existential formula) と呼ぶ。原子論理式とは、論理結合子や量化子を含まない論理式、あるいは厳密な部分論理式を持たない論理式である。原子論理式の厳密な形式は、どんな形式体系のものかで変わってくる。例えば命題論理での原子論理式はである。一階述語論理では、項である引数を伴った述語記号が原子論理式である。量化子を伴わず、論理結合子のみを使って原子論理式を結合した論理式を「開論理式」(open formula) と呼ぶこともある。「閉論理式」(closed formula) または「文」(sentence) とは、自由変数がない論理式を指す。一階述語論理の論理式に変数が出現する場合、閉論理式とするためにはそれぞれの変数に対応して束縛作用素（量化子など）を前置する必要がある。初期の数理論理学では、論理式 (formula) は単なる記号列、整論理式 (wff) はその中でも正しい構成規則に従って作られた記号列とされていた。何人かの学者は単に論理式 (formula) と呼んでいる。現代においては（特に計算機科学の文脈でモデル検査、自動定理証明などのソフトウェアを扱う場合）、（論理）式といえば代数学的な概念とされ、well-formedness すなわち（論理）式を表す具体的文字列表現の規定（結合子や量化子にどの記号を用いるか、どのような括弧の使い方にするか、ポーランド記法か中置記法かなど）は単なる記法の問題とされることが多い。それでも well-formed formula という記述は様々な著作に見られるが、任意の記号列という formula の古典的定義に対応する概念という使い方ではなく（むしろ fomula と wff は同義として使われている）、formula をそのような意味で使う数理論理学の用法は廃れた。

出典:wikipedia