Types of I-free hereditary right maximal terms (Q812102)

By the formulas-as-types (or Curry-Howard) isomorphism, for every closed \(\lambda\)-term there is a theorem of the implicational intuitionistic logic \(H_\to\), which is its type. Also, every such theorem is the type of a \(\lambda\)-term which represents a natural deduction style proof of the theorem. The theorems of weaker logics than \(H_\to\) have subsets of the closed lambda terms as their sets of proofs/inhabitants. Such subsets of the closed lambda terms were identified by \textit{P. Trigg, J. R. Hindley} and \textit{M. W. Bunder} [``Combinatory abstraction using \(B, B'\) and friends'', Theor. Comput. Sci. 135, 405--422 (1994; Zbl 0838.03012)] for a large number of logics including the implicational fragment \(T_\to\) of Ticket Entailment. Other work on this appears in the reviewer's chapter ``Combinators, proofs and implicational logics'' [in: D. M. Gabbay and F. Guenthner (eds.), Handbook of philosophical logic. Vol. 6. 2nd ed. Dordrecht: Kluwer, 229--286 (2002; Zbl 1065.03002)]. The current paper also identifies the class of \(\lambda\)-terms representing the proofs of \(T_\to\) and finds a Fitch-style formulation for \(T_\to\).