Lindstroem’s theorem, both syntax and semantics free

摘要

Lindstroem’s theorem characterizes first-order logic in terms of its essential model theoretic properties. One cannot gainexpressive power extending first-order logic without losing at least one of compactness or downward L?wenheim–Skolemproperty. We cast this result in an abstract framework of institution theory, which does not assume any internal structureeither for sentences or for models, so it is more general than the notion of abstract logic usually used in proofs of Lindstr?m’stheorem; indeed, it can be said that institutional model theory is both syntax and semantics free. Our approach takes advantageof the methods of institutional model theory to provide a structured proof of Lindstr?m’s theorem at a level of abstractionapplicable to any logical system that is strong enough to describe its own concept of isomorphism and its own concept ofelementary equivalence.We apply our results to some logical systems formalized as institutions and widely used in computerscience practice.