この章と次の章では自然演繹による古典論理・直観主義論理の 形式化を紹介する．参考書としては

1. 前原昭二「記号論理学入門」（日本評論社，1967）
2. 桔梗宏孝「応用論理」（共立出版，情報数学講座，1996）
3. 角田譲「数理論理学入門」（朝倉書店，1996)

1. 林晋「数理論理学」（コロナ社，1989）
2. 松本和夫「数理論理学」（共立出版，初版1970，復刊2001）

目次

1. 命題論理の形式化（NK,NJ）

2. 証明・演繹のさまざまな例

3. 排中律と直観主義論理

総目次に戻る

1. 命題論理の形式化（NK,NJ）

1.1 論理式・公理系・推論規則

論理式の構成要素

• 命題記号 p, q, r, ...
• 特殊な記号⊥
• 論理結合子∧, ∨, →, ¬（↔を含めることもできる）

NK・NJの公理系と推論規則は以下の通りである.

公理系

NKの場合：φ∨¬φ（排中律）（φは任意の論理式）

NJの場合：なし

推論規則

推論規則はNK・NJ共通で，以下に示すような論理結合子に関する 「導入規則」・「除去規則」と⊥に関する 例外的な規則からなる（φ，ψ，χは任意の論理式）．

φ    ψ （∧導入） φ∧ψ	φ∧ψ φ∧ψ    （∧除去） φ ψ
φ ψ    （∨導入） φ∨ψ φ∨ψ	φ∨ψ      [φ] ： χ      [ψ] ： χ （∨除去） χ
[φ] ： ψ （→導入） φ→ψ	φ    φ→ψ （→除去） ψ
[φ] ： ⊥ （¬導入） ¬φ	φ    ¬φ （¬除去） ⊥
⊥   （⊥） φ

∨除去・→導入・¬導入については少し注釈が必要だろう． [φ]，[ψ] というように括弧で囲まれたものは「仮定」 と呼ばれる．そこから推論規則を適用する直前までの…の部分は 仮定を「仮の前提」として扱う一連の推論である． これらの仮定は推論規則の適用に際して前提からはずれる． これを「仮定が落ちる」（英語で「discharge」） という．これは自然演繹独特の概念で，証明を列記したり証明図を 描いたりするときには表記上それなりの工夫が必要になる．

この「仮定」ならびに「仮定が落ちる」という概念は 数学で場合分けや背理法などによって証明を行う際の 推論をそのまま模倣したものである．たとえば場合分けは 「仮に…としてみよう．このとき…となる． 今度は…としてみよう．このとき…となる．」 というような形をとるが，この「仮に…としてみよう」 という仮定の部分が前述の「仮の前提」すわなち「仮定」 に相当する．この前提は定理の前提とは別のもので， 最後に結論を下すときには姿を消す．それが 「仮定が落ちる」ということに他ならない．

NKとNJの関係を表にしてまとめると次のようになる．

述語論理の場合も∀，∃に関する推論規則（これにも導入と除去の 二種類の規則がある）が加わること以外はまったく同様である． 述語論理の場合の形式的体系もそれぞれNK，NJと呼ばれる．

【注意】

1. ↔を含めて定式化するときには次の二つの推論規則を加える：

   [φ] ： ψ      [ψ] ： φ （↔導入） φ↔ψ

   φ    φ↔ψ （↔除去） ψ

   ψ    φ↔ψ （↔除去） ψ

2. 上のように論理式φを単独で書かないで，それが依存する 前提の集合Γと常に組にしてΓ|-φというようにあらわす （実はこれはシークェントの概念に近い）ことにすれば， 「仮定が落ちる」ということの意味はもう少しわかりやすくなる． たとえば→導入はこの記法に従えば

   Γ∪{φ}|-ψ Γ|-φ→ψ

   という推論規則になる．ヒルベルト流の形式化ではこれは実は 演繹定理なのだが，自然演繹ではそれを推論規則にしている わけである．ちなみに，→除去はMP（modus ponens）に他ならない．

