関係代数 (数学)
RAの超数学は1987年のタルスキとGivantによる本の中で大きな分量を割いて議論されている。また Givant の論文においても簡潔に述べられている。
RA は全体として等式から成り、それらは一様な置き換えと代入だけで操作される。この二種類の操作規則は、学校教育でも扱われ、抽象代数でも扱われ、一般的に慣れ親しまれた操作である。よって RA の証明は一般の数理論理学における証明と異なり数学者が慣れ親しんでいる形で進められる。
RA は三つ未満の変数をもつ一階述語論理(FOL と記す)の論理式(もしくはそれと論理的に同値なもの)を記述することができる。与えられた変数は三回を越えない範囲で繰り返し量化子を用いて量化されうる。驚くべきことに、このような FOL の一部分だけでもペアノの公理を記述することができ、現在提唱されている中で殆ど全ての公理的集合論を記述することができる。よって、 RA は FOL とその結合子、量化子、ターンスタイルと三段論法を使わずに、数学全てを代数化する手段となる。RA はペアノの算術と集合論を記述するのでゲーデルの不完全性定理が適用され、RA は不完全であり完全化不能であり決定不能である(一方、RA におけるブール代数は完全で決定可能)。
RelMICS / Relational Methods in Computer Science maintained by Wolfram Kahl
Carsten Sinz: ARA / An Automatic Theorem Prover for Relation Algebras