はじめに
数学を学ぶと誰もが目にする「式」というもの。これは数字や記号を組み合わせて構成された表現ですが、その本質とは何でしょうか？単なる計算手順のメモでしょうか、それとも何らかの意味世界を指し示す記号列でしょうか。実は「式」は、数学と論理学の基盤をなす重要な概念であり、その捉え方には様々な側面があります。本稿では「式とは何か？」という根源的な問いに立ち返り、構造論的・記号論的・意味論的な視点から掘り下げてみます。まずは数学に登場する式の多様な種類を概観し、次に数式と論理式の異同、式の構文と意味、形式主義における記号操作としての式、代数構造と式、計算理論と式、さらにヒルベルトの形式主義からゲーデルの不完全性定理、現代の構成主義・型理論に至るまで、式というものの捉え方の変遷を論じます。
多様な「式」 – 数学における記号表現の種類
一口に「式」と言っても、その内容や役割は文脈により様々です。数学の世界では、以下のような多種多様な式が登場します。
- 数式（数値式）：数や変数、演算記号からなる計算式です。例えば
3x + 5やy^2 - 4といった表現は、具体的な値を表す数学的表現ですnumberanalytics.com。数式は値（number）を表し、複雑な計算もこのような基本構成から成り立ちます。数式には四則演算や累乗・対数・三角関数など様々な演算子が含まれ、構文規則（演算の優先順位など）に従って一義的に意味が定まるようになっています。 - 等式・不等式：等号（=）や不等号（<、>、≤、≥）を用いて2つの表現の関係を記述する式です。等式は「左辺と右辺の値が等しい」という関係を述べる命題であり、不等式は「左辺と右辺が等しくない」という比較関係を述べますnumberanalytics.comen.wikipedia.org。例えば
2x + 5 = 10は「2x+5と10が等しい」という主張であり、x^2 > 2は「xの二乗が2より大きい」という主張です。等式・不等式は真偽を持つ数学的命題であり、特定の変数値の下で成り立つかどうか（解の存在）を問う対象ともなります。 - 恒等式と方程式：等式の中でも、恒等式（identity）は全ての変数値について常に成り立つ等式を指します。一方で、特定の変数値でのみ成り立つ等式は一般に方程式（conditional equation）と呼ばれます。例えば
(x + y)^2 = x^2 + 2xy + y^2はどんな x, y に対しても成り立つ恒等的な式ですが、x^2 = 2はある特定の x（例えば √2 など）に対してのみ成り立つ方程式です。恒等式は代数的法則として扱われ、数学体系の中では公理または定理として位置付けられることもありますcuemath.com。 - 関数定義：関数や写像を定義する際にも式が使われます。例えば「f(x) = x^2 は x を入力として xの二乗を出力する関数を定義する式」です。このような関数定義の式では、左辺に関数記号と変数を置き、右辺にその計算規則を与えます。関数定義は等式の一種ですが、「任意の入力に対してこの関係が成り立つ」という点で恒等式に似ています（左辺を簡略化すれば必ず右辺と等しくなる）。関数定義は形式的には変数を含む等式であり、一種のルール記述と言えます。
- 論理式（論理的な式）：数学的論証や命題論理・述語論理で扱われる論理的な文を指します。これは通常、記号論理の体系で定められた論理記号や述語記号、変数を使って書かれる記号列で、命題（真偽の定まる主張）を表します。例えば、命題論理の式
P ∧ (¬Q)は命題変数 P, Q を使った論理式であり、一階述語論理の式∀x (P(x) → Q(f(x)))は量化記号 ∀（全称）、関数記号 f、述語 P,Q などを用いた述語論理式です。論理式はその構成規則（文法）によってよく形成された式（well-formed formula; WFF）であることが求められますproofwiki.org。形式的には、論理式もアルファベット（論理記号・述語記号など）からなる記号列であり、文法規則に沿って構成されたものです。 - 形式体系の式（ラムダ式など）：計算機科学や論理学では、特殊な形式体系の中の式も考えられます。例としてラムダ計算におけるラムダ式（λ式）があります。ラムダ計算は関数の適用と抽象化を扱う形式体系で、その基本要素である ラムダ項 (lambda term) も一種の「式」ですen.wikipedia.org。ラムダ項は変数、関数抽象（λ記号）、関数適用という3つの構成規則から再帰的に定義され、例えば
λx. (x + 1)やλx.λy. P(x,y)のような形をしています。プログラミング言語の式（式文）も広義にはここに含まれ、型付きラムダ計算の式などは「論理式」と「プログラム」の双方の性質を併せ持つ興味深い存在です。
以上のように、数学や論理学には様々な「式」が存在します。数式は値を表現し、等式・不等式は関係を主張し、論理式は命題の論理構造を示し、ラムダ式は計算手続きを表すなど、役割は多岐にわたります。しかし共通しているのは、いずれも記号によって構成された体系的な表現であり、一定の規則（構文）に従っていることですproofwiki.org。次節では、この構文の観点から、数式と論理式の違いや共通点を見てみましょう。
数式と論理式の違いと接点
数学の式（数式）と論理学の式（論理式）は、一見すると別物のようですが、本質的な部分で深く繋がっています。その違いと共通点を整理してみましょう。
1. 真偽値を持つかどうか：基本的に、数式（例えば 3x+5）はそれ自体では真偽のない値表現です。一方、等式や論理式（例えば 3x+5 = 10 や P ∧ Q）は命題を表し、真か偽かの値（真理値）を持ちますnumberanalytics.com。しかし、この区別は絶対的ではありません。数式であっても文脈により「方程式」として解釈されれば「真となる変数値は何か？」という命題的側面を帯びますし、論理式も解釈（後述）によって真偽が定まります。したがって、式が値を持つか真偽を持つかは、その式の種類と扱い方によって決まります。
2. 項と命題：論理学では、項 (term) と 原子式 (atomic formula) を区別します。項とは個体を指示する名前のようなもので、変数や定数、関数記号を組み合わせて作られ、対象となる「もの」を表しますmath.stackexchange.com。例えば論理における n や 0、あるいは n+0 などは「項」であり、それ自体は真偽を持ちませんmath.stackexchange.com。一方、原子式は述語記号（関係記号）に項を適用して得られる最小の命題ですmath.stackexchange.com。例として「Even(n)」（n が偶数である）や「0 = 0」や「n + 0 = n」は原子式で、いずれもそれ自体で真偽が定まる論理式ですmath.stackexchange.com。項は数式に相当し、原子式は等式などの簡単な命題に相当すると考えれば、数学の式との対応関係が見えてきます。例えば数式 n+0 は論理学では項であり、それを使った等式 n+0 = n は原子論理式となりますmath.stackexchange.com。
3. 複合式の構成：論理式は、原子式から論理結合子や量化記号を用いて複合的に組み立てられます。例えば「¬(P ∨ Q)」や「∀x (P(x) → ∃y Q(y))」のように、否定・論理積・論理和・含意・全称量化・存在量化などの構成ルールによって複合命題が作られます。一階述語論理では、これらの構成規則を厳密に定めて**「よく形成された論理式」を定義しますproofwiki.org。この点で、論理式は文法的に厳格な形式言語の産物です。一方、通常の数学の記法では厳密な文法規則が暗黙の了解として存在するものの、論理ほど形式的に規定されてはいない場合もあります。しかし原理的には、例えば方程式 x^2 = 2 も「= を述語、x^2` を項とみなせば原子述語論理式**」と見做すことができ、論理学の枠組みに乗せることができます。実際、数論や群論などを述語論理で形式化する際には、等号や大小比較、演算記号を述語・関数記号として取り入れ、数学の命題を全て論理式として表現します。このように数式と論理式は相互に行き来可能であり、数学的命題は論理式で表現しうるし、論理式の内容を特定の数学的構造上の命題として読むこともできます。
4. 解釈と意味：数学の式はしばしば暗黙のうちにある解釈の下で扱われます。例えば x^2 = 2 という方程式は通常「実数において x の二乗が2に等しい」という意味で使われ、真となる x は存在する（具体的には ±√2）と理解されます。しかし論理学の形式言語では、式自体に固定の意味は無く、どのような構造の上で解釈するかによって真偽が変わります。論理式 ∀x (P(x) → Q(f(x))) も、どのようなドメイン・どのような P,Q,f の解釈を与えるかで内容が決まります。したがって論理式は「解釈待ち」の記号列という側面が強いです。一方で通常の数学では「自然数の世界」「実数の世界」など前提となるモデルが共有されているため、式の意味（セマンティクス）があらかじめ固定されている場合が多いといえます。この点で、論理式は文脈から独立した一般的な形を保ち、数式は特定の文脈で意味づけられているとも言えるでしょう。しかしこれは程度問題で、数学基礎論においては数学のあらゆる式を一旦文脈から切り離して形式化し（例えば集合論の言葉で全てを書き表し）、論理式として考察することも行われます。
以上のように、数式と論理式には違い（値 vs 命題、項 vs 原子式、文脈依存性など）がありますが、根底では「記号で書かれた形式的な表現である」という共通点があります。また数学の命題は論理式で厳密に記述でき、その真理は論理式の真理として議論できます。この橋渡しは数理論理学という分野で確立されており、命題論理・述語論理を駆使して数学を形式的に扱うアプローチが発展してきました。次章では、そのような形式言語としての式の構文と意味に焦点を当て、式の持つ二面性（構文論と意味論）を見てみます。
式の構文と意味 – シンタックスとセマンティクス
形式体系における「式」は、常に構文（syntax）と意味（semantics）の二つの側面を持ちます。構文は記号列としての構造に関する規則であり、意味はその式が何を表しているかに関する解釈です。この節では、論理式を中心に、式の構文と意味の関係を考えてみます。
● 構文論: 式は規則に従った記号列 – 論理学では、まず「どのような記号列が式として正しく構成されているか」を厳密に定義します。例えば一階述語論理では、論理記号（¬, ∧, ∨, →, ∀, ∃ など）、述語記号、関数記号、変数記号などから成るアルファベットを決め、以下のような構文規則でWFF (well-formed formula) を定義しますproofwiki.org:
- 任意の述語記号 P と項 t₁, t₂, …, tₙ の組 P(t₁,…,tₙ) は原子的な論理式である（原子式）。
- φ が論理式なら ¬φ も論理式である（否定の導入）。
- φ, ψ が論理式なら (φ ∧ ψ), (φ ∨ ψ), (φ → ψ) も論理式である（論理結合子の導入）。
- φ が論理式で x が変数なら、∀x φ と ∃x φ も論理式である（量化の導入）。
これらのルールを用いることで、「括弧の入れ方」「演算子の配置の仕方」を明確に決め、字句列が論理式か否かを機械的に判定できるようにします。形式言語において、式は文字列（シンタックス）のパターンとして捉えられており、このような構文的側面だけを考えるときには式は意味を持たない単なる記号列です。ヒルベルトら形式主義者は、この構文的側面を重視し「数学を記号操作の体系」として扱おうとしました（後述）postcomplete.medium.compostcomplete.medium.com。
● 意味論: 式に意味を与える解釈 – 一方で、通常我々は式に意味を感じ取ります。それは人間が式をある対象の記述とみなしているからです。論理式の意味論はアルフレッド・タルスキらによって確立されました。基本的な考え方は、式に対して「モデル（解釈）」を与えることですplato.stanford.edu。モデルとは「変数は何を動くか」「述語・関数記号は何を意味するか」を具体的に定めた数学的構造のことですplato.stanford.edu。例えば述語論理の式 ∀x (P(x) → Q(x)) を考えるとき、ある構造 I においてこの式が真であるとは、「構造 I における任意の要素について、もしその要素が P の性質を持てば必ず Q の性質も持つ」ということを意味しますplato.stanford.edu。一般に、論理式 S と構造 I に対して、I ⊨ S （構造 I が式 S を充足する）と記号的に表し、「S を I に解釈したとき真である」という意味になりますplato.stanford.edu。このとき S は I の下で意味（真偽値）を持ったと言えます。また「ある構造 I が S を充足する」ことを「S は I で真である」とも言い換えますplato.stanford.edu。このようにしてモデル理論的意味（model-theoretic semantics）が定義されます。
論理式が普遍的に真（恒真式、論理的妥当）であるとは、どんな解釈を与えても真になることを指し、逆に充足不能とはどんな解釈でも偽になることを指します。またある特定の構造 M において真である式の集合をその構造の理論と呼びます。重要な点は、形式言語の式は解釈を指定しなければ意味（真偽）は未定であり、解釈を与えて初めて真か偽かが評価できるということです。「意味論的に有効な推論」とは「全てのモデルで前提が真なら結論も真」となるような論理式の関係性を言いますplato.stanford.edu。
● 構文と意味の架橋: 完全性定理 – 構文的側面（証明論）と意味的側面（モデル論）は一見独立に見えますが、両者を結び付ける重要な結果があります。ゲーデルの完全性定理（1930年）です。これは「一階述語論理において、論理的妥当な（全てのモデルで真となる）式は、形式証明によって証明可能であり、逆も成り立つ」というものですen.wikipedia.orgen.wikipedia.org。言い換えれば、モデル理論上の真理と証明論上の証明可能性が一致するということです。例えば全ての構造で成り立つ論理式 φ があれば、公理系から論理的に φ を導けるしen.wikipedia.org、導けなければ何か反例となるモデルが存在することになります。これは**「もしある理論 T のあらゆるモデルで式 φ が真ならば、T から φ を証明できる」**という形で表現されますen.wikipedia.org。この定理により、形式体系の完全性が保証され、論理におけるシンタックス（証明体系）とセマンティクス（モデルによる真理条件）は幸いにも矛盾なく対応していると分かりましたen.wikipedia.org。完全性定理は特に一階論理で成り立つ重要定理であり、論理が我々の直感的な「真理の追求」を忠実に形式化できていることの保証でもありますen.wikipedia.org。
一方で、ゲーデルは後述の不完全性定理によって、より強い算術系では「真だが証明できない命題」が存在することを示しました。これは構文と意味のズレの存在を示唆する結果です。ただそれは形式体系（公理系）内部の問題であり、一階論理そのものの枠組みは完全である点に注意が必要です。
● サウンドネス（健全性）と決定不能性 – 完全性定理に対し、より自明ながら重要なのが健全性定理です。「証明可能ならば全てのモデルで真」、すなわち形式証明で導けるものは論理的に妥当であることを指します。これは我々が構築した論理体系が間違った推論を許さないという健全さの保証です（こちらは証明の各ルールが明らかに真理保存的であることから容易に示せます）。
さらに、構文と意味の関係においては決定可能性の問題も無視できません。19世紀末から Hilbert が問いかけた**“Entscheidungsproblem”（決定問題）、すなわち「ある論理式が恒真かどうか（ある理論の下で証明可能かどうか）を機械的に判定するアルゴリズムは存在するか？」という問いは、Church と Turing によって1936年に否定的な回答が与えられましたen.wikipedia.orgen.wikipedia.org。彼らは「一階述語論理の論理的妥当性一般を判定する計算手続き（アルゴリズム）は存在しない」ことを証明したのです。つまり論理式の真理一般を自動判定することは不可能であることが示されました。この結果は計算機科学と論理学の両方に衝撃を与え、チューリングマシンによる計算可能性**の理論へと繋がっていきます。
以上のように、式には「構文（形式）」「意味（内容）」という双面性があり、論理学ではその両者が精緻に理論化されています。式を記号列として扱う視点からすれば、その操作規則や証明可能性が重視され、一方意味を持つ記号と見る視点では、その真理値やモデル上での解釈が問題になります。次の節では、特に形式主義の立場から「式を記号操作として見る」ことに焦点を当て、そこに絡む哲学的問題を考えます。
形式主義と記号操作としての式
19～20世紀初頭、数学基礎論において形式主義(formalism)という立場が台頭しました。形式主義者にとって、数学とは意味を問わない純粋な記号操作の体系であり、数学の真偽はその体系内での証明可能性に還元されますpostcomplete.medium.compostcomplete.medium.com。形式主義を端的に説明すると「数学とはある公理（初期の式）と推論規則に基づいて行われる記号ゲームに過ぎない」というものですpostcomplete.medium.com。有名な数学者ダフィット・ヒルベルトは「数学の各命題は無内容な数符号の構成である」と述べ、数学を無意味な記号操作として形式体系に翻訳し、その無矛盾性だけを問題にすべきだと考えました。この立場では、式は何かを意味している必要はなく、ゲームの駒のように扱われます。数学者が定理を「発見」するというより、定理は公理と規則から演繹される記号列に過ぎないという見方ですpostcomplete.medium.com。
しかし、ヒルベルト自身は「数学を無意味な記号遊戯に貶める」つもりはなかったことに注意が必要です。彼の形式主義的プログラムの目的は、数学全体の無矛盾性を示すことであり、そのために数学を形式体系に置き換えただけでした。実際ヒルベルトは、「我が証明理論の理念は、数学を意味のない記号ゲームに変えることではなく、それを理論的な科学に高めることだ」と述べていますplato.stanford.edu。つまり、形式主義とは数学を記号体系として再構成する方法論であり、数学そのものの意味や有用性を否定するものではないのです。ヒルベルトは形式化によって数学の確実性を担保しようとしましたが、その背景には「数学的命題も、本来は何か意味を持っている」という暗黙の理解がありましたplato.stanford.edu。ただしその意味を直接取り扱うことは難しいため、一旦形式へと抽象化したのです。
それでも形式主義への典型的批判として、「数学を記号の空しい遊びと見なして良いのか？」という点があります。人間の数学的直観では、式には意味や内容が伴っています。例えば E = mc^2 という式は単なる文字の羅列ではなく、物理的世界に関する深い意味を含んでいます。形式主義はそのような直観的意味を数学から切り離し、「意味は数学には不要」という立場を取ります。極論すれば、意味は数学の外側（メタレベル）で考えればよく、数学内部では「証明できるか否か」だけが問題だとする姿勢です。この立場に対し、フレーゲやブラウアーといった他の哲学者・数学者は反論し、意味論を無視した数学に不満を唱えました。
興味深いのは、現代の計算機科学ではこの形式主義的見方が実際的に重要な役割を果たしていることです。例えば自動定理証明やソフトウェア検証では、コンピュータが論理式を単なるシンボル列として処理し、機械的に変形・検証します。コンピュータにとって「式の意味」はなく、すべては0と1の列（バイナリ符号）として内部で扱われます。それでも私たちは「コンピュータが定理を証明した」「プログラムが論理的に正しいことを検証した」と言います。ここには二重の見方が潜んでいます。すなわち、機械的プロセスとしては形式主義そのものなのに、人間はそれに意味を読み取っているのです。
ヒルベルトの形式主義は一見すると極端ですが、このように**「式を意味のない記号列と見る視点」と「式を意味を伝えるものと見る視点」はしばしば交錯しますpostcomplete.medium.com。実際、多くの数学者は定理を発見・証明するとき、その式の背後にある直観的意味を頼りにしますが、同時に証明は記号の厳密な操作手順で構成されます。記号操作の客観性と意味理解の主観性という、数学の二側面がここに現れています。20世紀前半の記号論理主義 vs. 意味論的直観主義の論争（ヒルベルトとブラウアーの対立など）は、この問題を巡るものでしたが、現在では双方の視点を適切に使い分ける**ことが一般的です。記号としての式を厳密に扱うことで論理的齟齬を防ぎつつ、その式が何を意味するかを解釈して応用する、というアプローチです。
要するに、形式主義によれば式はゲームの駒（シンボル）であり、その操作規則が数学ですpostcomplete.medium.com。しかし多くの数学者にとって、式は「物事を表現する言語」でもあります。次節では、特に代数的体系における式について見てみましょう。群や環などでの恒等式や方程式の位置づけを通して、式の持つ構造的役割を考察します。
代数的構造と式 – 恒等式と方程式
数学の大きな領域である代数では、「式」は日常茶飯事的に使われます。多項式の式、方程式、恒等式、演算規則など、代数的構造（群・環・体など）を議論するとき、式はその構造の性質を表現する手段となります。ここでは代数体系における式の役割を見ていきます。
● 代数系の公理 = 恒等的な式：群や環などの代数的構造は、集合と演算の組で定義され、その公理はしばしば恒等式の形をとりますen.wikipedia.org。例えば群は、「演算 ・ に関して単位元が存在し逆元が存在し結合的である」という公理から定義されますが、これらは記号的には次のような式で表現できます。
- 結合法則: ∀x∀y∀z ((x・y)・z = x・(y・z))
- 単位元の存在: ∃e ∀x (e・x = x ∧ x・e = x)
- 逆元の存在: ∀x ∃y (x・y = e ∧ y・x = e)
このように、「～であること」を要請する公理は全称・存在を用いた論理式（恒真な形の等式を含む）で表されます。特に結合法則は全ての元で (x・y)・z と x・(y・z) が等しいという恒等式の形になっています。またアーベル群（可換群）の定義には 交換法則 ∀x∀y (x・y = y・x) という恒等式が追加されますmath.stackexchange.com。この式は**「任意の x,y について x・y と y・x は等しい」という一般化された等式であり、まさに性質（可換性）の表明です。ここで重要なのは、代数の公理はその体系内で常に成立する式（恒等式）の集まりだということですcuemath.com。ゆえに代数構造を論じるとき、我々は常に「ある式がすべての元で成り立つか？」**を考えていることになります。
● 恒等式 vs 方程式：上述の通り、恒等式は変数の値に依らず常に真となる等式ですcuemath.com。対照的に、方程式は特定の変数値では真、他では偽となり得る等式です。例えば環の世界で x^2 = 1 という方程式を考えると、一般にはすべての x で成り立つわけではなく、構造や x によっては成り立ったり成り立たなかったりします。たとえば実数体では x^2 = 1 の解は x = ±1 だけですが、複素数体では x = ±1 の他にありません（同じですが）、Z_2（2を法とする有限体）では実は x = 1 だけが解になるなど、構造によって解集合が異なることになります。このように方程式は「ある式が成り立つ元は存在するか？」という問い（充足可能性問題）に繋がり、恒等式（論理的妥当性）とは対称的な概念です。
代数構造では、恒等式はその構造が満たすべき法則であり、方程式は構造内で解を求める問題となります。例えば「2次方程式の解の公式」は与えられた2次多項式方程式の解（根）を求める手順であり、これは充足可能性を解く問題と言えます。一方、「因数分解公式」や「三角関数の恒等式」はその構造内で常に真の関係式であり、恒等的に成立する式変形を示しています。代数的手法では、未知数を含む方程式を既知の恒等式などを駆使して解くことになります。この意味で、恒等式は変形のルール、方程式は問題であり、両者は式を通じて緊密に関係しています。
● 代数的等式の意味論：前節で述べた論理式の意味論と同様に、代数における式もモデルによって意味づけられます。例えば x^2 = 2 は実数体をモデルとすれば偽ですが、拡大実数体系（√2を添加した体）をモデルとすれば真になる、といった具合です。モデル理論では、ある代数系が別の代数系の部分構造である時、ある式が一方で成り立てば他方でも成り立つか、といった議論（初等的部分構造や同値性）が行われますen.wikipedia.org。特に一階の等式理論では、恒等式（方程式恒真）の集合で理論が特徴付けられます。例えば「可換群の理論」は交換法則を含む群の公理全てからなる恒等式の集合です。モデル理論の言葉では、その恒等式集合を満たすすべての構造のクラスが可換群のクラスに他なりません。こうした視点から、代数的対象 = ある論理式（恒等式）のクラスという理解もできます。実際、普遍代数学（一般代数）では「等式で公理づけられる理論」を代数的理論と呼び、サブ構造や射なども論理式で特徴付けます。
● 例: アーベル群 – 具体例としてアーベル群（可換群）を考えます。アーベル群の定義は「群 G が任意の元 a, b について ab = ba を満たす」ことですmath.stackexchange.com。この「ab = ba」という式は G 内の全ての a, b に対して成り立つ恒等式であり、可換性という性質そのものを表現しています。したがって「G がアーベル群である」という命題自体を論理式で書けば: ∀a ∀b (a⋅b=b⋅a)\forall a\,\forall b\ (a \cdot b = b \cdot a)∀a∀b (a⋅b=b⋅a)
となります。実際、この式が真になるような構造 G は可換群のモデルであり（公理を全て満たす）、偽になる構造は非可換群です。ここで見るように、式（等式）の普遍的な真偽がそのまま代数的構造の性質を決定しています。このように代数の文脈では、式は構造の法則（公理）を記述したり、構造内の問題（方程式の可解性）を提示したりする役割を果たしています。
計算可能性と式 – チューリングマシンとラムダ計算の視点
上図: マイク・デイビーによるチューリングマシンの物理モデル（有限の紙テープで両方向に計算可能な装置）。これは数学的な「計算モデル」を実際に再現したもので、シンボル（穴の開いた紙テープ）を機械的に読み書きして操作する。チューリングマシンは記号列の操作として計算を定義する理論モデルであり、任意のアルゴリズムをシンボル操作の規則として実現できることを示したen.wikipedia.org。
20世紀前半、コンピュータ科学の黎明とともに「計算とは何か」という問いが形式的に扱われるようになりました。アラン・チューリングやアロンゾ・チャーチは、それぞれチューリングマシンとラムダ計算という形式体系を導入し、計算の本質を記号操作として定式化しました。
● チューリングマシンと計算：チューリングマシンは「無限長の紙テープ上の記号を、有限個の状態を持つ装置が読み書きしながら動き回る」という抽象機械ですen.wikipedia.org。このモデルでは、紙テープ上の記号列こそが扱われる対象（= 式）であり、マシンはその記号を有限の規則表に従って機械的に操作しますen.wikipedia.org。たとえば「記号Aを見たら記号Bに書き換えて右に移動し状態3に遷移する」等のルールが与えられると、マシンはそれに従って延々と記号列を書き換えていきます。重要なのは、チューリングマシン上では記号は意味を持たないという点です。テープ上の 1011 というパターンは、単に「1と0の列」であって、それが数値11を表すとか、ある論理式を符号化したものだとかはマシンにとって無関係です。マシンは決められた形式規則に従って記号を処理（操作）するだけです。それでもなお、チューリングマシンは任意の計算可能な処理（アルゴリズム）をシミュレートできることが示されましたen.wikipedia.org。つまり、人間が意味を見出すような計算（例えば足し算や文章検索）であっても、それは全て記号列操作に還元でき、チューリングマシンという形式体系の中で実現できるということです。チューリングマシンの登場は、「意味の無い形式操作」が如何に強力な計算能力を持ちうるかを示し、計算理論の基礎を築きました。
● ラムダ計算と言語：一方、アロンゾ・チャーチが提唱したラムダ計算 (λ-calculus) は、関数の適用と抽象化だけで計算のあらゆる過程を表現できるという驚くべき形式体系ですen.wikipedia.org。ラムダ計算では、「式」はラムダ項と呼ばれ、変数・関数抽象（λx.）・関数適用（M N）というルールで作られますen.wikipedia.org。例えばラムダ計算の式 λn. n+1 は「入力 n に対し n+1 を返す関数」という意味を持ちますが、ラムダ計算内ではそのまま一つの記号列として操作の対象になります。計算（関数適用）はラムダ式同士の代入と簡約という形式的操作で実現されます。チャーチもまた、このラムダ計算模型で計算可能関数を定義し、任意のチューリング計算はラムダ計算でも表現できることを示しましたen.wikipedia.org。実際、チャーチとチューリングは互いのモデルが同等の計算能力を持つことを認め、チャーチ＝チューリングのテーゼ「計算可能なものはすべてチューリングマシン（または同等のモデル）で計算可能」という考え方を確立しました。
● 式としてのプログラム：このように、計算理論の観点からはプログラムも一種の式（記号列）です。プログラミング言語は構文規則に従ったコードという文字列を入力とし、それをマシンが解釈して実行します。高水準言語のソースコードから機械語に至るまで、すべて記号によって表現された式であり、その意味（プログラムの挙動）は構文解析と意味的解釈によって初めて得られます。ここでもやはり、人間にとってはコード片 x := x + 1 に「変数 x の値を1増やす」という明確な意味がありますが、機械にとっては := や + は所定の命令セットに従った符号に過ぎません。つまり、計算機にとってプログラムは純粋に形式的な式であり、それを実行するとは記号列を規則通り変換していくことです。現代のコンパイラやインタプリタ理論でも、まず字句解析・構文解析によってプログラム（文字列）を構文木という形式構造に組み立て、その後意味的な処理（最終的な機械語への翻訳）を行います。この手順は論理式の場合と概念的に似ています。すなわち形式 → 意味への段階が存在し、形式の段階ではただの記号列として扱われ、意味の段階で「実際の計算」として解釈されるのです。
● 決定不能性と計算の限界：前述の決定問題の話に戻ると、計算理論ではチューリングマシンモデルを使って「ある問題がアルゴリズムで解けるか否か」を議論します。述語論理の完全性定理により「ある式が証明可能か」は「すべてのモデルで真か」に等しいと分かっていましたが、汎用のアルゴリズムではそれを判定できないことがチューリングらにより証明されましたen.wikipedia.org。これは**「真理」という意味論的概念が一般には計算不能であることを示しています。別の有名な結果として、チューリングは停止問題**（与えられたプログラムが有限時間で停止するかどうか）は決定不能であることも証明しました。これらはすべて記号列としての式に対する一般的な問いであり、答えが理論的に求められないことが示されたものです。計算可能性理論は、計算（= 記号操作）が持つ原理的な限界を突き止めた点で、式の世界にも限界があることを示唆しています。
計算の観点から見ると、式 = 情報を記述したコードとも言えるでしょう。チューリングマシンやラムダ計算の成果は、「式は機械的に扱える」ことと「式に機械的に扱えないものが潜む」ことの両方を教えてくれました。前者は現代のコンピュータの設計思想として活かされ、後者は暗号理論やAIにおける理論的限界の認識として重要です。
以上、計算可能性から式を捉えてみました。最後に、式の哲学的側面、すなわちヒルベルトの形式主義からゲーデルの不完全性定理、そして構成主義・型理論へという歴史の流れの中で、式の意味論や存在論がどう変遷したかを概観して締めくくります。
形式化の哲学 – ヒルベルトの夢、ゲーデルの挑戦、構成主義・型理論へ
「すべての数学を形式的に公理化し、無矛盾性を証明する」——これはダフィット・ヒルベルトが20世紀初頭に掲げた壮大な計画でした。ヒルベルトの形式主義的プログラムでは、あらゆる数学的命題は形式体系の式に翻訳され、その体系内での証明という形で数学の正しさを保証しようとしました。しかし、この夢は1931年に若き数学者クルト・ゲーデルによって打ち砕かれます。
● 不完全性定理: 式に内在する限界 – ゲーデルの第一不完全性定理は、「任意の（十分強力な）無矛盾な形式体系には、体系内で証明も反証もできない命題が存在する」ことを示しましたquantumzeitgeist.com。ここで言う「命題」は形式体系の中の式です。ゲーデルは各論理式を自然数に対応付け（ゲーデル数）、「自分は証明できない」という自己言及的な命題を巧妙に作り出しましたquantumzeitgeist.com。この命題は体系内では証明も否定もできませんが、体系が無矛盾である限り「真」だと解釈できてしまうのです。つまり「真理であるが証明不可能な式」が存在することになりますquantumzeitgeist.com。さらに第二不完全性定理では、「体系が自分自身の無矛盾性を証明することはできない」ことも示されましたquantumzeitgeist.com。これらの結果は、ヒルベルトの構想に決定的な打撃を与えました。すなわち、形式体系は自らの中のすべての真理をとらえることができない（完全にはなり得ない）ということですquantumzeitgeist.com。ヒルベルトが望んだ「数学の完全な形式化」は原理的に不可能だったわけですquantumzeitgeist.com。
ゲーデルの不完全性定理は、式の意味論について深い示唆を与えました。それまで形式主義者は「証明可能性が数学的真理と同義」と考えたかったわけですが、ゲーデルは「真理が証明可能性を超えうる」ことを暴露したのですquantumzeitgeist.com。つまり、形式体系の中で扱われる式には、体系が用意した意味（証明可能性）を逸脱してメタな意味（真理値）を持ち得るものがあるということです。この発見は数学基礎論だけでなく哲学や計算機科学にも波及し、**「数学的真理とは何か？」**という問いを新たに突きつけましたquantumzeitgeist.comquantumzeitgeist.com。
● 直観主義と構成主義: 意味への回帰 – ゲーデルの結果より前に、実はルイ・ブラウアーは直観主義(intuitionism)を唱えてヒルベルトと論争を繰り広げていました（1920年代）。直観主義は「数学的対象は心的な構成物であり、命題が真であるとはその構成が与えられることだ」という考えに基づきます。ブラウアーは特に排中律（命題は真か偽かのどちらか）が一般には受け入れられないと主張しました。彼の立場では、「命題が真である」とはその命題の構成的証明が存在することを意味しますen.wikipedia.org。証明がない限り命題は「真」とは見做せないし、「偽」であると断定もできない、という慎重な論理観です。この立場に立つと、式（命題）は単なる記号列ではなく**「証明という構成物が存在するか？」という問い**になります。
ブラウアーの主張を形式化したのがアレンド・ハイティングで、彼は直観主義論理（Heyting 論理）を公理化しましたen.wikipedia.org。直観主義論理では排中律 P ∨ ¬P が公理でないなど、古典論理とは異なる体系になります。直観主義論理の意味論は興味深く、BHK解釈（Brouwer–Heyting–Kolmogorov 解釈）によれば:
- 命題 A の証明が与えられたら「A は真」とみなす。
- 論理結合子や量化子は証明に対して定義される（例えば A ∧ B の証明は A の証明と B の証明の組、A ∨ B の証明は A の証明または B の証明のどちらか、など）。
- 特に ¬A とは「A の証明から矛盾が導ける」という構成であり、A の直接の偽を示すものではない。
この解釈では、証明そのものが命題の意味を与えます。直観主義の立場では式は単なる形式ではなく、それに対応する構成（証明 or 反証）が重要なのですen.wikipedia.org。事実、直観主義論理では**「真」=「証明がある」**と定義されるので、証明不可能な命題は真でも偽でもないという第三の状態があり得ますen.wikipedia.org。これは形式主義・古典主義とは全く異なる式の見方です。式は「証明という実体を持つか否か」で評価され、真偽二値の単純な意味論を拒否するわけです。
● Curry-Howard対応と型理論 – 直観主義の流れを汲みつつ、20世紀後半に登場したのが型理論(type theory)と呼ばれる形式体系です。その根幹にあるのがカリー＝ハワード対応という驚くべき原理で、これは「論理の証明」と「計算機プログラム」が同一視できるというものですen.wikipedia.org。簡単に言えば、論理の世界では命題があり証明がありますが、計算機科学の世界では型があり**プログラム（項）があります。そして「命題 ⇔ 型」「証明 ⇔ 項」という対応関係が成立しますen.wikipedia.org。これは別名「 propositions as types 」**と呼ばれ、直観主義論理と関数型プログラミング言語の構造が一対一に対応することを意味しますen.wikipedia.org。例えば直観主義論理の含意 P → Q は型理論では「型 P を入力とすると型 Q を出力する関数の型」を表し、この型の項（具体的な関数）が存在することが P→Q の証明に対応します。同様に、論理積 P ∧ Q は型の直積、論理和 P ∨ Q は型の直和、偽 ⊥ は空型（inhabited by no term）など、正確な対応があります。
この対応により、論理式はデータ型として、証明はプログラムとして理解できるようになります。言い換えれば、式が持つ意味（証明の存在）は、ある型に属する項（プログラム）の存在だということですen.wikipedia.org。型理論では論理と計算が統合され、式は「計算可能な構成物の型」としての意味を帯びます。ペル・マーティン＝レーフらの直観主義型理論（1970年代）はこの思想に基づくもので、そこでは命題はタイプ（集合のようなもの）と見なされ、証明はそのタイプの要素（集合の要素のようなもの）と見なされます。例えば「P は真」というのは「型 P に属する要素が存在する」ということであり、「P が証明できる」と同義です。この枠組みではゲーデル不完全性定理も少し異なった姿で現れ、例えば「この型に属する項は存在しない」といった命題が同様の困難を引き起こしますが、少なくとも命題の意味が証明（プログラム）の存在として明示されている点で、式に対する捉え方が構文論・意味論・計算論の全てを包含するものになっています。
● ホモトピー型理論と新基礎 – ごく最近の理論的展開としては、ホモトピー型理論 (HoTT: Homotopy Type Theory) の登場が挙げられます。これは型理論における「型（命題）は空間的対象であり、その証明は連続的変形（ホモトピー）として理解できる」という革新的な視点をもたらしましたen.wikipedia.org。2013年にはヴォエヴォドスキーらによる大著 “Homotopy Type Theory: Univalent Foundations of Mathematics”（通称 HoTT Book）が出版され、そこで新しい数学の基礎としてホモトピー型理論を位置づけていますhomotopytypetheory.org。HoTT ではunivalence公理と呼ばれる原理（同型な対象は同一視できる）が導入され、それにより集合論に代わる型理論ベースの基礎付けが提案されましたhomotopytypetheory.org。このプロジェクトは、論理式（型）の意味をホモトピー的な構造でとらえる点で、非常に高度に「意味論が豊かな形式体系」を作り出しています。例えば、∀x: A. P(x) という命題は型理論では「型 A の各要素 x に対し命題 P(x) の証明が構成できる」という意味ですが、HoTTではさらにその背景に位相空間や高次の構造が対応します。HoTT は現在も発展中であり、従来の集合論的基礎と並ぶ新たな基礎論アプローチとして注目されていますhomotopytypetheory.org。
以上、駆け足でしたがヒルベルトから現代までの流れを概観しました。この流れの中で**「式」の捉え方**も変容してきました：
- ヒルベルト: 式 = 無意味な記号列。ただし数学の全体系を記号列の操作で表し無矛盾性を示したい（形式主義）。
- ゲーデル: 式 = 自己言及もできる強力な表現。形式体系内の式の真理は体系から逸脱し得る（不完全性）。形式主義への反証。
- ブラウアー: 式 = 心的構成の記録。証明が無ければ真とも偽とも言えない（直観主義）。
- ハイティング: 式 = 証明という構成物が存在するかを問う命題。形式論理に組み込む（直観主義論理）。
- カリー＝ハワード: 式 = 型（プログラムの仕様）。証明 = プログラム。意味論と計算を同一視。
- 型理論: 式 = データ型。証明はそのデータの一つ（構成主義の完成形）。計算機上で扱える論理体系に。
- HoTT: 式 = ホモトピー的対象。論理と幾何を結合し、式の意味の多層化。
このように、「式」という概念一つを取っても、その哲学的意味と理論的位置付けは時代とともに大きく変わってきました。現代では、式は単なる記号列以上の意味を持ちつつ、しかし依然として形式的厳密さ（記号操作可能性）の担保された存在として扱われます。私たちは日常的に数式を書き、論理式を用いて証明を行いますが、その背景には上記のような深い理論が横たわっています。
おわりに
「式とは何か？」という問いに答えることは容易ではありません。本稿では、数学および論理学の枠内で「式」を様々な角度から論じてみました。式は記号列であり、構文規則に従って構成されますが、それ自体が世界の構造や計算の過程を映し出す意味を帯びる存在でもあります。数式・論理式・ラムダ式といった多様な表れを見せ、真理や計算や構造と結びつく式の姿は、数学の基盤そのものと言えるでしょう。
20世紀の数学基礎論は、形式的な式の世界を徹底的に追求し、その限界と可能性を明らかにしました。ヒルベルトは式の体系化に夢を託し、ゲーデルは式の語る真理の不可思議さを示し、直観主義者たちは式の意味を再考し、計算機科学者は式を走る機械を作り、現代の論理学者は式に新たな意味付け（型やホモトピー）を与えようとしています。式は記号に過ぎない——しかし記号であって記号に非ず、そこに数学的真理の一端が宿る。それが「式」というものの奥深さではないでしょうか。
最後に、読者の皆さんが何気なく書いている数式や論理式にも、こうした豊かな背景があることを感じていただければ幸いです。式という一見単純な存在を問い直すことは、数学とは何か、真理とは何か、計算とは何かという根源的問題に繋がっています。今後も新しい理論や哲学的考察が生まれ、式の捉え方が更新されていくことでしょう。数学と論理の発展とともに、「式」とは何かという問いもまた深化していくに違いありません。
参考文献:
- Alfred Tarski, “On the Concept of Truth in Formalized Languages”, 1933 (タルスキの真理定義論文。形式言語の意味論の基礎)plato.stanford.eduplato.stanford.edu
- Kurt Gödel, “Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme”, 1931 (ゲーデルの不完全性定理論文)quantumzeitgeist.comquantumzeitgeist.com
- David Hilbert, “Neubegründung der Mathematik”, 1922 など (ヒルベルトによる形式主義の説明)plato.stanford.edu
- Arend Heyting, “Die formalen Regeln der intuitionistischen Logik”, 1930 (直観主義論理の公理化)en.wikipedia.org
- H. Curry & R. Feys, “Combinatory Logic”, 1958 （カリー＝ハワード対応の源流となる論理と言語の研究）en.wikipedia.org
- Per Martin-Löf, “Intuitionistic Type Theory”, 1984 （構成的数学・型理論の基礎付け）
- Univalent Foundations Program, “Homotopy Type Theory: Univalent Foundations of Mathematics”, 2013 （ホモトピー型理論による新しい数学基礎）homotopytypetheory.org
その他、数理論理学や計算機科学の標準的教科書（Shoenfield 1967, Enderton 1972, Sipser 1996 など）や、スタンフォード哲学百科事典の関連項目（「Hilbert’s Program」plato.stanford.edu、「Gödel’s Completeness Theorem」en.wikipedia.orgen.wikipedia.org、「Intuitionistic Logic」en.wikipedia.orgen.wikipedia.org など）も併せて参照されたい。