1.2 推論規則の意味・妥当性

1. ∨除去は数学で用いられる「場合分け」の論法を 推論規則にしたものと解釈できる．その大前提は「φ∨ψ」 すなわち「φまたはψが成立する」である． これは公理（つまり排中律）であるか，演繹の前提であるか， あるいはそれらから導出されたものでなければならない． この大前提と「φを仮定すればχが導かれる」および 「ψを仮定すればχが導かれる」ということから 最終的にχを結論する，というのがこの推論規則である． 妥当性は直観的には明らかだろう．

2. すでに注意したように，→導入はヒルベルト流の 形式化における演繹定理を推論規則にしたものであり，また →除去はMPに他ならないから，いずれも妥当なものである． ヒルベルト流の形式化は推論規則として後者しか用意しないが， ゲンツェン流では両方とも推論規則に組み込んでいる． しかも，これらを→に関する「導入」と「除去」といういわば 対等の規則としてとらえて，他の論理結合子についても同様に 「導入」と「除去」の規則を設けているのである．ヒルベルト流の 形式化が公理系重視の形式化であるのに対して，ゲンツェン流は 推論規則を重視する形式化である，ということがよくわかる．

3. ¬の導入・除去規則および⊥の規則は自然演繹の推論規則 の中では最もわかりにくく，かつ注意を要する．推論規則の 妥当性だけを問題にするならば，⊥の真理値を F すなわち 「偽」と解釈するだけでよい．たとえば¬導入については， φから⊥が導出されることは意味論的には v[φ→F] = T すなわち v[φ] = F を意味するから，v[¬φ] = T となって， 妥当性がわかる（他の場合についても同様に考えてみよ）． 他方，これらの規則の意味を理解するには，⊥を「矛盾」 （あるいは「矛盾状態」）と解釈するのがよい．このとき 三つの推論規則は次のようなことを意味している：
   1. ¬導入は「φを仮定して矛盾が出たら，¬φである」 と読める．これは「背理法」に似ているが，実は異なる ものである．背理法は「¬φを仮定して矛盾が出たら，φである」 というものであり，推論規則として書けば

      [¬φ] ： ⊥ （背理法） φ

      となる．¬導入と背理法は厳密に区別する必要がある（また， その区別ができるのが形式的体系の利点でもある）．背理法は ¬導入と「二重否定除去」¬¬φ|-φを組み合わせたもの， すなわち

      [¬φ] ： ⊥
      	（¬導入）
      ¬¬φ
      	（二重否定の除去）
      φ

      という演繹と考えることができる（最初に前提として置いた ¬φは¬導入の際に仮定として落ちた）．ただし，ここでは 二重否定の除去を一つの推論規則として扱っているが， 自然演繹ではこれも一連の推論過程で実現する必要がある． この部分はあとで例を通じて説明する．以上のように， 二重否定の除去は（したがって背理法も）排中律に基づくもの である．言い換えれば，排中律を認めない直観主義論理では 背理法も認めないのである．

   2. ¬の除去はφと¬φが両立する事実上の矛盾状態から ⊥という本当の矛盾状態に移行することと読める．最後の⊥の 規則は矛盾状態から任意の状態ψにいわば「脱出」することを 意味しているが，通常は¬の除去の規則と組み合わせて

      φ∧¬φ
      	（¬除去）
      ⊥
      	（⊥）
      ψ

      という形で用いられることが多い．これは 「矛盾からは何でも出せる」ということを意味する恒真式 |= φ∧¬φ→ψ（あるいは意味論的演繹関係 φ∧¬φ|=ψ） に相当する．自然演繹による形式的証明の中でこれが最も 技巧的な部分である．実際にどのように用いられるかは あとで例を通じて示す．

