Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

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.

share|improve this question

4 Answers 4

up vote 4 down vote accepted

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.

share|improve this answer
    
François, I think this could work once you prove that your theory is consistent (otherwise the map is not injective), maybe there one needs BPI. Besides that, I think this works, doesn't it? –  godelian Apr 1 at 16:50
    
@godelian: In the classical case, that the theory is satisfiable is equivalent to BPI, but no choice is needed to see that the theory is consistent. –  François G. Dorais Apr 1 at 16:53
    
Oh, I see...so every finite subset of the axioms is satisfiable since one can find an ultrafilter (without choice) in the countable subalgebra generated by the elements of $H$ they involve. But then the theory is indeed consistent... –  godelian Apr 1 at 17:10
    
What about the injectivity of the map? I see how to prove it using BPI, but did you have a choice free proof in mind? –  godelian Apr 1 at 17:30
    
@godelian: There is an $H$-valued model that separates all equivalence classes. –  François G. Dorais Apr 1 at 18:14

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.

share|improve this answer
    
Hi Joseph, very nice! Could you expand a bit on why $T$ has quantifier elimination? –  godelian Apr 1 at 7:51
    
Very nice argument! –  Joel David Hamkins Apr 1 at 12:58
    
I explained why quantifier elimination works in this theory. –  Joseph Van Name Apr 1 at 14:43
    
Excellent, thanks! I tried to see if this argument could be used for the Heyting case, adding the condition $c_a \to c_b=c_{a \to b}$, but the only problem is that when you want to prove that $L$ is injective one should use Heyting algebra homomorphisms, which correspond to ultrafilters if the codomain is $2$. Unfortunately, ultrafilters (unlike prime filters) do not separate points in the Heyting case (for instance, they do not distinguish between $1$ and an instance of excluded middle) –  godelian Apr 1 at 14:55

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.

share|improve this answer
    
I'm using only sentences in my algebra, but do you want to allow formulas also, with free variables? If so, that is a complication. –  Joel David Hamkins Apr 1 at 1:33
    
I was rather thinking on sentences, so it's ok. I'm however not sure if this could be generalized to the Heyting case since it seems to rely on the fact that $b \vee \neg b=1$ –  godelian Apr 1 at 7:55

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 paper "On an Interpretation of Second Order Quantification in First Order Intuitionistic Propositional Logic" (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.

share|improve this answer
    
Thanks! I'll check the paper to see if it helps. –  godelian Apr 1 at 14:57

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.