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.