MARGINALIA ON GENTZEN'S SEQUENZEN-KALKÜLE

Publisher Summary Gentzen fashioned in two novel versions of elementary logic or, to be more precise, of the quantificational calculus of first order (QC). One kalkul, called LK, sports besides the standard primitives of QC a fresh primitive, the symbol →; it also sports besides the standard formulas of QC so-called sequents. Gentzen's other kalkul, NK, can be thought of as a fragment of LK, a fragment that also boasts the primitive →. This chapter presents that all valid sequents of LK are susceptible in LK of direct proofs in both of the senses of the word direct and that all valid propositional sequents of NK are susceptible in NK of direct proofs in the weaker sense of the word direct. It also presents that not all valid propositional sequents of NK are susceptible in NK of direct proofs in the stronger sense of the word direct and that not all valid quantificational sequents of NK are susceptible in NK of direct proofs in the weaker sense of the word direct.