4. ∨除去・→導入・¬導入では，まず仮定を置き，一連の 推論によってある論理式（∨除去におけるχ，→導入におけるψ， ¬導入における⊥）を導いたあとでその仮定を落とすわけだが， 特別な場合として

   φ∨ψ      [φ]      [ψ] ： φ φ

   φ∨ψ      [φ] ： ψ      [ψ] ψ

   というもの（すなわち χ = ψ あるいは χ = φ というように 仮定とその帰結が同じものである場合）なども許す必要がある． →導入でも同様である．実際，これを用いて，たとえば φ→φを

   [φ] φ→φ

   （→導入を用いた）

   というように証明することができる．一見するとこれは技巧的で 奇妙なことに見えるが，実はそれほど不自然でもない．実際， 「仮定」と呼んでいるものはもともとは前提として置いたもの であり，推論規則を適用するまでは他の前提とまったく区別が 付かない（区別のしようがない）からである．特に，前提として 置いたものがそのまま仮定として落ちることを禁止する理由はない． このような考え方に抵抗を感じるならば自明な推論規則

   φ   φ

   が間に挟まれていると考えてもよいだろう．

2. 証明・演繹のさまざまな例

2.1 非常に簡単な例

【例１】|-φ→φ （φは任意の論理式）

1: [φ]²（前提）

2: φ→φ（1→導入）

【例２】{φ,¬φ} |- ψ（φ，ψは任意の論理式）

1: φ（前提）

2: ¬φ（前提）

3: ⊥（1,2 ¬除去）

4: ψ（3 ⊥）

【例３】{φ→ψ, ψ→χ} |- φ→χ （φ，ψ，χは任意の論理式）

1: φ→ψ（前提）

2: ψ→χ（前提）

3: [φ]⁶（前提）

4: ψ（3,1 →除去）

5: χ（4,2 →除去）

6: φ→χ（3,5 →導入）

このように「仮定」というものを設けて推論を重ねて行くのは 数学の証明に似ている．数学の定理は一定の前提のもとで 「…ならば…」となることを主張する（記号化すればΓ|-φ→ψ という形になる）ものが多いが，その証明はφを仮定して推論を 進める（記号化すればΓ∪{φ}|-ψに相当する）という形をとるのが 普通である．自然演繹が「自然」と考えられるのは，このように 数学における証明の仕方をそのまま形式化した部分が多いからである．

【例４】φ|-¬¬φ（φは任意の論理式）

1: φ（前提）

2: [¬φ]⁴（前提）

3: ⊥（1,2 ¬除去）

4: ¬¬φ（2,3 ¬導入）

「ゴールから遡って考える」は「トップダウン」の思考法と 言ってもよいだろう．トップダウンの思考法では，目標の問題を より簡単な問題に還元・分解して行くことによって解決しよう とする．他方，手近なところから次第に目標の問題に近づいて 行くことをめざすのが「ボトムアップ」の思考法である． この二つの思考法にはもちろん一長一短があるし，問題の性質 によってどちらが適しているかも違ってくるが，一般に， ゴールが明確な問題にはトップダウンの思考法が有効である．

今の場合，ゴールは¬¬φである．ところで，推論規則を 一通り眺めてみれば，¬¬φを導出するのに直接使える 推論規則は¬導入である（他の推論規則を使う可能性も 否定できないが，自然演繹の場合は最も簡単な可能性から あたってみることでうまく行くことが多い）． ¬導入で¬¬φを出すには，¬φを仮定して⊥を導けばよい． そこで¬φを前提（仮定）として置いてみる．すると， 最初の前提とたちまち矛盾する（⊥がでる）．これを 形式的証明として書き下せば上のようになる．

【例５】¬¬φ |- φ （φは任意の論理式）

1: ¬¬φ（前提）

2: [¬φ]⁷（前提）

3: ⊥（1,2 ¬導入）

4: φ（3 ¬）

5: [φ]⁷（前提）

6: φ∨¬φ（排中律）

7: φ（6,4,5 ∨除去）

