Definition talk:Huntington Algebra

Moved discussion

The following discussion was on User talk:Prime.mover/Archive 4. Definition:Huntington Algebra had been archived to Lord_Farin's sandbox and subsequently deleted. I want to restore it because I intend to do something with it in due course. --prime mover (talk) 05:23, 6 October 2020 (UTC)

Boolean Algebras/Boolean Rings

I intend to start covering the book I've recently added (as you have noticed). Several issues demand attention:

• The likely confusion of :Category:Boolean Algebra and Category:Boolean Algebras. Suggested resolution: destroying the former and incarnating it in a different manner.

Okay, makes sense.

• Terminology "Join" and "Meet"; Definition:Join of Subgroups needs to be changed (I have indicated to come back to this; now I do so). These concepts really belong in order theory (being respectively Definition:Infimum of Set and Definition:Supremum of Set). The operations described on Definition:Boolean Algebra could be named identically, with reference, of course. Maybe it's better to simply include material on Supremum/Infimum on them being treated as binary operations. I also recall some page describing different notations for these, but couldn't locate it.

Don't agree with putting them in order theory. They have instantiations in order theory, but they are operations which are themselves abstract, and until they are concretised by applying them to order theory IMO that's how they should be treated.

• I am tempted to use $\wedge$ and $\vee$ for meet and join, resp. This seems to be the standard convention, as nobody ever seems to care about investigating boolean algebras, lattices or related concepts in logic (where this naturally conflicts with con- and disjunction). If we desire so, we can always decide to pass to $\cap$ and $\cup$ whenever necessary. The $\smile$ and $\frown$ symbols are also an option but MathJax seems to give a suboptimal rendering.

$\wedge$ and $\vee$ work for me (as long as I refrain from calling them veg and wee) - again $\cap$ and $\cup$ are concretisations of an abstract concept.

• In line with the above renaming proposal, the results like Join Distributes over Meet are in general false, and don't belong in Category:Boolean Algebras. They need to be renamed as appropriate (but Join (Boolean Algebra) is Distributive seems awkward).

Does join not distribute over meet? I thought that was one of the distinguishing features of a B.A. (or is that Huntingdon algebra?). And at this stage I am out of my immediate depth without reading up on stuff.

Before taking drastic measures (effectively destroying what's currently up - besides some peripheral ripples - is what it's going to come down to), I'd like to hear your thoughts about the matter. --Lord_Farin (talk) 18:36, 14 December 2012 (UTC)

If you need to change existing pages which have come from source works that I put up then let me know so I can then go back to those source works to check the context they have come in from and see if I need to amend anything appropriately. --prime mover (talk) 19:28, 14 December 2012 (UTC)

As to the second and fourth points, my proposed definition of "join" coincides with a binary Definition:Supremum of Set. Cf. (the always-cursed but occasionally illustrative) WP. This usage is standard in order-theoretical works (particularly lattice theory). As there is a concept of "distributive lattice" it is nontrivial to assume the distributivity laws. I'd like to conform to standard usage of the terms. --Lord_Farin (talk) 19:34, 14 December 2012 (UTC)

Okay, if that's what it is. But we still need to retain the group-theory definition of "Join" because it's out there, it's a definition. So a disambig is required. --prime mover (talk) 19:37, 14 December 2012 (UTC)

Of course; I think it will return on a place like Definition:Join of Subgroups (incidentally, the join in the lattice of subgroups of a group, as mentioned on the talk). I'll get going then. --Lord_Farin (talk) 19:39, 14 December 2012 (UTC)

The next step in this task involves the rewriting of all results in Category:Boolean Algebras and Category:Huntington Algebras. It turns out the latter definition is called "Boolean algebra" in the literature, while "Huntington algebra" is reserved for an equivalent approach using rather $\vee$ and $\neg$ as primitives rather than also including $\wedge$. There are a lot of other characterisations of a BA/HA, but those can be covered later.

