So I was reading the Wikipedia page about Heyting algebra.
What does "weakest proposition" (formally) mean in Heyting algebra?
In mathematics, a Heyting algebra is a bounded lattice (with join and meet operations written ∨ and ∧ and with least element 0 and greatest element 1) equipped with a binary operation a → b of implication such that c ∧ a ≤ b is equivalent to c ≤ a → b. From a logical standpoint, A → B is by this definition the weakest proposition for which modus ponens, the inference rule A → B, A ⊢ B, is sound. Equivalently a Heyting algebra is a residuated lattice whose monoid operation a⋅b is a ∧ b; yet another definition is as a posetal cartesian closed category with all finite sums.
Here "weakest" means "highest in the partial ordering of the Heyting algebra". As a rule of thumb, a statement is called "stronger" if it implies more, and (informally) an element of a Heyting algebra implies all elements above it.
In particular this means that the set of elements of the Heyting algebra of which you want to take "the weakest" has to have a maximum element, otherwise the notion of "the weakest" does not make sense.