0
$\begingroup$

A Heyting algebra is a bounded distributive lattice $(L,\vee,\wedge,0,1)$ together with a binary operation $\rightarrow$ called implication or relative pseudocomplementation with the property that, for all $x,y,z\in L$, $$ x\le y\rightarrow z\quad\text{ if and only if } x\wedge y\le z. $$ Boolean algebras and finite distributive lattices are examples.

Free Heyting algebras exist. A free Heyting algebra $H$ with generating set $X$ has the property that $X\subseteq H$ and any function from $X$ to a Heyting algebra $K$ can be extended uniquely to a homomorphism from $H$ to $K$.

A Heyting algebra $H$ is a retract of a Heyting algebra $F$ if there are homomorphisms $\iota:H\to F$ and $\pi:F\to H$ such that $\pi\circ\iota$ is the identity on $H$. We call $\pi$ a retraction.

A Heyting algebra $H$ is projective if, for any surjective homomorphism $\alpha:G\twoheadrightarrow F$ and any homomorphism $\gamma:H\to F$, there exists a homomorphism $\beta:H\to G$ such that $\alpha\circ\beta=\gamma$. A Heyting algebra is projective if and only if it is a retract of a free algebra.

Let $P$ be a poset. Fix $x\in P$. A principal filter generated by $x$ is the set of elements $p\in P$ such that $x\le p$.

A principal filter of a free Heyting algebra is a Heyting algebra. Is it projective?

A positive answer might help resolve an issue raised at the end of the paper by Raymond Balbes and Alfred Horn, ``Injective and Projective Heyting Algebras,'' Transactions of the American Mathematical Society 148 (1970), 549-559.

Improve this question
$\endgroup$
4
  • 1
    $\begingroup$ See §2 of Ghilardi, Unification in intuitionistic logic, Journal of Symbolic Logic 64 (1999), for a characterization of finitely presented projective Heyting algebras. $\endgroup$
    – Emil Jeřábek
    Commented Jun 7, 2023 at 19:13
  • $\begingroup$ @EmilJeřábek Thank you. I can't for the life of me see the connection between projective algebras and what that paper calls projective formulas, but at least I know where to look. $\endgroup$
    – Tri
    Commented Jun 8, 2023 at 22:10
  • 1
    $\begingroup$ Propositional formulas are the same as Heyting algebra terms. A finitely presented algebra $\langle\vec x\mid\phi(\vec x)=1\rangle$ is projective iff the formula $\phi$ is projective. (You don’t need more than one relation, as $\langle\vec x\mid\phi_1(\vec x)=\psi_1(\vec x),\dots,\phi_n(\vec x)=\psi_n(\vec x)\rangle$ ${}=\langle\vec x\mid((\phi_1(\vec x)\leftrightarrow\psi_1(\vec x))\land\dots\land(\phi_n(\vec x)\leftrightarrow\psi_n(\vec x)))=1\rangle$.) $\endgroup$
    – Emil Jeřábek
    Commented Jun 9, 2023 at 5:18
  • $\begingroup$ @EmilJeřábek Thank you again. $\endgroup$
    – Tri
    Commented Jun 10, 2023 at 17:43

0

Reset to default

You must log in to answer this question.