I will be moving the results I don't intend to return (recognisably) to my personal graveyard User:Lord_Farin/Backup and probably there is considerable work in bringing the references to Deskins back in line. This quite massive operation will conclude the refactoring of the lattice theory section and allow me to continue covering Givant/Halmos.

As an aside, there is a growing need, coming with the new approach of multiple definitions on a page, to have theorems which involve proving things that are axiomatically true in one, but not in another definition. For example, $\neg$ in a BA may be defined as a unary operation or by an existence clause. In the former case, Complement in Huntington Algebra is Unique is trivial, while it isn't in the second. Do you have ideas on how to approach this? I have not been able to come up with entirely satisfactory paradigms; either we suffice to add proofs "This is axiom X for Definition Y of Concept Z" or we will have a difficult time aptly naming pages. OTOH these proofs may be sufficiently involved that they deserve their own page (for the arguments are sometimes of more use than only in the proof of equivalence). --Lord_Farin (talk) 18:21, 21 January 2013 (UTC)

My own attempts to come up with a usable paradigm are as yet embryonic. As you see I am fragmenting the existing results in PropLog into ever smaller and atomic pieces, with a view to being able to assemble them appropriately into "proof trees" (I'm not sure what to call it when you have axioms at the root and theorems at the nodes, whatever) for any particular axiomatic system. Naming is difficult, as you see I have been reduced to more-or-less arbitrary numbering of "versions" of a particular result.

So don't be immediately afraid of tiny results, and don't worry about not finding a good name for them, the names may evolve, and so might the compound structures which they form. --prime mover (talk) 19:20, 21 January 2013 (UTC)

The results previously stated for Huntington Algebras have now been reformulated according to Definition:Boolean Algebra. You will want to review the links to Deskins located on the pages about HAs in User:Lord_Farin/Backup and make them reappear on the appropriate page for BAs. --Lord_Farin (talk) 20:32, 22 January 2013 (UTC)

Thx - will do once I've sorted out Exponential. --prime mover (talk) 20:34, 22 January 2013 (UTC)

I am completely lost. I can see no difference between the definition of Huntington Algebra and both definitions of Boolean Algebra except for the notation used. Also, I have this on the Deskins thread: User:Lord Farin/Backup/Power Set with Union and Intersection forms Huntington Algebra but I'm disinclined to go hunting round for its equivalent in the language of Boolean algebra. --prime mover (talk) 20:53, 22 January 2013 (UTC)

I think LF might be intending to change the HA definition to something else to match a traditional definition, but ultimately, these two notions are apparently equivalent, so it's probably more a matter of history than anything else. --Dfeuer (talk) 21:49, 22 January 2013 (UTC)

Firstly, that result now resides on Power Set with Union and Intersection forms Boolean Algebra. You are right to observe that only the notation has changed so as to match current use and compatibility with the lattice theory section. Secondly, I intend to put the definition of a Huntington algebra as follows: A system $(S, \vee, \neg)$ with $\vee$ binary, $\neg$ unary, subject to $\vee$ being comm. and assoc., and the Huntington axiom:

$(H): \quad \neg \left({\neg p \vee \neg q}\right) \vee \neg \left({\neg p \vee q}\right) = p$

A Robbins algebra is obtained by interpreting $(H)$ on $\neg p$ for $p$ (and transferring one $\neg$ from right to left). BA, HA and RA are all equivalent (but the last equivalence was only shown in the 90s by computer-aided proving) but they are historically different enough to merit covering them on separate pages. Of course, this introduces the need to appropriately link them; I will get to that in due course. I hope this clarifies stuff. --Lord_Farin (talk) 22:01, 22 January 2013 (UTC)

The other results on HAs are to be found approximately identically named in Category:Boolean Algebras, should you look for them. --Lord_Farin (talk) 22:02, 22 January 2013 (UTC)

Okay, in due course, I'm up to my ears in refactoring minute results in PropLog at the moment, which is fiddlesome and I don't want to break off from it or I'll get lost. --prime mover (talk) 22:05, 22 January 2013 (UTC)