「ゲーデル 不完全性発見への旅」のド・モルガンの法則の証明

P49の解説の中でド・モルガンの法則を勝手に使っているわけですが、
そこは証明が必要です。

* (B => A) => (^A => ^B) :[逆対偶律]
(1) A => ^^A :[二重否定付加{A -> A}]
(2) (B => A) => (B => ^^A) : [仮定付前件後件前件付加{(B => C) -> (1),A -> B}]
(3) ^^B => B :[公理11{A -> B}]
(4) (B => ^^A) => (^^B => ^^A) : [仮定付後件前件後件付加{(A => B) -> (3),C => ^^A}]
(5) (^^B => ^^A) => (^A => ^B) : [対偶律{A -> ^A, B -> ^B}]
(6) (B => A) => (^A => ^B) : [三段論法{(2),(4),(5)}]
* (^B \/ ^C) => ^(B /\ C) : [ド・モルガンの法則1]
(1) B /\ C => B : [公理5{A -> B, B -> C}]
(2) ((B /\ C) => B) => (^B => ^(B /\ C)) : [逆対偶律{A -> B, B -> (B /\ C)}]
(3) ^B => ^(B /\ C) : [mp{(1),(2)}]
(4) B /\ C => C : [公理6{A -> B, B -> C}]
(5) ((B /\ C) => C) => (^C => ^(B /\ C)) : [逆対偶律{A -> C, B -> (B /\ C)}]
(6) ^C => ^(B /\ C) : [mp{(4),(5)}]
(7) (^B => ^(B /\ C)) => ((^C => ^(B /\ C)) => ((^B \/ ^C) => ^(B /\ C))) : [公理9{A -> ^B, B -> ^C, C -> ^(B /\ C)}]
(9) (^B \/ ^C) => ^(B /\ C) : [mp {(3),(6),(7)}]

1月22日の「ゲーデルを読もう」第3回にて、モデル理論の話があった。
モデル理論では、「真偽は定まる」としているようだ。
真偽概念そのものは、数学の外にゆだねるってことですかね。