1 型の推論者

スマリヤンの決定不能の論理パズル を相変わらず読んでるのですが、つまずいたところがあったので、頭の整理を兼ねてメモ。
なかなか理解できなかったのが、以下の論法。
教授が生徒に「君が神の存在を信じないならば、そしてそのときに限り神は存在する」と言ったとする。
ここで生徒は

• すべての恒真式を信じる。
• 任意の命題 X と Y について、X と X ⊃ Y を信じるならば Y を信じる。
• 自分が命題 X を信じるならば X は真である、と信じている。

とする。このとき
(a) 生徒が教授の言うことを信じるならば、生徒は神の存在を信じ、かつ自分が神の存在を信じないことを信じる。
(b) さらに教授の言うことが真ならば、神は存在しないが、生徒は神の存在を信じる。

まず (a) から。
神が存在するという命題を g 、命題 p を信じるという命題を Bp と表すと、

1. B(¬Bg ≡ g)　（「神の存在を信じないならば、そのときに限り神は存在する」と信じる）
2. B(Bg ⊃ g)　（「自分が神の存在を信じるならば神は存在する」と信じる）
3. B( (¬Bg ≡ g) ∧ (Bg ⊃ g) )　（1. と 2. より）
4. B( (¬Bg ∧ g) ∨ (Bg ∧ ¬g) ) ∧ (¬Bg ∨ g) )　（3. より）
5. B(¬Bg ∧ g)　（4. より）
6. B(¬Bg) ∧ Bg　（5. より）

となって、(a) 生徒は神の存在を信じ、かつ自分が神の存在を信じないことを信じる ことが示せた。
つぎに (b) を。

1. ¬Bg ≡ g　（神の存在を信じないならば、そのときに限り神は存在する）
2. Bg　（(a)6. より）
3. Bg ∧ (¬Bg ≡ g)　（1. と 2. より）
4. Bg ∧ ( (¬Bg ∧ g) ∨ (Bg ∧ ¬g) )　（2. より）
5. Bg ∧ ¬g　（3. より）

となって、(b) 神は存在しないが、生徒は神の存在を信じる ことが示せた。

こういう生徒を 1 型の推論者というらしいのですが、これは一般的な用語なんでしょうか？それともスマリヤンが勝手につけた呼び名？
あと(a)の5.から6.の推論が妥当なのかもちょっと気になります。