Is every Heyting algebra the Lindenbaum algebra of an intuitionistic first order theory?

Question

This question comes after the comments in the recent related question Sigma-complete Lindenbaum algebras?, but in its current form is sufficiently different in my opinion, and so I decided to follow Joel's suggestion. It is also something I had asked myself before but never seriously considered.

Question 1: Is every Heyting algebra the intuitionistic Lindenbaum-Tarski algebra of some first-order theory over some language?

There are two possible motivations for this. First, the assertion would be true should one consider propositional theories instead. Second, an analogous result for categories is known to hold, and could be considered a generalization: every Heyting category is equivalent to the syntactic category of an intuitionistic first order theory (namely, the theory of the category itself).

In the case of an affirmative answer for Question 1, I would be also interested in an answer to

Question 2: Does the assertion in Question 1 (if true) requires some amount of choice? How much exactly? Is it, e.g., equivalent to BPI?

EDIT: Joseph has answered affirmatively Question 1 for the case of an arbitrary Boolean algebra: there is in fact a first order theory over a language whose Lindenbaum algebra is isomorphic to it (one could considered instances of excluded middle as part of the theory).

Remarkably, his proof does use BPI, which motivates also the corresponding version of Question 2 for the Boolean case:

Question 2': Is the assertion that every Boolean algebra is the Lindenbaum algebra of a first order theory equivalent to BPI?

EDIT 2: François' answer and his comments underneath give a simple complete solution.

Question 1: Yes

Question 2 & 2': No. Everything is provable in ZF.

Answer 1

I'm not sure why you seem to disallow propositional theories. Here is a workaround... Given a Heyting algebra $H$, add a unary predicate $P_a(x)$ for every $a \in H$ along with the axioms $$\forall x (P_{a \land b}(x) \leftrightarrow (P_a(x) \land P_b(x)))$$ $$\forall x (P_{a \lor b}(x) \leftrightarrow (P_a(x) \lor P_b(x)))$$ $$\forall x (P_{a \rightarrow b}(x) \leftrightarrow (P_a(x) \rightarrow P_b(x)))$$ $$\forall x (P_1(x) \land \lnot P_0(x))$$ To trivialize the role of equality, also add a constant symbol $*$ with the axiom $\forall x (x = *)$. It's not hard to see that every formula is then equivalent to one of the form $P_a(*)$ and the map $a \in H \mapsto [P_a(*)]$ is an isomorphism.

Answer 2

Given a Boolean algebra $B$, I shall construct a theory whose Lindenbaum-Tarski algebra is isomorphic to $B$. I do not know anything about intuitionistic logic, so I will answer this question just for first order logic and Boolean algebras.

Let $B$ be a Boolean algebra. Let $V$ be the variety consisting of all algebras $(A,(c_{a})_{a\in B})$ such that $A$ is a Boolean algebra and $c_{a}\wedge c_{b}=c_{a\wedge b},c_{a}\vee c_{b}=c_{a\vee b},c_{0}=0,c_{1}=1$ whenever $a,b\in A$. Then $V$ is a variety. Let $T$ be the theory of all algebras $\mathcal{A}=(A,(c^{\mathcal{A}}_{a})_{a\in B})\in V$ such that $|A|=2$. I claim that the mapping $L:B\rightarrow Sent(T)$ given by $L(b)=[c_{b}=1]$ is a Boolean algebra isomorphism.

Take note that $L(1)=[c_{1}=1]=1$ and $L(0)=[c_{0}=1]=0$. Furthermore, $$L(a)\wedge L(b)=[c_{a}=1]\wedge[c_{b}=1]=[c_{a}\wedge c_{b}=1]=[c_{a\wedge b}=1]=L(a\wedge b).$$ Furthermore, we have $L(a)\vee L(b)=[c_{a}=1]\vee[c_{b}=1]=[c_{a}\vee c_{b}=1]=[c_{a\vee b}=1]=L(a\vee b)$. Therefore $L$ is a Boolean algebra homomorphism. To show that $L$ is injective, suppose that $a\neq 1$. Then there is a Boolean algebra homomorphism $\phi:B\rightarrow 2$ with $\phi(a)=0$. In particular, if $\mathcal{A}=(2,(c^{\mathcal{A}}_{a})_{a\in B})$ and $c^{\mathcal{A}}_{b}=\phi(b)$ for $b\in B$, then $\mathcal{A}\models T$, but also $\mathcal{A}\models c_{a}\neq 1$. Therefore $L(a)=[c_{a}= 1]\neq 1$. We conclude that $L$ is an injective Boolean algebra since its kernel is trivial. Now assume that $\Phi$ is a sentence in $T$. It is easy to see that the theory of $T$ has quantifier elimination: We can simply replace a formula $\forall x\Phi(x)$ with $\Phi(0)\wedge\Phi(1)$ and $\exists x\Phi(x)$ with $\Phi(0)\vee\Phi(1)$. Therefore every sentence in the language of $T$ is equivalent to a quantifier free sentence. Furthermore, every quantifier free sentence in $T$ can easily be reduced to a sentence of the form $c_{a}= 1$. Therefore every sentence in the language of $T$ is equivalent modulo $T$ to a sentence of the form $c_{a}=1$. Therefore every element $[\Phi]$ in $Sent(T)$ is of the form $L(a)=[c_{a}=1]$ for some $a\in B$. In other words, the mapping $L$ is surjective. We conclude that $L$ is an isomorphism.

