Wednesday Challenges

[1] We saw in the course two normalization strategies:

(a) Prawitz’ normalization strategy. This is based on the following result: in the fragment {conjunction, implication, negation, absurd, for all}, every application of the classical absurd rule can be restricted to atomic applications, i.e., to applications with atomic conclusions.

(b) Seldin’s normalization strategy. This is based on the following result: in the fragment {conjunction, implication, negation, for all, disjunction, existential}, every derivation  of Gamma proves A can be transformed into another derivation of Gamma proves A such that the new derivation has at most one application of the classical absurd rule. If this application occurs in the derivation, then it is the last rule applied.

Can these results be formulated for the sequent calculus LK?

[2] As a preparatory step for the proof of decidability of the propositional fragment of the intutionistic sequent calculus LJ, Gentzen proves the following result: A sequent Gamma proves A in this fragment is called reduced if no formula occurs in the sequent Gamma proves A, more than three times. If a reduced sequent Gamma proves A is provable in the fragment, then Gamma proves A has a reduced proof, i.e., a proof that contains only reduced sequents.

Question: Why “three times”??