An institution-independent proof of the Robinson consistency theorem (Q878156): Difference between revisions

The authors develop a very general proof of the Robinson consistency theorem within the framework of the so-called `institutions', a categorical abstract model theory which arose within algebraic specification theory. This effort is part of the grand project of institution-independent model theory, which attempts to develop model-theoretic methods and results independently of any commitment to any specific kind of logical systems. This proof, which of course subsumes the corresponding classical first-order result, has been instantiated to a large diversity of logical systems, thus obtaining a rather impressive array of concrete Robinson consistency results and consequently of interpolation results. Most notably, through this approach a difficult conjecture on many-sorted interpolation has received an elegant answer. Other remarkable applications include interpolation results in infinitary logics and in logics with partial functions.