Answer 3

Here is a partial answer in the case of complete Boolean algebras, which I claim do all arise as Lindenbaum algebras. Let $\mathbb{B}$ be a complete Boolean algebra, and suppose that $M$ is any $\mathbb{B}$-valued structure in a first-order language, for which every $b\in\mathbb{B}$ arises as the Boolean value $[\![\varphi]\!]$ of some formula. This is true, for example, with the Boolean-valued models usually built in the case of models of set theory, in the forcing language, since if $\dot G$ is the canonical name of the generic filter, then $[\![\check b\in\dot G]\!]=b$ for any $b\in\mathbb{B}$. But there are many other examples.

Now, let $T$ be the theory of all sentences $\sigma$ in the language of $M$ for which $[\![\sigma]\!]=1$. I claim that the Lindenbaum algebra of formulas under equivalence modulo $T$ is precisely isomorphic to $\mathbb{B}$. My isomorphism is just $\sigma\mapsto[\![\sigma]\!]$. This is well-defined, because if $T$ proves $\sigma\leftrightarrow\eta$, then $[\![\sigma]\!]=[\![\eta]\!]$. It is a Boolean homomorphism, and it is onto. Finally, it is an isomorphism, because if $[\![\sigma]\!]=[\![\eta]\!]=b$, then it follows that $[\![\neg\sigma]\!]=[\![\neg\eta]\!]=\neg b$ and consequently $[\![\sigma\leftrightarrow\eta]\!]=b\vee \neg b=1$. Thus, $\sigma$ and $\eta$ are provably equivalent modulo $T$.

Conclusion: any Boolean algebra that arises as the collection of Boolean values in a Boolean-valued model arises as a Lindenbaum algebra, and this includes every complete Boolean algebra.

Perhaps one can hope to generalize this to Heyting-valued models in your intuitionistic context.

Answer 4

It is known that any Heyting algebra is the Lindenbaum algebra of some theory in the second order intuitionistic propositional calculus. I believe this gives affirmative answer to your question although I do not know enough to be sure.

In the 1992 JSL paper "On an Interpretation of Second Order Quantification in First Order Intuitionistic Propositional Logic" (JSTOR; draft version freely available) Andy Pitts constructed quantifiers out of any Heyting algebra $H$. There are operators $A_p,E_p:H[p]\to H$ such that for any Heyting algebra polynomial $\phi(p)$ with coefficients in $H$ and any $h\in H$, one has $\phi(p)\leqslant h$ in $H[p]$ (with $h$ regarded as a constant polynomial) iff $E_p(\phi(p))\leqslant h$ in $H$, and $h\leqslant\phi(p)$ iff $h\leqslant A_p(\phi(p))$.

It follows that the generic model of the theory of $H$-algebras (i. e. Heyting algebras together with a homomorphism from $H$ to them) produces a model of soipc. For details see the last page of the paper.

Pitts also asked whether this can be extended to higher orders. Because of the correspondence between higher order intuitionistic type theories and elementary toposes, a variant of his question is whether for any Heyting algebra $H$ there exists a topos with $H$ as the lattice of all subobjects of the terminal object.

Dito Pataraia has an amazing construction of such a topos, although more than two years after his death we (his closest friends and colleagues) still have not managed to turn his work into a publication. This is mostly my fault I have to admit.

For complete $H$ a solution is given by the topos of sheaves on $H$.

For a (not necessarily complete) Boolean algebra $B$ there is a construction by Freyd which goes as follows. Present $B$ as a filtered colimit of a diagram of finite algebras $(B_i, \iota_{ij}:B_i\to B_j)$ (for example, union of all finite subalgebras of $B$). Each finite $B_i$ is the algebra of subobjects of 1 in the topos $\mathbf T_i=\mathbf{Sets}^{\textrm{atoms of $B_i$}}$ (or if you prefer you can take only finite sets), and each $\iota_{ij}$ induces a logical functor $\mathbf T_i\to\mathbf T_j$ (reindexing along the dual map between atoms in the opposite direction). The colimit of this diagram of logical functors gives a topos $\mathbf T$ whose algebra of subobjects of 1 is $B$. (This is an exercise in the first topos book of Johnstone.)

Perhaps more explicitly one may view this $\mathbf T$ as follows. Let $X_B$ be the dual space of $B$ (any zero-dimensional compact Hausdorff space). Then objects of $\mathbf T$ are given by local homeomorphisms $Y\to X_B$ which can be realized as pullbacks along a continuous map $X_B\to X$ of a map $Y'\to X$ of finite sets (with discrete topology). Thus such objects are represented by finite strict $B$-valued sets: finite sets $S$ equipped with an equality predicate $\mathrm{eq}_S:S\times S\to B$ such that for any $s,s'\in S$, either $\mathrm{eq}_S(s,s')=0$ or $\mathrm{eq}_S(s,s')=\mathrm{eq}_S(s,s)=\mathrm{eq}_S(s',s')$. Morphisms $(S,\mathrm{eq}_S)\to(T,\mathrm{eq}_T)$ are then defined as usual with $B$-valued sets, i. e. as certain predicates $S\times T\to B$ serving as graphs of maps.

All this however heavily uses Booleanness of $B$. At least Dito's construction is completely different and much more involved.