[FOM] some new results about intuitionistic propositional logic

[Michael O'Connor]

Hello everyone,

I'd like to announce two preprints that might be of interest to
readers of this list.

In the first, available at
http://www.arxiv.org/abs/math.LO/0702651
I show that there is a translation of intuitionistic propositional
logic in countably infinitely many variables into intuitionistic
propositional logic in two variables.  This follows from some more
general facts about free Heyting algebras.

In the second, available at
http://www.arxiv.org/abs/math.LO/0702675
I give an order-theoretic characterization of the free Heyting algebra
on countably many generators (which is the same as the Lindenbaum
algebra for intuitionistic propositional logic in countably many
variables) as a Fraisse limit.  Some results about automorphisms and
embeddings immediately follow.

Below the main theorem from the second preprint is stated, but it
requires some definitions:

Definitions: A quasisemilattice (qsl) is a poset P such that for any
two elements p and q, the set {r\in P : r <= p, r <= q} of lower
bounds of p and q has only finitely many maximal elements and such
that every lower bound of p and q is below at least one such maximal
element.

A qsl is called bounded (a bqsl) if it has a minimum element.

A qsl is called locally finite if it is locally finite under the
relation R(p,q,r) which holds iff r is a maximal lower bound of p and
q.

 A bqsl embedding between two bqsls Q_1 and Q_2 is an order-embedding
that respects the minimal element and respects, for each pair of
elements p, q in Q_1 the number and identity of the maximal elements
of {r\in Q_1 : r <= p, r <= q}.

A qsl is universal countable bounded locally finite if it is
countable, bounded, and locally finite, and embeds all countable,
bounded, locally finite qsls.

By a standard Fraisse argument, there is a unique universal countable
homogeneous locally finite bounded quasisemilattice.  Let it be Q. Let
Q' be Q with a maximum element added and the minimum element removed.

Theorem: The poset of join-irreducibles in the free Heyting algebra on
countably infinitely many generators is isomorphic to Q'

As a sample corollary, given any finite set S of pairwise-incomparable
join-irreducible elements and any permutation of S, there is an
automorphism of the whole Heyting algebra extending the chosen
permutation.

Michael O'Connor
Grad student, Dept. of Math., Cornell University