目 次



第1章  THEAX言語の概要

1.1  名前の概念

1.2  一般関数形

1.3  一般の式

1.4  述語論理式

1.5  空白の扱い


第2章  テキストの構成

2.1  Text,End Text

2.2  公理(Axiom)

2.3  定理(Theorem,Lemma他)

2.4  量化ブロックの構造

2.5  合意ブロックの構造

2.6  Becauseブロック

2.7  定義ブロックと置換ブロック

2.8  置換ブロック

2.9  単純置換文

2.10 複合置換文

2.11 ユニーク置換文

2.12 選択置換文


第3章  推論規則

3.1  推論規則概観

3.2  LOGIC(命題論理の推論)

3.3  ALS(全称記号の限定)

3.4  EXIST(存在記号の付加)

3.5  ALIMとEXIM(量化記号とimpの交換)

3.6  ARRN(量化記号と括弧の整理)

3.7  FLW(量化変数の名前登録)

3.8  ORD(量化記号の順序交換)

3.9  DMOR(ド・モルガン)

3.10 CNST(定数式からの量化記号除去)

3.11 EQ(等式の導出)

3.12 SUBST(代入)

3.13 EQPT(等式の置き換え)

3.14 FUNF(定義式による置き換え)


第4章  数学体系の諸問題

4.1  矛盾の回避

4.2  RUSSELのパラドックス

4.3  パラドックスの回避

4.4  パラドックス再論

4.5  集合論の必要性

4.6  帰納関数公理