Normal form theorem for systems of sequents
Keyword(s):
In a system of sequents for intuitionistic predicate logic a theorem, which corresponds to Prawitz?s Normal Form Theorem for natural deduction, are proved. In sequent derivations a special kind of cuts, maximum cuts, are defined. Maximum cuts from sequent derivations are connected with maximum segments from natural deduction derivations, i.e., sequent derivations without maximum cuts correspond to normal derivations in natural deduction. By that connection the theorem for the system of sequents (which correspond to Normal Form Theorem for natural deduction) will have the following form for each sequent derivation whose end sequent is ??A there is a sequent derivation without maximum cuts whose end sequent is ??A.
1977 ◽
Vol 67
(2)
◽
pp. 215-215
◽
Keyword(s):
Keyword(s):
2019 ◽
Vol 375
(3)
◽
pp. 2089-2153
◽
Keyword(s):
2018 ◽
Vol 12
(3)
◽
pp. 363-424
Keyword(s):
2007 ◽
Vol 17
(05n06)
◽
pp. 951-961
◽