Relace bisimulace

Abstract

Tato práce se zabývá relací bisimulace v modální logice a také v intuicionistické logice bez kontrakce. Bisimulace je relace mezi sémantickými modely, která je slabí neo isomor smus, ale přitom pořád zaruuje ekvivalenci v dané logice. Jejím typickým pouoitím jsou d·kazy nerozliitelnosti uritých typ· struktur jazykem dané logiky. Příkladem takové vlastnosti je kardinalita modálních model·, jejío nerozliitelnost ukazuje konstrukce disjunktního sjednocen í. Pro modální logiku má relace bisimulace velký význam jet také proto, oe objas ňuje její vztah ke klasické prvořádové logice. Krom bisimulace je zkoumán také souvisej ící pojem vázaného mor smu, který umooňuje převést výsledky o nede novatelnosti i na úroveň rámc·. ást o modální logice je předevím shrnutím obecn známých výsledk·, přiemo se snaoí objasnit jejich souvislosti, případn rozvést nkteré d·kazy, které se obvykle přecházejí jako zřejmé. U mén prozkoumané intuicionistické logiky bez kontrace spoívá znaná ást práce uo v samotné de nici její sémantiky a zajitní její funknosti. Také zde je ovem zavedena bisimulace i vázaný mor smus a na jejich konkrétních příkladech je naznaeno mooné vyuoití.

This work is about bisimulation in modal logic as well as in intuicionistic logic without contraction. Bisimulation is a relation between models, which is weaker than isomorphism, yet still guarantees equivalence in the in the selected logic. It is typically used to demonstrate that some properties of models cannot be distinguished. For instance the cardinality cannot be distinguished, which is shown by disjunct union. Bisimulation also helps to clarify the relation between modal and classical logic. Apart from bisimulation, the related notion of bounded morphism is studied because it enables to elevate the unde- nability and undistinguishability to the discourse of frames. The part about modal logic is basically a compilation of well known facts, yet their interaction is made more clear and some proofs, which are usually disregarded as obvious, are presented in an explicit manner. Talking about the second part, mere reasonable de nition of the semantics is an honest work. Yet even here the bisimulation and bounded isomorphism are introduced and some examples are shown in order to illustrate their utility.