Intuitionistic logic and axiomatic theories

Abstract

Pr ace zkoum a vlastnosti n ekter ych element arn ch intuicionistick ych teori . Vybr any jsou n asleduj c teorie: teorie rovnosti, line arn ho uspo r ad an , hust eho line arn ho uspo r ad an , teorie n asledn ka, Robinsonova aritmetika a teorie s c t an racion aln ch c sel; nav c t em e r ka zdou z t echto teori formulujeme dv ema r uzn ymi zp usoby. Z vlastnost teori n as zaj maj p redev s m n asleduj c cty ri: spl yv an s klasickou verz teorie, saturovanost, platnost De Jonghovy v ety a rozhodnutelnost. Diplomov a pr ace vych az zejm ena z v ysledk u C. Smorynsk eho a D. de Jongha a sna z se je rozvinout. N ekter e v ysledky zn am e pro Heytingovu aritmetiku dokazuje i pro jin e teorie. D ale se pokou s odpov ed et nap r klad na to, jak y vliv m a z am ena axiomu teorie za jin y (klasicky ekvivalentn ) axiom nebo jak e vlastnosti by m ela m t dobr a intuicionistick a teorie.

This thesis explores some properties of elementary intuitionistic theories. We focus on the following theories: the theory of equality, linear order, dense linear order, the theory of a successor function, Robinson arithmetic and the theory of rational numbers with addition; moreover, we usually deal with two dierent formulations of the theories. As for the properties, our main interest is in the following four: coincidence with the classical version of a theory, saturation, De Jongh's theorem and decidability. The thesis draws especially from the results of C. Smorynski and D. de Jongh and tries to develop them. Some results known for Heyting arithmetic are proved for other theories. We also try to answer the question of what is the eect of replacing an axiom by a dierent (classically equivalent) axiom, or which properties a \good" intuitionistic theory should have.