OFFSET
0,2
COMMENTS
Equivalently, size of the diagram of the fragment [&, ->]^n of IpL (i.e., the sublogic of the intuitionistic propositional logic generated by n propositional variables, conjunction, and implication; see the introduction from Renardel de Lavalette et al.) (the diagram, or Lindenbaum-Tarski algebra, of a fragment is the set of the equivalence classes of its formulae, partially ordered by the derivability relation).
It is conjectured that log(a(n+1)) ~ a(n) as n tends to infinity (see the introduction from de Bruijn).
a(4) has around 10^14 digits.
LINKS
R. Balbes, On free pseudo-complemented and relatively pseudo-complemented semi-lattices, Fundamenta Mathematicae, vol. 78, 1973, pp. 119-131.
N. G. de Bruijn, Exact finite models for minimal propositional calculus over a finite alphabet (EUT report. WSK, Dept. of Mathematics and Computing Science, vol. 75-WSK-02), Technische Hogeschool Eindhoven, 1975.
D. H. J. de Jongh, A. Hendriks, and G. R. Renardel de Lavalette, Computations in fragments of intuitionistic propositional logic, Journal of Automated Reasoning, vol. 7, 1991, pp. 537-561.
G. R. Renardel de Lavalette, A. Hendriks, and D. H. J. de Jongh, Intuitionistic implication without disjunction, Journal of Logic and Computation, vol. 22, 2010, pp. 375-404.
EXAMPLE
The 18 elements of the free implicative semilattice on 2 generators are, modulo logical equivalence: p -> p, ((q -> p) -> q) -> q, (p -> q) -> ((q -> p) -> p), ((p -> q) -> p) -> p, q -> p, (p -> q) -> q, (((q -> p) -> q) -> q) & (((p -> q) -> p) -> p), (q -> p) -> p, p -> q, (p -> q) -> p, ((p -> q) -> q) -> p, ((p -> q) -> q) & ((q -> p) -> p), ((q -> p) -> p) -> q, (q -> p) -> q, p, (p -> q) & (q -> p), q, p & q (cf. Fig. 1 from de Jongh et al. and Fig. 2 from Balbes, where the first four formulas differ).
CROSSREFS
KEYWORD
nonn
AUTHOR
Lorenzo Sauras Altuzarra, Feb 24 2026
STATUS
approved