戦略は∨除去に持ち込むことである．すでに触れたように， ∨除去は場合分けの論法と考えることができる．今の場合の 場合分けの大前提は排中律（６行目）である．最終的に導出 したいのはφであるから，¬φが成立する場合というのは 実は起こり得ない．したがって¬φを仮定すれば（２行目） 矛盾をあらわす⊥が出てくる（３行目）．数学では， 矛盾が出たから背理法によって証明終わり，とするところ であるが，自然演繹ではここから何を出してもよいので 特にφを出して（４行目）∨除去につなげる（７行目） という面白い処理を行う．ちなみに，φが成立する場合には 普通は何もしなくていいわけだが，自然演繹ではφを 前提として置いて（５行目）それをただちに仮定として 落とす（７行目）．

この証明を一種の背理法と見ることもできる（背理法と 二重否定の関係についてはすでに触れた）．実際，証明の 本質的な部分は¬φを仮定して矛盾を導くという部分にある． φを仮定してただちに落とす部分には実質的な意味はなく， 単に∨導入の形を完成するための形式（いわば礼儀作法） に過ぎない．もちろん，ここで排中律が用いられていることは 極めて重要で，結局のところ二重否定の除去は排中律に 依存しているのである．

2.2 基本的な恒真式・演繹関係を形式的に確かめること

以下にいくつかの例を示す．いずれの例についても， まず形式的証明を示してから，説明や注釈を加えている． 特に，このような形式的証明を見つけるための戦略を 詳しく解説しているので，参考にされたい．ここに示した 形式的証明はあくまで一例であり，これ以外の証明も あり得る．

【例１】|- φ→（ψ→φ）（ウカシェビッチの第一公理）

1: [φ]⁴（前提）

2: [ψ]³（前提）

3: ψ→φ（2,1 →導入）

4: φ→（ψ→φ）（1,3 →導入）

【例２】|- (φ→(ψ→χ))→((φ→ψ)→(φ→χ))（ウカシェビッチの第二公理）

1: [φ→(ψ→χ)]⁹（前提）

2: [φ→ψ]⁸（前提）

3: [φ]⁷（前提）

4: ψ（3,2 →除去）

5: ψ→χ（3,1 →除去）

6: χ（4,5 →除去）

7: φ→χ（3,6 →導入）

8: (φ→ψ)→(φ→χ)（2,7 →導入）

9: (φ→(ψ→χ))→(φ→ψ)→(φ→χ))（1,8 →導入）

この例には自然演繹による形式的証明の特徴がよく現れている． この例を意味解釈に基づいて理解することはもちろん可能だが， 上の形式的証明のように，→の入り組み具合を純粋な「パターン」 として処理することもできるのである．

【例３】|- (¬ψ→¬φ)→(φ→ψ)（ウカシェビッチの第三公理）

1: [¬ψ→¬φ]¹¹（前提）

2: [φ]¹⁰（前提）

3: [¬ψ]⁹（前提）

4: ¬φ（3,1 →除去）

5: ⊥（2,4 ¬除去）

6: ψ（5 ⊥）

7: [ψ]⁹（前提）

8: ψ∨¬ψ（排中律）

9: ψ（8,6,7 ∨除去）

10: φ→ψ（2,8 →導入）

11: (¬ψ→¬φ)→（φ→ψ）（1,10 →導入）

【演習問題】ウカシェビッチの第二・第三の公理の逆

1. |- ((φ→ψ)→(φ→χ))→(φ→(ψ→χ))
2. |- (φ→ψ)→(¬ψ→¬φ)

【例４】|- ¬φ∨¬ψ→¬(φ∧ψ)（ド・モルガンの法則の一部）

1: [¬φ∨¬ψ]¹¹（前提）

2: [φ∧ψ]¹⁰（前提）

3: [¬φ]⁹（前提）

4: φ（2 ∧除去）

5: ⊥（3,4 ¬除去）

6: [¬ψ]⁹（前提）

7: ψ（2 ∧除去）

8: ⊥（6,7 ¬除去）

9: ⊥（1,5,8 ∨除去）

10: ¬(φ∧ψ)（1,9 ¬導入）

11: ¬φ∨¬ψ→¬(φ∧ψ)（1,10 →導入）

【例５】|- ¬(φ∧ψ)→¬φ∨¬ψ（ド・モルガンの法則の一部）

