Uniformin yksiulotteisen fragmentin ratkeavuus
Tirkkonen, Topi (2026)
2026
Matematiikan ja tilastollisen data-analyysin maisteriohjelma - Master's Programme in Mathematics and Statistical Data Analytics
Informaatioteknologian ja viestinnän tiedekunta - Faculty of Information Technology and Communication Sciences
Hyväksymispäivämäärä
2026-06-10
Julkaisun pysyvä osoite on
https://urn.fi/URN:NBN:fi:tuni-202606057024
https://urn.fi/URN:NBN:fi:tuni-202606057024
Tiivistelmä
Tutkielmassa osoitetaan, että ensimmäisen kertaluvun logiikan uniformi yksiulotteinen fragmentti on ratkeava. Kyseinen fragmentti yleistää tunnetumpaa kahden muuttujan logiikkaa sallimalla useampi kuin kaksipaikkaisia predikaatteja. Logiikkojen yhteys toisiinsa ei välttämättä ole selvä pelkästään määritelmistä, ja tätä yhteyttä avataan. Kahden muuttujan logiikkaa ei käsitellä enempää, vaan siirrytään ratkeavuuden tutkimiseen.
Ensimmäisen kertaluvun logiikan ratkeavat fragmentit ovat ilmaisuvoimaltaan ensimmäisen kertaluvun logiikkaa heikompia, mutta ne saattavat silti kyetä ilmaisemaan epätriviaaleja käsitteitä. Ratkeavien fragmenttien ilmaisuvoimaa havainnollistetaan esimerkein. Ratkeavuuden osoitetaan olevan avainasemassa formaalin todistamisen automatisoimisessa. Lisäksi osoitetaan, että fragmenttien ratkeavuus seuraa äärellisen mallin ominaisuudesta, johon uniformin yksiulotteisen fragmentin ratkeavuustodistus perustuu.
Tutkielmassa esitellään tutkittavan logiikan kaavojen Scottin normaalimuoto, joka koostuu ainoastaan konjunkteista, joissa on ainoana kvantifiointina edessä joko toistuva universaali- tai yksittäistä universaalikvanttoria seuraava toistuva eksistenssikvantifiointi. Scottin normaalimuodon osoitetaan olevan yhtätoteutuva alkuperäisen kaavan kanssa. Ratkeavuustodistus pohjautuu Scottin normaalimuodossa olevien kaavojen tutkimiseen, sillä näiden totuutta on helpompi tarkastella.
Ratkeavuustodistus etenee tavanmukaisesti esittelemällä niin kutsuttu "kuninkaallinen hovi", jossa "kuninkaat" ovat todistettavana olevan tuloksen kannalta hankalasti käyttäytyviä alkioita. Hankaluudet väistetään huomioimalla kaikki kuninkaat erikseen. Muuntyyppisten alkioiden kohdalla ristiriitojen välttämiseksi todistuksessa esiintyy syklisyyttä siten, että alkiot saattavat tarvita "todistajia" jostakin toisesta joukosta, jotka puolestaan tarvitsevat todistajia jälleen uudesta joukosta, jotka lopulta nekin tarvitsevat todistajia, mutta nämä voidaan valita joukosta, josta lähdettiin liikkeelle.
Lopuksi tutkielmassa osoitetaan, että tutkittavan fragmentin uniformisuus ja yksiulotteisuus eivät yksin riitä ratkeavan fragmentin muodostamiseksi. Täten esitellään fragmentit, joissa on vain toinen rajoituksista. Nämä ovat vahvasti uniformi kaksiulotteinen fragmentti sekä yleinen yksiulotteinen fragmentti. Ratkeamattomuus osoitetaan reduktioina tiilausongelmaan molemmille fragmenteille.
Ensimmäisen kertaluvun logiikan ratkeavat fragmentit ovat ilmaisuvoimaltaan ensimmäisen kertaluvun logiikkaa heikompia, mutta ne saattavat silti kyetä ilmaisemaan epätriviaaleja käsitteitä. Ratkeavien fragmenttien ilmaisuvoimaa havainnollistetaan esimerkein. Ratkeavuuden osoitetaan olevan avainasemassa formaalin todistamisen automatisoimisessa. Lisäksi osoitetaan, että fragmenttien ratkeavuus seuraa äärellisen mallin ominaisuudesta, johon uniformin yksiulotteisen fragmentin ratkeavuustodistus perustuu.
Tutkielmassa esitellään tutkittavan logiikan kaavojen Scottin normaalimuoto, joka koostuu ainoastaan konjunkteista, joissa on ainoana kvantifiointina edessä joko toistuva universaali- tai yksittäistä universaalikvanttoria seuraava toistuva eksistenssikvantifiointi. Scottin normaalimuodon osoitetaan olevan yhtätoteutuva alkuperäisen kaavan kanssa. Ratkeavuustodistus pohjautuu Scottin normaalimuodossa olevien kaavojen tutkimiseen, sillä näiden totuutta on helpompi tarkastella.
Ratkeavuustodistus etenee tavanmukaisesti esittelemällä niin kutsuttu "kuninkaallinen hovi", jossa "kuninkaat" ovat todistettavana olevan tuloksen kannalta hankalasti käyttäytyviä alkioita. Hankaluudet väistetään huomioimalla kaikki kuninkaat erikseen. Muuntyyppisten alkioiden kohdalla ristiriitojen välttämiseksi todistuksessa esiintyy syklisyyttä siten, että alkiot saattavat tarvita "todistajia" jostakin toisesta joukosta, jotka puolestaan tarvitsevat todistajia jälleen uudesta joukosta, jotka lopulta nekin tarvitsevat todistajia, mutta nämä voidaan valita joukosta, josta lähdettiin liikkeelle.
Lopuksi tutkielmassa osoitetaan, että tutkittavan fragmentin uniformisuus ja yksiulotteisuus eivät yksin riitä ratkeavan fragmentin muodostamiseksi. Täten esitellään fragmentit, joissa on vain toinen rajoituksista. Nämä ovat vahvasti uniformi kaksiulotteinen fragmentti sekä yleinen yksiulotteinen fragmentti. Ratkeamattomuus osoitetaan reduktioina tiilausongelmaan molemmille fragmenteille.