L'inexistence des licornes et les théorèmes de L"owenheim-Skolem à plusieurs sorts

L'infinité stable, la forte témoinabilité finie et la douceur sont des propriétés logiques pertinentes pour la combinaison de théories dans la satisfiabilité modulo théories. Les théories qui sont fortement témoins finies et douces sont appelées fortement polies et peuvent être combinées efficacement avec d'autres théories. Toledo, Zohar et Barrett ont conjecturé que les théories stablement infinies et fortement témoins finies sont douces et donc fortement polies. Ils ont appelé contre-exemples à cette conjecture des théories licornes, car leur existence semblait peu probable. Nous prouvons qu'en effet, les licornes n'existent pas. Nous prouvons également des versions du théorème de L"owenheim-Skolem et du test de o's-Vaught pour la logique à plusieurs sorts.