Two countable dense boolean algebras are isomorphic

Stream: Is there code for X?

[SnO2WMaN]

Roughly stated, the following should hold:

Any two countable dense Boolean algebras are isomorphic.

Similar result is Order.iso_of_countable_dense, for linear dense order.

This theorem is required for the following corollary

Let T and U be enough rich countable theory to prove Gödel's 1st incompleteness theorem (G1), then Lindenbaum algebra of Tand U are countable dense Boolean algebras, hence isomorphic. So in the sense, they're not intresting structure. (e.g. take Peano Arithmetic and ZFC.)

We've formalized that G1 for T implies density of Lindenbaum algebra of T (Here), so immediately we'll obtain this corollary I assume.

(Tracking in FFL/Foundation#739)

[James E Hanson]

I believe the condition you're referring to as density is also commonly called atomlessness.

Both the theorem for countable dense linear orders and an analogous statement for countable atomless Boolean algebras follow from the general theory of Fraïssé limits, but I don't know if using this library would be the fastest way to prove the desired result.