人と人とのコミュニケーションを目的にするので、機械可読ではない。特に、新しい変数（fresh variable）が登場したら、適当な変域の自由変数（または全称束縛変数）と解釈する。 前提 次は前提（既に知っているもの）とする。':⇔' は '⇔' と同じだが、定義…