Computing interpolants in implicational logics (Q2503400)

Motivated by a problem in the simply typed lambda-calculus which concerns a certain computational model of acquisition of word meanings by children, the author investigates how interpolants are obtained in the implicational fragment of intuitionistic logic. Through a fine proof-theoretical analysis of well-known syntactical methods for proving the interpolation theorem, one on the Gentzen system by Maehara and the other on the natural deduction system by Prawitz, it is shown that Maehara's method gives rise to many interpolants (for a given partition of a provable sequent) including more information than the usually stated ones, but there exist also some interpolants that are not available by the method, while Prawitz's method determines a unique interpolant that is contained in those obtained by Maehara's. On the basis of this analysis, the author introduces an order between interpolants and provides a new algorithm, applied to normal deductions, which constructs a ``strongest'' interpolant under a certain restricted but reasonable notion of what counts as an ``interpolant''. The argument is carried out by careful use of structural rules, so that the observations are relativised to the substructural subsystems in parallel by suitable modifications.