Lindenbaum algebras of intuitionistic theories and free categories (Q1092043)

Lindenbaum algebras (LA) of countable classical theories often coincide. For example this is the case for propositional calculus and ZF set theory. The authors show that the situation is different in the intuitionistic case. While excluded middle (EM) can be stated as a single sentence in the presence of comprehension, it is proved (by extension of Kleene slash) that no consistent sentence implies all closed instances of EM in Heyting arithmetic. There are sentences weaker than complete EM, that imply all closed instances of EM in the second order arithmetic. An example is the existence of X, Y such that \[ \{X\subset Y,\quad ((n\in X\to m\in X)\to (n\in Y\to m\in Y))\quad and\quad n\in X\leftrightarrow n\in Y\to (n\in X\vee n\not\in X)\}. \] Similar tricks allow to distinguish between LA of (i) intuitionistic propositional predicate logic and arithmetic, ii) second order arithmetic, (iii) propositional and predicate logic with finite number of predicates and functions. Some results on representation of the free Heyting algebra on one generator in Lindenbaum algebra are presented.