この論文では，LKに comprehension axiom ∃y∀x(x∈y≡F(x)) を付加した形式的体系（但しここで F(x) には¬は現れない．このことを以下単に「制限された」と表現する）で次の結果の成り立つことが示されている：
⑴ この形式的体系で cut-elimination theorem が成り立つ．
⑵ 公理系 T,¬⊥,∃y∀x(x∈y≡F(x)) は LK上で無矛盾性である（ここに T,⊥ はpropositional constantで，内容的には前者は真な命題，後者は偽な命題を表わす）．
まず⑴については，その証明の方法は基本的にGentzenによるPeano算術の無矛盾性の証明に準ずる．粗くいえばindの部分を除き，そして証明図の終結部にあるsuitable cutのreductionにおいて制限された comprehension axiom（正確にはそれと同等な推論図）の場合を付け加えて考えればよい［と思う］．
次に⑵だが，これも大まかにいえば LK上 で無矛盾な公理系に制限された comprehension axiom を付加したものもまた無矛盾ということ［だろう］．
ここで個人的に疑問（＝調べたいこと）なのは，
・この結果の comprehension axiom において F(x) の（ ¬ についての）制限がどれだけ本質的なものか，という点．つまり仮にこの制限を除いたら，この論文の証明のどの過程でどのような問題が起こるのか？
・comprehension axiom において F(x)の ¬ についての制限の他に，どのような制限を課せば同様の結果が保たれるか？ 等々
まあ…時間が有り余っている時にでも調べよう．