boolean algebras

\(\textit{Proof}~~\) \(=\) is reflexive by introduction of equality. If \(a=b\) and \(b=a,\) then \(a=b\) by conjunction elimination, so \(=\) is antisymmetric. Finally, if \(a=b\) and \(b=c,\) we can use elimination of equality to transform \(a=b\) into \(a=c\) by equality of \(b\) and \(c.\) \(\blacksquare\)

\(\textit{Proof}~~\) By applying the well-ordering principle on \(S,\) we get a binary relation \(\lt\) on \(S\) which is irreflexive, asymmetric, and transitive.
Let's define \(\le\) the binary relation on \(S\) which is simply \({\lt}\cup{=}.\) In other words, for all \(a,b\in S,\) we have \(a\le b\) if and only if either \(a\lt b\) or \(a=b:\) these are mutually exclusive conditions because of \({\lt}\text{'s}\) reflexivity.
Since both \(\lt\) and \(=\) are transitive, we have \(\le\) transitive for free from proof by cases.
As for reflexivity, since for any \(a\in S,\) we have \(a=a\) by equality introduction, we also have \(a\le b\) by disjunction introduction.
For any \(a,b\in S,\) if \(a\le b\) and \(b\le a,\) then :
- if it were the case that \(a\lt b,\) we'd have \(b\not\lt a,\) so \(a=b\) by disjunctive syllogism ;
- if \(b\lt a,\) we'd have \(a\not\lt b,\) so \(a=b\) by disjunctive syllogism ;
- if neither \(a\lt b\) nor \(b\lt a,\) then \(a=b\) by disjunctive syllogism ;
so from proof by cases, this yields \(a=b,\) which demonstrates its antisymmetry.
Finally, because of the connected property of \(\lt\) on \(S,\) we have that for all \(a,b\in S:\)
- either \(a=b,\) in which case we have \(a\le b\) by disjunction introduction,
- or \(a\lt b,\) in which case we have \(a\le b\) by disjunction introduction,
- or \(b\lt a,\) in which case we have \(b\le a\) by disjunction introduction,
so by constructive dilemma, we at least have \(a\le b\) or \(b\le a,\) which proves \(\le\) is strongly connected.
We've therefore demonstrated that \(\le\) is reflexive, antisymmetric, transitive, and strongly connected : in other words, \(\le\) is a total order. \(\blacksquare\)

\(\textit{Proof}~~\) For any \(x\in\{0,1\},\) either \(x=0\) and thus satisfies \(0\le x\le1,\) or \(x=1\) and thus satisfies \(0\le x\le1.\) Therefore, \((\{0,1\},\le)\) is a bounded poset : its top element is \(1,\) and its and bottom element is \(0.\)
For any \(x\in\{0,1,2,3\},\) either \(x=0\) and thus satisfies \(0\le x\le3,\) or \(x=1\) and thus satisfies \(0\le x\le3,\) or \(x=2\) and thus satisfies \(0\le x\le3,\) or \(x=3\) and thus satisfies \(0\le x\le3.\) Therefore, \((\{0,1,2,3\},\le)\) is a bounded poset : its top element is \(3,\) and its bottom element is \(0.\) \(\blacksquare\)

\(\textit{Proof}~~\) Let \(a\in S_1\times S_2.\) We have \(a_1\le_1a_1\) from reflexivity of \(\le_1,\) and \(a_2\le_2a_2\) from reflexivity of \(\le_2.\) Therefore, \(a\le a.\)
Let \(a,b\in S_1\times S_2\) such that \(a\le b\) and \(b\le a.\) Then, \(a_1\le_1b_1\) and \(b_1\le_1a_1,\) so \(a_1=b_1\) by antisymmetry of \(\le_1.\) As well, \(a_2\le_2b_2\) and \(b_2\le_2a_2,\) so \(a_2=b_2\) by antisymmetry of \(\le_2.\) Therefore, \(a=b.\)
Let \(a,b,c\in S_1\times S_2\) such that \(a\le b\) and \(b\le c.\) Then, \(a_1\le_1b_1\) and \(b_1\le_1c_1,\) therefore \(a_1\le_1c_1\) by transitivity of \(\le_1.\) As well, \(a_2\le_2b_2\) and \(b_2\le_2c_2,\) therefore \(a_2\le_2c_2\) by transitivity of \(\le_2.\) Therefore, \(a\le c.\) \(\blacksquare\)

