接続詞＝構造構成語句
自分が使っている言葉をとりあえず列挙する。
メタな言明
- …（命題）が言える。
行為の予告
- …を計算する。
- …を示す。
- …を示そう。
行為と結果
- …（行為する）と、
文と文のあいだの接続詞
- …（命題）(に)?より、
- …（命題）から、
- …（命題）なので、
- …（命題）(だ)?から、
仮定の導入
- …（命題）と仮定する。
- …とする。
文頭に付く接続詞
- したがって、
- よって、
- つまり、
- これらから、
- 以上により、
用途を決めてみる。
つまり
定義により、同値な命題に言い換える。
Def: P(x) :⇔ Q(x) が背景知識Γ内にあるとき、
P(x) つまり Q(x)
より、から、なので、だから
当該推論ステップの根拠を示すために使う。
「より」「から」は背景知識または証明済み命題を名前や番号などで参照する場合に使う。
A (ラベルX) より B
これは
A (Xの参照先命題)
-----------------------[推論ルール]
B推論ルールは明示されないが、容易に推測可能とする。
「なので」「だから」は、根拠となる命題をインラインで前置する。
A Cなので B
これは
A C
----------[推論ルール]
B「より／から」と「なので／だから」を併用してもよい。
「から」と「だから」の音が似ているので、「から」はやめて「より」がいいだろう。
A (ラベルX) より C なので B
これは
(Xの参照先命題)
-----------------[推論ルール 1]
A C
--------------[推論ルール 2]
B推論ルール 1 は、非常に簡単なものに限る。
〜すると
〜の部分にはオペレーショナルな推論ステップを行為として書く。オペレーショナルな推論ステップとは、「両辺にtを足して」とか「平方根を取れば」のように、等式・不等式の項にオペレーショナルをする（しても命題が保たれる）もの。
A 〜すると B
このときの根拠は、s = t ⇒ F(x) = F(t) のような命題。Fがオペレーション。
〜を計算する、よって
〜は項tで、tから出発する等式的推論（等式命題の推論）ブロックをはじめる。
tを計算する。
t
= t'
:
:
= s「よって」は等式的的推論ブロックを閉じて、ローカルな結論を提示する。
tを計算する。
t
= t'
:
:
= s
よって
t = s
仮定する、以上により
含意導入ブロックの開始と終了。このとき、全称導入ブロックも同時に使われることが多い。
Aを仮定する。 ： ： B 以上により A⇒B
全称を一緒に使うケースでは、
A(x)を仮定する。 ： ： B(x) 以上により ∀x.(A⇒B)
これは次のような入れ子と同じ
任意のxに対して、
A(x)を仮定する。
：
：
B(x)
以上により
A(x)⇒B(x)
以上により
∀x.(A⇒B)
文頭の接続詞
「つまり」は同値な命題への置き換えとして、
- したがって、
- よって、
- これらから、
- 以上により、
日本語の通常の解釈として、「したがって」と「よって」、「これらから」と「以上により」に差があるとは思えない。この4つの差を見出すのも困難。
使い分けるのは不自然だろう。いずれも、ブロックを閉じる作用を持つ。
