I will augment François Dorais’s answer with an exact identification of the propositional logic.

Let $D_n$ be the free distributive lattice with a top, considered as a finite Heyting algebra. Algebras are a nuisance to work with, so let us compute the dual Kripke frame $F_n$, which validates the same formulas, but is much smaller and simpler. Since we are dealing with a finite algebra, the elements of $F_n$ are just the $\lor$-irreducible (which entails $\bot$-irreducible, i.e., nonzero) elements of $D_n$, ordered upside down.

If $\{x_i:i\in[n]\}$ is the set of free generators, each element of $D_n$ can be written in a disjunctive normal form
$$a=\bigvee_{i\in I}\bigwedge_{j\in J_i}x_j,$$
where $J_i\subseteq[n]$, $I\ne\varnothing$, and $\{J_i:i\in I\}$ is an antichain. Clearly, if $a$ is $\lor$-irreducible, we must have $|I|=1$, thus $a$ is of the form
$$a_J=\bigwedge_{j\in J}x_j$$
for some $J\subseteq[n]$. Moreover, we must have $J\ne[n]$ so that $a_J\ne\bot$. Conversely, it is not difficult to check that all $a_J$ with $J\ne[n]$ are indeed $\lor$-irreducible. Since
$$a_J\le a_{J'}\iff J\supseteq J',$$
$F_n$ is just the powerset Boolean algebra without top:
$$F_n\simeq\langle\mathcal P([n])\smallsetminus\{[n]\},{\subseteq}\rangle.$$
These Kripke frames are known as *Medvedev frames*, and the logic defined by $\{F_n:n\in\mathbb N\}$ is *Medvedev’s logic* (aka *logic of finite problems*), denoted LM or ML, based on Medvedev [1]. See e.g. Chagrov&Zakharyaschev [2,§2.9]. Thus, the logic of $\{D_n:n\in\mathbb N\}$ is also Medvedev’s logic.

Despite its seemingly simple definition, this logic is shrouded in mystery: it is particularly scandalous that half a century after its discovery, it is still an open problem if the logic is recursively axiomatizable. Let me just mention that apart from the Kreisel–Putnam axiom
$$(\neg p\to q\lor r)\to(\neg p\to q)\lor(\neg p\to r),$$
Medvedev’s logic is also known to include Scott’s axiom
$$((\neg\neg p\to p)\to p\lor\neg p)\to\neg\neg p\lor\neg p,$$
and an axiom identified by Andrews (reported in Gabbay [3]), which in fact implies both the Kreisel–Putnam and Scott axioms:
$$((\neg p\to q)\to r\lor s)\to(p\to r)\lor(q\to s).$$
On the other hand, Medvedev’s logic is included in the logic of weak excluded middle $\mathrm{KC}=\mathrm{IPC}+(\neg p\lor\neg\neg p)$.

Medvedev’s logic has many interesting properties. In particular, it is the largest logic with the disjunction property that extends Kreisel–Putnam logic (Levin [4], Maksimova [5], cf. [2,Thm. 15.18]), and it is the only known superintuitionistic logic that simultaneously has the disjunction property and is structurally complete (Prucnal [6,7]).

**References:**

[1] Yuriĭ T. Medvedev: *Finite problems*. Doklady Akademii Nauk SSSR 142 (1962), no. 5, pp. 1015–1018, http://mi.mathnet.ru/eng/dan26117 (in Russian). English translation: Soviet Mathematics, Doklady 3 (1962), pp. 227–230.

[2] Alexander Chagrov and Michael Zakharyaschev: *Modal logic*. Oxford Logic Guides vol. 35, Oxford University Press, 1997.

[3] Dov Gabbay: *Semantical investigations in Heyting’s intuitionistic logic*. Synthese Library vol. 148, Springer, 1981, doi: 10.1007/978-94-017-2977-2.

[4] Leonid A. Levin: *Some syntactic theorems on the calculus of finite problems of Yu. T. Medvedev*. Doklady Akademii Nauk SSSR 185 (1969), no. 1, pp. 32–33, http://mi.mathnet.ru/eng/dan34473 (in Russian). English translation: Soviet Mathematics, Doklady 10 (1969), 288–290.

[5] Larisa L. Maksimova: *On maximal intermediate logics with the disjunction property*. Studia Logica 45 (1986), no. 1, pp. 69–75, doi: BF01881550.

[6] Tadeusz Prucnal: *Structural completeness of Medvedev’s propositional calculus*. Reports on Mathematical Logic 6 (1976), pp. 103–105.

[7] Tadeusz Prucnal: *On two problems of Harvey Friedman*. Studia Logica 38 (1979), no. 3, pp. 247–262, doi: 10.1007/BF00405383.

1more comment