1: [¬(φ∧ψ)]¹²（前提）

2: [φ]¹¹（前提）

3: [ψ]⁶（前提)

4: φ∧ψ（2,3 ∧導入）

5: ⊥（1,4 ¬除去）

6: ¬ψ（3,5 ¬導入）

7: ¬φ∨¬ψ（6 ∨導入）

8: [¬φ]¹¹（前提）

9: ¬φ∨¬ψ（8 ∨導入）

10: φ∨¬φ（排中律）

11: ¬φ∨¬ψ（10,7,9 ∨除去）

12: ¬(φ∧ψ)→¬φ∨¬ψ（1,11 →導入）

このような場合にはある意味で前提を強めるしかない． もとの前提を強めるわけには行かないから，仮定として あとで落とすものを強めに設定することになる．仮定が落ちる 推論として今の場合に関係がありそうなのは¬除去と∨除去 である．∨除去を用いるならば∨で結ばれた前提が必要だが， すでに置いた前提はそうではないので排中律を使うしかない． 排中律はなるべく使わないという方針を採るならば（これは あとで議論する直観主義論理との関係を意識している）， まず¬除去を使う可能性を探るべきだろう．

そこでとにかくφを前提として置いてみる（２行目）．これで 何ができるかと考えると，実はまだ何もできない．そこで今度は ψに関わる前提を（あとで仮定として落とすことを想定して） 置いてみよう．ψそのものを前提として置けば（３行目）， ２行目の前提と組み合わせて１行目に矛盾する状況ができる （４，５行目）．ここで¬導入を用いれば¬ψが導かれて （６行目），そこから∨導入で¬φ∨¬ψが出せる（７行目）． 以上は２行目のφを前提とする推論過程である．

このφを仮定として落とすにはいよいよ排中律を使うしかない． 考えてみれば，目標の¬φ∨¬ψは¬φから∨導入で導ける式である （８，９行目）．そこで，排中律を呼び出して（１０行目） ∨導入でまとめる（１１行目）．あとは→導入で仕上げればよい．

【演習問題】可換律，結合律，分配律，吸収律，→の別表現， ド・モルガンの法則，対偶の法則を自然演繹によって 形式的に証明せよ．ただし，|-φ↔ψ という形の定理は |-φ→ψ と |-ψ→φ に分けて証明すること．

【例６】「Γ∪{¬φ} |- ⊥ ならば Γ|-φ である」という 超定理を証明せよ．

Γ∪{¬φ} |- ⊥ の推論過程を

1: ¬φ（前提）

… …

n: ⊥

n+1: φ（n ⊥）

n+2: φ（前提）

n+3: φ∨¬φ（排中律）

n+4: φ（n+3,n+1,n+2 ∨除去）

【注意】これは背理法の正当化である．背理法は

【演習問題】modus tollens，選言三段論法，仮言三段論法に相当する 派生推論規則

3. 排中律と直観主義論理

1. 林晋「数理論理学」（コロナ社，1989）
2. 松本和夫「数理論理学」（共立出版，初版1970，復刊2001）
3. 小野寛晰「情報科学における論理」（日本評論社，1994）

3.1 排中律に依存する定理と依存しない定理

1. 二重否定導入 |-φ→¬¬φ：証明に排中律を使わない
2. 二重否定除去 |-¬¬φ→φ：証明に排中律を使う

1. 二重否定導入は NJ，NK のいずれにおいても定理である
2. 二重否定除去はNK においてのみ定理である

同様の例は他にもいろいろある．排中律は¬に関わることなので， ¬を含まないものについてはこの違いはないと考えてよいが， ¬を含む論理式については NK で証明できても NJ で証明できない 場合が起こり得る．しかし¬が含まれていても排中律を使わないで 証明できる場合もあるのでややこしい．

特に興味深いのは，排中律を使えば |-φ→ψ, |-ψ→φ の 両方が証明できるが，使わないとどちらか一方しか証明できない， というような場合である．すでに指摘した二重否定の除去や， 前節で例題として採り上げたド・モルガンの法則（二つあるが， そのうちの一方）の場合もそうである：

