Některé sémantické metody v intuicionistické logice

Abstract

V práci se podíváme do světa intuicionistické logiky. Zjistíme že v intuicionistické logice nelze definovat logické spojky pomocí jiných logických spojek. Podíváme se, jak je to v intuicionistické logice s jednoatomovými formulemi, ukážeme, že je můžeme vyčerpávajícím způsobem zorganizovat. Také se budeme věnovat kripkovským modelům a uvidíme, že v některých případech lze vydatně zredukovat nosnou množinu kripkovského modelu. Předložíme nástroje, pomocí kterých poznáme, které prvky jsou v modelu jaksi "navíc" a tudíž je můžeme z modelu "vyškrtnout". Na závěr se soustředíme na jednoatomové modely a na to, jak to vypadá s jejich složitostí, když je maximálně redukujeme. V práci je využito toho, že lze písmem rozlišit dvě implikace ---+ a ~- První z nich je používána jako implikace v rámci diskutovaných formulí, druhá jako prvek metajazyka, kterým si povídáme o této problematice. Při důkazech tvrzení o intuicionistické logice se řídíme pravidly klasické logiky. Písmena A, B, C, ... a z, cp, lf/, . . . představují formule, písmena p, q představují atomy.