資産負債モデル

論理式（formula）は極性（ポラリティ polarity, 符号 sign）を持つとする、正負号（positive sign）と負符号（negative sign）。正負号は省略してもよい。（書き方は後で）

正（極性が正）の論理式の集まりを論理資産（logical asset(s)）、負の論理式の集まりを論理負債（logical obligation(s)）と呼ぶ。負債は、liabilities, debt デット, debit デビなどがあるが、ここでは責務という意味合いでobligationを使う。

論理資産（正の論理式）を作り出す行為・手続きを証明（proof）と呼び、論理責務（負の論理式）を返済する行為を解決（resolution レゾリューション）と呼ぶ。resolutionの訳語のひとつ「導出」は証明と似ているので使わない。

• 目的命題の証明 -- 目的額の貯金
• 責務命題の解決 -- 現状債務の返済

既に終わっている証明や解決を既決（settled, proved, resolved）、まだ手付かずの証明や解決を未決（pending, unproved, unresolved）と呼ぶ。

書き方

• 正の論理式は、+ A と書く。
• 負の論理式は、- A と書く。
• 正の論理式は、A でもよい。

正の論理式達（論理資産）から正の論理式達を得る行為を証明と呼び、次のように書く。

• +[A₁, ..., A_n |- B₁, ..., B_n]

先頭のプラスとブラケットは省略してもよい。

• [A₁, ..., A_n |- B₁, ..., B_n]
• A₁, ..., A_n |- B₁, ..., B_n

証明を、正のリーズニング、順方向リーズニング、フォワード・リーズニングとも呼ぶ。また、上記のような形式を、正のシーケント、順方向シーケント、フォワード・シーケントと呼ぶ。

負の論理式達（論理負債、論理責務）を減らす行為を解決と呼び、次のように書く。

• -[B₁, ..., B_n -| A₁, ..., A_n]

区切り記号が -| なので、先頭のプラスとブラケットは省略してもよい。

• [B₁, ..., B_n -| A₁, ..., A_n]
• B₁, ..., B_n -| A₁, ..., A_n

ただし、証明を逆向きに書いただけと区別するために、負符号を省略しないほうが望ましい。

推論、証明、リーズニング

推論にはいくつかの対称性がある。

1. 導入規則と除去規則の対称性： これは対称というよりは単に対で出現するというだけ。個々の規則はそれぞれの個性を持つが、全体で何個あるかを列挙するときは便利な“対称性”。論理記号（結合子と定数）がN個あれば、2N個の推論規則が生じる。
2. 矛盾双対性： T→A と ¬A→⊥ にある双対性。f:T→A という射があれば、双対として ¬A→¬T、つまり ¬A→⊥ という射がある。この矛盾双対性（contradiction duality/adjointness）は背理法の原理になっている。否定が自己反変関手になっている。
3. 証明・解決-双対性： 証明があるなら、その逆向きの解決がある、という双対性。圏Cの射と、反対圏C^opの射が1:1対応することが根拠となる。反対圏双対性である。

命題を対象、証明を射とする圏Cがあると、その反対圏の対象と射を表すために次の記法を使う。

• +A∈|C₊| ←→ -A∈|C_-|
• +f:+A→+B in C₊ ⇔ f:A→B in C
• -f:-B→-A in C_- ⇔ f:A→B in C

明らかに、C C₊, C^op C_-。この状況で：

• +f:+A→+B を、命題Aから命題Bへの証明と呼ぶ。
• 命題Aを証明の前提（premise）、命題Bを証明の結果（result(s)）と呼ぶ。
• -f:-B→-A を、命題Bから命題Aへの解決と呼ぶ。
• 命題Bを解決の課題（theme）、命題Aを解決の要求（requirement(s)）と呼ぶ。

証明の書き方：

target B // Bは証明の目標
proof
  :
  :
 results C // Cが証明の結果
end proof
now we got C toward B
(we owed C⇒B)

解決の書き方

obligation B // Bは責務、目標と同じ
resolve
  B
  :
  :
  requires A // Aは要求（必要事項）
  (AがTrueなら done)
end resolve
now we got B providing A
   (we got A⇒B)
   (we owed A)

推論図

論理結合子∨について例示する。

  + A
 ---------
  + A∨(B)


  + A∨B  +[A |- C, B |- C]
 ---------------------------
  + C

これは導入規則と除去規則。正負号を取れば、通常の自然演繹の推論規則そのもの。

シーケントを使って書くと：

  +[Γ |- A]
 ------------------
  +[Γ |- A∨(B)]


  +[Γ |- A∨B]  +[Δ, A |- C] +[Π, B |- C]
 ---------------------------------------------
  +[Γ, Δ, Π |- C]

直観論理シーケントに関する推論規則になる。

正負号を負符号に変えて、証明図やシーケントを逆向きにすると：

  - A∨B
 ----------
  - A

  - C
 ------------------------------
  - (A)∨(B) -[C -| A, C -| B]

これは、負の論理式（責務）に対して解決（リゾリューション、分解、返済）を行う。A∨Bが解決すべき責務のとき、Aに責務を減らすことができる。下側の推論図（逆推論図、原子解決図）は、責務Cを別な論理式責務と解決の責務に変換している。-[C -| A, C -| B]は、未決な解決が2つ残っている（解決責務の残余がある）ことを示す。

逆証明図を逆シーケント（余シーケント）に直すと：

   -[A∨B -| Γ]
  -----------------
   -[A -| Γ]


   -[C -| Γ, Δ, Π]
  -----------------------------------------------
   -[(A)∨(B) -| Γ] -[C -| A, Δ] -[C -| B, Π]

上側の解決責務があるとき、下側の解決責務に還元・帰着できることを示す。

用語法の案

正と順の世界	負と逆の世界
正命題＝論理資産	負命題＝論理責務
順証明	逆証明＝解決
推論規則	還元規則
Aから推論してAを獲得する	Aを還元してBに帰着する
証明の結果（終点）	解決の課題（始点）
証明の前提（始点）	解決の要求（終点）
証明の目標（終点の先）	？（始点より前）
シーケント	逆シーケント＝余シーケント
証明射＝オペラッド射	逆証明射＝余オペラッド射
オペラッド	余オペラッド

通常は、証明の目標＝証明の結果（結論）となる。