\(\textit{Proof}~~\) Let \((S_1,\le_1)\) and \((S_2,\le_2)\) be two posets. Then, there exists \(\bot_1,\top_1\in S_1\) and \(\bot_2,\top_2\in S_2\) such that for all \(x\in S_1\times S_2,\) we have \(\bot_1\le_1x_1\le\top_1\) and \(\bot_2\le_2x_2\le\top_2,\) thus \((\bot_1,\bot_2)\le x\le(\top_1,\top_2).\) \(\blacksquare\)

\(\textit{Proof}~~\) Let \(\bot,\bot'\) be bottom elements of \((S,\le).\) Since \(\bot\) is bottom, we have \(\bot\le\bot'\;;\) however, \(\bot'\) is also bottom, so \(\bot'\le\bot\;;\) by antisymmetry, we conclude that \(\bot=\bot'.\)
Let \(\top,\top'\) be top elements of \((S,\le).\) Since \(\top\) is bottom, we have \(\top'\le\top\;;\) however, \(\top'\) is also bottom, so \(\top\le\top'\;;\) by antisymmetry, we conclude that \(\top=\top'.\) \(\blacksquare\)

\(\textit{Proof}~~\) Let \(a,b\in S\) which have a meet. If \(c_1\) and \(c_2\) are meets of \(a\) and \(b,\) we get \(c_1\le a\) and \(c_1\le b\) by lower bound property so \(c_1\le c_2\) by limit property, as well as \(c_2\le a\) and \(c_2\le b\) by lower bound property so \(c_2\le c_1\) by limit property ; therefore, \(c_1=c_2\) by antisymmetry.
Let \(a,b\in S\) which have a join. If \(c_1\) and \(c_2\) are joins of \(a\) and \(b,\) we get \(a\le c_1\) and \(b\le c_1\) by upper bound property so \(c_2\le c_1\) by colimit property, we get \(a\le c_2\) and \(b\le c_2\) by upper bound property so \(c_1\le c_2\) by colimit property ; therefore, \(c_1=c_2\) by antisymmetry. \(\blacksquare\)

\(\textit{Proof}~~\) Let \(a,b\in L\) such that \(a~\mathcal R_1~b.\) By upper boundedness property, we have \(a\vee b\le b.\) By colimit property, \(a\le b.\) Therefore, \(\mathcal R_1\subset{\le}.\)
Let \(a,b\in L\) such that \(a\le b.\) By upper boundness property, \(b\le a\lor b.\) Moreover, if there existed \(x\in L\) such that \(x\lt b\) and \(a\vee b=x,\) we'd have to have \(b\le x\) by upper boundedness property ; by contradiction, there exists no \(x\in L\) such that \(x\le b\) and \(a\vee b=x.\) Therefore, \(b\) is a least upper bound between \(a\) and \(b.\) Since \((L,\le)\) is a lattice, we have existence and uniqueness of least upper bounds, so \(a\vee b=b,\) i.e. \(a~\mathcal R_1~b.\)
By double inclusion, we have \(\mathcal R_1={\le}.\) \(\Box\)
Let \(a,b\in L\) such that \(a~\mathcal R_2~b.\) By lower boundedness property, we have \(a\le a\land b.\) By limit property, \(a\le b.\) Therefore, \(\mathcal R_2\subset{\le}.\)
Let \(a,b\in L\) such that \(a\le b.\) By lower boundness property, \(a\lor b\le a.\) Moreover, if there existed \(x\in L\) such that \(a\lt x\) and \(a\vee b=x,\) we'd have to have \(x\le a\) by lower boundedness property ; by contradiction, there exists no \(x\in L\) such that \(a\le x\) and \(a\vee b=x.\) Therefore, \(a\) is a greatest lower bound between \(a\) and \(b.\) Since \((L,\le)\) is a lattice, we have existence and uniqueness of greatest lower bounds, so \(a\land b=a,\) i.e. \(a~\mathcal R_2~b.\)
By double inclusion, we also have \(\mathcal R_2={\le}.\) \(\blacksquare\)

\(\textit{Proof}~~\) Let \((L_1,\land_1,\lor_1)\) and \((L_2,\land_1,\lor_2)\) be lattices, \(L=L_1\times L_2,\) maps \(\land:L\times L\to L\) and \(\lor:L\times L\to L\) such that, for all \(a,b\in L,\) we have \(a\land b=(a_1\land_1b_1,a_2\land_2b_2)\) and \(a\lor b=(a_1\lor_1b_1,a_2\lor_2b_2).\)
For all \(a,b\in L,\) we have \(a_1\land_1b_1\le_1a_1\) and \(a_1\land_1b_1\le_1b_1,\) as well as \(a_2\land_2b_2\le_2a_2\) and \(a_2\land_2b_2\le_2b_2,\) which when combined yields \(a\land b\le a\) and \(a\land b\le b,\) so \(\land\) satisfies the lower bound property.
For all \(x,a,b\in L\) such that \(x\le a\) and \(x\le b,\) we have \(x_1\le_1a_1\) and \(x_1\le_1b_1\) so \(x_1\le_1a_1\land_1b_1\) by limit property, as well as \(x_2\le_2a_2\) and \(x_2\le_2b_2\) so \(x_2\le_2a_2\land_2b_2\) by limit property, which when combined yields \(x\le a\land b.\) Thus, \(\land\) also satisfies the limit property.
For all \(a,b\in L,\) we have \(a_1\le_1a_1\lor_1b_1\) and \(b_1\le_1a_1\lor_1b_1,\) as well as \(a_2\le_2a_2\lor_2b_2\) and \(b_2\le_2a_2\lor_2b_2,\) which when combined yields \(a\lor b\) and \(b\le a\lor b,\) so \(\lor\) satisfies the upper bound property.
For all \(x,a,b\in L\) such that \(a\le x\) and \(b\le x,\) we have \(a_1\le_1x_1\) and \(b_1\le_1x_1\) so \(a_1\lor_1b_1\le_1x_1\) by colimit property, as well as \(a_2\le_2x_2\) and \(b_2\le_2x_2\) so \(a_2\land_2b_2\le_2x_2\) by colimit property, which when combined yields \(a\land b\le x.\) Thus, \(\lor\) also satisfies the colimit property. \(\blacksquare\)

\(\textit{Proof}~~\) Let \(a,b\in H.\) Since \((H,\le)\) is a toset, we either have \(a\le b\) or \(b\lt a.\) If \(a\le b,\) \(\top\land a\le a\) by lower boundedness property, thus \(\top\land a\le b\) by transitivity. For all \(x\in H,\) we have \(x\le\top\) by \(\top\) being the top element. In conclusion, \(a{\Rightarrow}b=\top.\)
Likewise, if \(b\lt a,\) we have \(b\land a\le b\) by lower bound property. If there were \(x\in H\) such that \(x\land a\le b\) and \(b\lt x,\) since \(\le\) is strongly connected, we at least have \(x\le a\) or \(a\le x.\) By proposition 2.4 and constructive dilemma, this yields having at least \(x\land a=x\) or \(x\land a=a.\) From proof by cases, we obtain \(b\lt x\land a,\) which contradicts \(x\land a\le b.\) Therefore, \(b\) is the greatest element of \(H\) whose meet with \(a\) is \(\le b,\) which proves that \(a{\Rightarrow}b=b.\)
In conclusion, \(a{\Rightarrow}b=\left\{\begin{array}{ll}\top&\text{if }a\le b\\b&\text{if }b\lt a.~\blacksquare\end{array}\right.\)

\(\textit{Proof}~~\) Let \((H_1,\le_1)\) and \((H_2,\le_2)\) be two Heyting algberas, with conditionals \({\Rightarrow}_1:H_1\times H_1\to H_1\) and \({\Rightarrow}_2:H_2\times H_2\to H_2.\) We define \((H,\le)\) as the product lattice \((H_1,\le_1)\otimes(H_2,\le_2),\) as well as \({\Rightarrow}:H\times H\to H\) such that, for all \(a,b\in H,\) we have \(a{\Rightarrow}b=(a_1{\Rightarrow_1}b_1,a_2{\Rightarrow_2}b_2).\)
Let \(a,b\in H.\) By modus ponens, \((a_1{\Rightarrow}b_1)\land_1a_1\le_1b_1\) and \((a_2{\Rightarrow}b_2)\land_2a_2\le_2b_2,\) which sums up to \((a{\Rightarrow}b)\land a\le b.\) Therefore, \(\Rightarrow\) follows the modus ponens property.
Let \(x,a,b\in H\) such that \(x\land a\le b.\) Then, \(x_1\land_1a_1\le_1b_1\) so \(x_1\le_1a_1{\Rightarrow_1}b_1\) by limit property, and \(x_2\land_2a_2\le_2b_2\) so \(x_2\le_2a_2{\Rightarrow_2}b_2\) by limit property, therefore \(x\le a{\Rightarrow}b.\) This shows that \(\Rightarrow\) also follows the limit property, which ends our demonstration of \((H,\le)\) being Heyting. \(\blacksquare\)

\(\textit{Proof}~~\) Let \({\Rightarrow}:H\times H\to H\) and \({\Rightarrow}':H\times H\to H\) be conditionals, and \(a,b\in H.\) By modus ponens, \((a{\Rightarrow}b)\land a\le b,\) therefore \(a{\Rightarrow}b\le a{\Rightarrow}'b\) by limit property. By modus ponens, \((a{\Rightarrow}'b)\land a\le b,\) therefore \(a{\Rightarrow}'b\le a{\Rightarrow}b\) by limit property. By asymmetry, we have \(a{\Rightarrow}b=a{\Rightarrow}'b,\) which demonstrates \({\Rightarrow}={\Rightarrow}'.\) \(\blacksquare\)

\(\textit{Proof}~~\) Follows directly from property 3.2. \(\blacksquare\)

\(\textit{Proof}~~\) Let \((B_1,\le_1)\) and \((B_2,\le_2)\) be Boolean algebras, and \((B,\le)\) the product Heyting algebra \((B_1,\le_1)\otimes(B_2,\le_2).\) For all \(x\in B,\) we have \(\neg_1\neg_1x_1=x_1\) and \(\neg_2\neg_2x_2=x_2,\) so by definition, \(\neg\neg x=(\neg_1\neg_1x_1,\neg_2\neg_2x_2)=(x_1,x_2)=x.\) This proves negation is involutive in \(B,\) which demonstrates that \((B,\le)\) is Boolean.

\(\textit{Proof}~~\) Let \((B,\le)\) be a Boolean algebra. Since it is Heyting, it's also bounded, so it has at least one element, which is its top/bottom element. For all \(x\in B,\) \(x\) belongs in the image of \(\neg\) as it can be expressed as a negation, that is, \(x=\neg(\neg x),\) thanks to \(\neg\) being involutive. However, we saw in property 3.5 that, in total Heyting algebras, negation's image is \(\{\bot,\top\}\). In summary, \(\varnothing\ne B\subset\{\bot,\top\},\) hence \(0\lt|B|\le2,\) so \(|B|=1\) or \(|B|=2,\) which proves our proposition. \(\blacksquare\)

\(\textit{Proof}~~\) Let \((B,\le)\) be a Boolean algebra. By law of excluded middle, there either exists \(x\in B\) such that \(x=\neg x,\) or there doesn't. Let's assume there does. In that case, \(\neg x\land x=(x{\Rightarrow}\bot)\land x\le\bot\) by modus ponens, but since \(\bot\) is bottom, \(\neg x\land x=\bot.\) However, \(\neg x=x,\) so \(x\land x=\bot.\) By reflexivity, \(x\le x,\) so by property 2.4, \(x\land x=x.\) By transitivity of equality, \(x=\bot.\) Since \(\bot\le\bot,\) we have \(\neg\bot=\bot{\Rightarrow}\bot=\top,\) but from elimination of equality with \(x=\bot\) and \(\neg x=x,\) we obtain \(\neg\bot=\bot.\) By transitivity of equality, this yields \(\top=\bot=:0,\) therefore every \(x\in B\) is such that \(x\le0\) by top property, and \(0\le x\) by bottom property, which yields \(x=0\) by asymmetry. This shows us that \(B\subset\{0\}.\) Since \((B,\le)\) is Boolean, it's also bounded, and therefore non-empty, which yields \(B=\{0\},\) thus \(|B|=1.\)
In summary, \((\exists x\in B)(x=\neg x)\) yields \(|B|=1.\) We will henceforth suppose that \(|B|\ne1.\) By modus tollens, this will result in \((\forall x\in B)(x\ne\neg x).\) To exploit this, we will first study the family of subsets of \(B\) that is \(\mathcal F:=\{\{x,\neg x\}~|~x\in B\}.\)
Let \(p_x=\{x,\neg x\}\) and \(p_y=\{y,\neg y\}\) arbitrary elements of \(\mathcal F.\) If \(p_x\cap p_y\ne\varnothing,\) we'd have at least \(y\in p_x\) or \(\neg y\in p_x.\) In the case where \(y\in p_x,\) either \(y=x\) in which case \(\neg y=\neg x\) so \(p_x=p_y,\) or \(y=\neg x\) in which case \(\neg y=\neg\neg x=x\) by involution so \(p_x=p_y.\) In the case where \(\neg y\in p_x,\) either \(\neg y=x\) in which case \(y=\neg\neg y=\neg x\) so \(p_x=p_y,\) or \(\neg y=\neg x\) in which case \(y=\neg\neg y=\neg\neg x=x\) by involution so \(p_x=p_y.\) This shows \(p_x=p_y.\)
By contraposition, we have that, for all \(p_1,p_2\in\mathcal F,\) if \(p_1\ne p_2,\) then \(p_1\cap p_2=\varnothing.\) This means that \(\mathcal F\) is pairwise disjoint.
Let \(x\in\bigcup\mathcal F,\) then there exists \(p_x\in\mathcal F\) such that \(x\in p_x,\) but since \(p_x=\{x,\neg x\}\subset B,\) we have \(x\in B,\) which shows \(\bigcup\mathcal F\subset B.\) Let \(y\in B,\) then \(y\in\{y,\neg y\}\in\mathcal F,\) thus there exists \(p_y=\{y,\neg y\}\in\mathcal F\) such that \(y\in p_y,\) thus \(y\in\bigcup\mathcal F,\) which shows \(B\subset\bigcup\mathcal F.\) By antisymmetry of \(\subset,\) we get \(\bigcup\mathcal F=B.\)
Since \(\mathcal F\) is pairwise disjoint and \(\bigcup\mathcal F=B,\) this tells us that \(\mathcal F\) is a partition of \(B.\) This entails that \(|B|=\sum_{p\in\mathcal F}|p|.\) However, every \(p\in\mathcal F\) is such that, for some \(x_p\in B,\) we have \(p=\{x_p,\neg x_p\}.\) Since \(|B|\ne1\), we have \(x_p\ne\neg x_p.\) Therefore, \(|p|=|\{x_p,\neg x_p\}|=2,\) regardless of \(p\in\mathcal F.\) Therefore, \(|B|=\sum_{p\in\mathcal F}2=2|\mathcal F|.\) Since \((B,\le)\) is bounded, \(B\) is non-empty, therefore \(\mathcal F\) is inhabited, which entails \(|B|\) is a positive even number. \(\blacksquare\)