The Hauptsatz for Stratified Comprehension: A Semantic Proof
Marcel Crabbé · Mathematical logic quarterly · 1994
Abstract We prove the cut‐elimination theorem, Gentzen's Hauptsatz, for the system for stratified comprehension, i. e. Quine's NF minus extensionality. Mathematics Subject Classification: 03B15, 03F05.