数学（mathematics）
数学（の内容）（content of mathematics）は様々な基盤言語（substrate language）の上で記述される。
通常は日本語や英語などの自然言語の上で記述されることが多い。
一方で、数学を計算機上で表現、記録、伝達しようという試みも行われている。この場合、数学は一種の計算機言語の上で記述される。このような言語は形式的な文法によって定義された人工言語である。
このような言語の1つとして、Mizar言語がある。Mizar言語は一階古典述語論理（体系）（classical first-order predicate logical system）とTarski-Grothendieck集合論（Tarski-Grothendieck set theory）を基盤として数学の記述のためだけに作られた独自の言語である。自然言語の上で数学が記述される場合とできる限り同様の用語および記法を採用しており、その記述が自然言語の上で記述される数学の記述と類似したものになるように工夫されている（が、実際のところ、かなり異質であると個人的には感じる）。
また、そのような言語の1つとして、Coq言語がある。Coq言語は数学の記述のために作られたものと言うよりは、依存型付け関数型言語を基盤として、定理証明を行うための便利な機能を追加したものと言った方がより実情に即しているだろう。数学の記述の他に、電子回路、通信手順（の実装）、様々な算法（の実装）などの正当性（所与の仕様に準拠していること）の証明のために利用されることも多い。
数学を記述するためには論理（体系）（logical system）が必要であり、数学を記述する際には基盤言語の中に埋め込まれている論理を利用する。たとえば、日本語や英語などの自然言語には論理が埋め込まれており、自然言語の上で数学を記述する場合はその論理を利用することになる。また、Mizar言語は先述のように一階古典述語論理を基盤としており、Mizar言語の上で数学を記述する場合は、基盤としている一階古典述語論理を利用することになる。更には、論理（体系）自体を数学的に構築することもでき、予め数学的に構築された論理の上で別の数学を記述することもできる（なお、この際に必ずしも論理そのものを数学的に構築する必要はなく、代わりに論理が埋め込まれている何らかの体系を構築しても良い。たとえば、最初に圏論を数学的に構築し、その圏論の上で別の数学を記述することもできる。このようなことが可能なのは圏論に論理が埋め込まれているからである）。
数学を記述するために必要なのは論理が埋め込まれている言語である。この条件を満たしてさえいれば、どのような言語の上で数学を記述しても構わない（それが他人に受け入れられるかは分からないが）。
以降では、基盤言語として対象物指向算譜言語（object-oriented programming language）（主にその1つであるC#）を採用して、数学を記述していきたい。対象物指向算譜言語には論理が埋め込まれており、数学を記述するに足る（と考えている）。
対象物指向数学（object-oriented mathematics: OOM）
あらゆる数学的物件（mathematical object）を対象物（object-oriented object）と考え、数学的対象物（mathematical object in terms of OOM）と言うことにする。
全ての数学的対象物はMathematical Object型であると考えることにする。すなわち、Mathematical Object型を全ての数学的対象物がそこから派生する抽象基底型とする。
対象物指向古典命題論理（体系）（object-oriented classical propositional logical system）
取り敢えず、最初に論理を構築していきたいと思う。論理にも様々なものがあるが、取り敢えず古典命題論理を構築しよう。
最初に必要なのは古典命題論理における式である（古典）命題論理式（classical propositional formula）である。命題論理式を表す抽象基底型を命題論理式としよう。
命題論理式は命題変数、恒偽命題、否定、連言、選言、含意および等意からなり、次のような内部構造を有する。それぞれを命題論理式から派生する具象派生型と考えれば良い。
定義＝高次公理 命題論理式
命題変数、恒偽命題、否定、連言、選言、含意および等意は命題論理式である。
σが文字列であり、ιが整数であるならば、Propositional Variable (σ, ι)は命題変数である。
Contradiction ()は恒偽命題である。
φが命題論理式であるならば、Negation (φ)は否定である。
φ, ψが命題論理式であるならば、Conjunction (φ, ψ)は連言である。
φ, ψが命題論理式であるならば、Disjunction (φ, ψ)は選言である。
φ, ψが命題論理式であるならば、Implication (φ, ψ)は含意である。
φ, ψが命題論理式であるならば、Equivalence (φ, ψ)は等意である。
型図式は次のようになる。
型図式
通常の数学での記法とほぼ同様になるように慣用表現を定めておこう。
慣用表現
Propositional Variable (σ, ι)のσはP, Q, R, Sのみであるとする。
Propositional Variable (σ, ι)をσιと表すことにする。
σ0をσと表すことにする。
Contradiction ()を⊥と表すことにする。
Negation (φ)を(￢φ)と表すことにする。
Conjunction (φ, ψ)を(φ∧ψ)と表すことにする。
Disjunction (φ, ψ)を(φ∨ψ)と表すことにする。
Implication (φ, ψ)を(φ→ψ)と表すことにする。
Equivalence (φ, ψ)を(φ←→ψ)と表すことにする。
命題論理式の慣用表現の最外括弧は省略するものとする。
￢, ∧, ∨, →, ←→の優先順位と結合性を次のように定め、この規則によって曖昧にならない限りにおいて、命題論理式の慣用表現に含まれる括弧を省略するものとする。
￢：優先順位高、右結合
∧：優先順位中、左結合
∨：優先順位中、左結合
→：優先順位低、右結合
←→：優先順位低、左結合
これで命題論理式を構築することができた。C#で実装しよう。
