Kvanttoriasteen säilyttävä Rossmanin homomorfismilause syntaktisesta näkökulmasta

Abstract

Säilymislauseina tunnetut tulokset kuvailevat malliteoriassa erilaisia yhteyksiä kaavojen syntaktisen rakenteen ja kaavat toteuttavien mallien semanttisten ominaisuuksien välillä. Esimerkiksi jokainen ensimmäisen kertaluvun logiikan eksistentiaalis-positiivinen kaava säilyy homomorfismien suhteen. Käänteiseen suuntaan jokainen homomorfismeissa säilyvä ensimmäisen kertaluvun kaava voidaan loogisesti yhtäpitävästi esittää myös eksistentiaalis-positiivisessa muodossa. Parannuksena tähän on Benjamin Rossman osoittanut, että jokainen funktiosymboleja sisältämätön ja homomorfismeissa säilyvä ensimmäisen kertaluvun kaava voidaan esittää eksistentiaalis-positiivisessa muodossa ilman tarvetta kaavan kvanttoriasteen kasvamiselle.

Tässä tutkielmassa Rossmanin menetelmää kehitetään hieman eteenpäin osoittamalla, että jokainen funktiosymboleja sisältämätön ja homomorfismien suhteen säilyvä kaava on mahdollista muuttaa eksistentiaalis-positiiviseen muotoon sellaisella tavalla, että tuloksena olevan kaavan syntaktista rakennetta saadaan rajattua alkuperäisen kaavan rakenteen avulla ja että tuloksena olevan kaavan kvanttoriasteeksi riittää pelkkä alkuperäisen kaavan eksistenssikvanttoreista laskettu kvanttoriaste. Todistuksen työvälineenä esitellään eräs yleistys malliteoriassa perinteisesti käytetyistä ja erilaisten mallirakenteiden vertailuun soveltuvista kahden pelaajan peleistä.