数理論理学において、述語論理の文(または閉じた式)[ 1 ]は、自由変数を持たないブール値の整形式式である。文は、真偽を問う命題を表すものと見なすことができる。自由変数を持たないという制約は、文が具体的で固定された真理値を持つことを保証するために必要である。なぜなら、(一般的な)式の自由変数は複数の値をとることができるため、そのような式の真理値は変化する可能性があるからである。
論理接続詞や数量詞を含まない文は、原子式になぞらえて原子文と呼ばれます。文は、原子文に接続詞や数量詞を適用することによって構成されます。
文の集合を理論と呼び、個々の文を定理と呼ぶ。文の真偽を正しく評価するには、理論の解釈を参照する必要がある。一階述語論理の理論では、解釈は一般的に構造と呼ばれる。構造または解釈が与えられれば、文の真偽値は固定される。理論は、そのすべての文が真となるような解釈を提示できる場合に充足可能である。すべての文が真となるような理論の解釈を自動的に発見するアルゴリズムの研究は、理論による充足可能性問題として知られている。
式の解釈には、正の実数、実数、複素数などの議論領域を与える必要があります。一階述語論理における次の例
これは文です。この文は、すべての y に対して、次の条件を満たす x が存在することを意味します。 この文は、正の実数に対しては真であり、実数に対しては偽であり、複素数に対しては真である。
しかし、その式は
自由変数yが存在するため、これは文ではありません。実数の場合、(任意に) を代入すると、この式は真になります。しかし、偽の場合は
重要なのは、不変の真偽値ではなく、自由変数の存在である。例えば、複素数のように常に真となる式であっても、それは文とはみなされない。そのような式は、述語と呼ぶべきだろう。