1. |- ¬(φ∧ψ)→¬φ∨¬ψ：証明に排中律を使う
2. |- ¬φ∨¬ψ→¬(φ∧ψ)：証明に排中律を使わない

ちなみに，もう一方のド・モルガンの法則はどちら向きも 排中律を使わずに証明できる：

1. |-¬(φ∨ψ)→¬φ∧¬ψ：証明に排中律を使わない
2. |-¬φ∧¬ψ→¬(φ∨ψ)：証明に排中律を使わない

|-¬(φ∨ψ)→¬φ∧¬ψの証明：

1: [¬(φ∨ψ)]¹¹（前提）

2: [φ]⁵（前提）

3: φ∨ψ（2 ∨導入）

4: ⊥（1,3 ¬除去）

5: ¬φ（2,4 ¬導入）

6: [ψ]⁹（前提）

7: φ∨ψ（6 ∨導入）

8: ⊥（1,7 ¬除去）

9: ¬ψ（6,8 ¬導入）

10: ¬φ∧¬ψ（5,9 ∧導入）

11: ¬(φ∨ψ)→¬φ∧¬ψ（1,10 →導入）

|-¬φ∧¬ψ→¬(φ∨ψ)の証明：

1: [¬φ∧¬ψ]¹¹（前提）

2: [φ∨ψ]¹⁰（前提）

3: [φ]⁹（前提）

4: ¬φ（1 ∧除去）

5: ⊥（3,4 ¬除去）

6: [ψ]⁹（前提）

7: ¬ψ（1 ∧除去）

8: ⊥（6,7 ¬除去）

9: ⊥（2,5,8 ∨除去）

10: ¬(φ∨ψ)（2,9 ¬導入）

11: ¬φ∧¬ψ→¬(φ∨ψ)（1,10 →導入）

【演習問題】次の定理が排中律を使わないで証明できることを確かめよ．

1. |-¬(φ∧¬φ)
2. |-¬¬¬φ→¬φ
3. |-(φ→ψ)→(¬ψ→¬φ)
4. |-(¬¬φ→¬¬ψ)→(¬ψ→¬φ)
5. |-¬¬(φ∧ψ)→¬¬φ∧¬¬ψ
6. |-¬¬φ∧¬¬ψ→¬¬(φ∧ψ)

3.2 直観主義論理の意味論

ハイティング代数による直観主義論理の意味論を本格的に 説明するにはかなりの準備が必要なので，詳しい説明は 参考書に譲って，ここでは直観主義論理の非常に簡単な モデルを紹介する．

このモデルは T,N,F という３個の真理値に基づく意味解釈である． T と F は古典論理と同様に「真」および「偽」をあらわすと 思ってよい．N は新しいもので，T と F の中間の真理値と解釈される． これらの間に演算∧，∨，¬，→を次のように定める：

実はこの３個の要素からなる真理値集合 {T, N, F} が ハイティング代数の一つの例である．ハイティング代数は ブール代数と同様に２項演算 (x,y)→ x∧y, x∨y， 1項演算 x→x ' ならびに特別な要素Ｔ, ⊥をもつ代数系で， ブール代数の性質のうち，べき等律，可換律，結合律， 吸収律，分配律ならびに⊥,Ｔの性質 x∨⊥ = x, x∨Ｔ = Ｔ, x∧⊥ = x，x∧Ｔ = x はそのまま残して， 補要素 x ' に関するものを一部緩めている．具体的には，

という性質は要求されるが，排中律に相当する性質

はなくてもよいとする．実際，上の３値真理値集合 （ちなみに，そこではＴ = T, ⊥ = F）においては

となっている．

ハイティング代数においては x→y という２項演算も 同時に決まる．その定義は少し込み入っているので ここでは説明を省くが，一般に x→y と ¬x∨y は一致しない． ３値真理値集合 {T, N, F} の→もこの一般的な定義に従って 決めたものだが，そこでは

