I detta dokument studeras finita modala logiker, tolkas över kolgebras för en endofunctor, och etablerar sundhet, fullständighet och decisionability resultat. Logikerna studeras inom den abstrakta ramen för kolgebraisk modal logik, som kan direktieras med godtyckliga endofunctors på kategorin av uppsättningar. Detta uppnås genom användning av predikativa lyft, som generaliserar atomförslag och modala operatörer från Kripke modeller till godtyckliga kolgebras. Predicate lyft gör också att vi kan använda induktion längs terminalsekvensen av den underliggande endofunctor som en bevisprincip. Denna induktionsprincip utnyttjas systematiskt för att etablera logikens sundhet, fullständighet och decibilitet. Vi tror att denna induktionsprincip också öppnar nya sätt att resonera om modala logiker: Vårt bevis på fullständighet bygger inte på en kanonisk modellkonstruktion, och beviset på den finita modellens egenskap använder inte filtrering.
Kolgebraisk modallogik REF strävar efter att på ett enhetligt sätt studera modallogiken över olika typer av strukturer.
Coalgebraic modal logic: Soundness, completeness and decidability of local consequence
{'venue': 'Theoret. Comput. Sci', 'journal': None, 'mag_field_of_study': ['Mathematics', 'Computer Science']}