となっていて，x→y と ¬x∨y は確かに食い違っている．

論理式φに含まれる各命題記号に対して T, N, F の いずれかの値を割り当てれば，上の演算表に従ってφ自身の 真理値が T, N, F のいずれかとして決まる．このようにして ３値真理値集合 {T, N, F} に関する真理値割り当ての 概念が導入される．真理値割り当て M のもとでの論理式φの真理値を M[φ] とあらわす．これが真理値集合 {T, N, F} に基づく 意味解釈を定める．この意味解釈においては排中律

がもやは成立しないことは明らかだろう．

同様にして，一般のハイティング代数に基づく意味解釈を 導入することができる（これは「多値」の 意味解釈の一種と考えられる）．ハイティング代数に基づく 直観主義論理の意味論では単一のハイティング代数ではなくて さまざまなハイティング代数を一緒に考えることが重要になる．

直観主義論理における「恒真式」の定義もこの考え方に基づく． すなわち，論理式φが直観主義論理の意味で恒真式である（|=φ）とは， 任意のハイティング代数 A とその上の任意 の真理値割り当て M に対して常に T の値をとることを言う．これは ２値の真理値集合 {T, F} に基づく古典論理の恒真性とは まったく異なる概念であるから，混同してはならない． たとえばφ∨¬φは直観主義論理では恒真式ではない．

NJによる直観主義論理の形式化の妥当性はハイティング代数 による意味解釈で裏付けられる．実際，次のことが確かめられる （参考書を参照されたい）：

1. 任意のハイティング代数による意味解釈のもとで， NJの推論規則はいずれも妥当である（すなわち，前提の 真理値がいずれも T であれば，帰結の真理値も T である）．
2. 特に，NJはハイティング代数による意味解釈のもとで 健全である（すなわち |-φ ならば |=φ である）．

このことから，NKで形式的に証明できるがNJでは形式的に 証明できない論理式の存在が厳密に言える．

【例１】φ∨¬φはNJでは証明できない．証明できるとすれば NJの健全性からこれは恒真式のはずである．ところが， ３値真理値集合 {T, N, F} で解釈すれば，M[φ] = N のとき M[φ∨¬φ] = N ≠T となり，φ∨¬φは恒真式ではない．

【例２】(φ→ψ)→¬φ∨ψ はNJでは証明できない． 証明できるとすればNJの健全性からこれは恒真式のはずである． ところが,３値真理値集合 {T, N, F} で解釈すれば， M[φ] = N, M[ψ] = N のとき M[φ→ψ] = T, M[¬φ∨ψ] = N であり，特に M[(φ→ψ)→¬φ∨ψ] = N ≠T となる． すなわち (φ→ψ)→¬φ∨ψ は恒真式ではない．

【注意】¬φ∨ψ→(φ→ψ) はNJで証明できる．

【演習問題】上に示したハイティング代数 {T,N,F} のもとで NJの推論規則がいずれも妥当であることを確かめよ．

ヒント：証明を次の二段階に分ける （この証明の方針は前原昭二「記号論理学入門」の付録に基づく）．

1. 前提の真理値がいずれも F でなければ帰結の真理値も F でない．
2. 前提の真理値がいずれも T ならば帰結の真理値も T である．

第一の主張を踏まえれば，第二の主張を推論の行数に関する 数学的帰納法で証明することができる （推論規則のひとつひとつについて妥当性を確かめる）．

証明をこのように二段階に分けることは一見無駄に見えるが， 実は，第一の主張をあらかじめ証明しておかないと， 第二の主張の証明の中で→導入などの取り扱いに困る．実際， →導入に対しては M[φ] = T,F,N のそれぞれの場合について M[φ→ψ] = T となることを確かめなければならないが， M[φ] = N の場合には φ|-ψ に帰納法の仮定が適用できないため， M[ψ] について何ら結論が引き出せないのである． 第一の主張をあらかじめ証明しておけば， φ|-ψから M[ψ] = T あるいは M[ψ] = N がわかり， M[φ→ψ] = T が言える．

キーワード