newsBooleanAlgebrasIntro2 - News: The big picture in bool2

 
 
Latest News
Ataboy posted by deluger, Mon 16 Jan 2023 04:13:59 AM UTC
Sneak Peak: Trees b y Serre posted by deluger, Mon 26 Dec 2022 10:44:49 PM UTC
Back from the dead! posted by deluger, Fri 23 Dec 2022 06:40:21 AM UTC
This project is semi-permanently retired posted by deluger, Mon 30 May 2022 04:07:09 PM UTC
Atomizer or What's a Guy Gotta Do To Get paid around heres! posted by deluger, Tue 15 Mar 2022 04:24:35 AM UTC

The big picture in bool2

Item posted by Daniel Wyckoff <deluger> on Fri 30 Mar 2018 01:45:41 AM UTC.

So, the big news with bool2, my humble, yet, ambitious Coq formalization of Boolean algebras, is that I will soon complement it with some computational group theory in GAP, in the directory http://cvs.savannah.nongnu.org/viewvc/bool2/bool2/bestfo/
.
Bestfo is short for "best focus" or "best first order" and will compute a sort of ideal way to manage a certain pivotal setwise stabilizer condition, which is detailed in
the LaTeX file goodaut.tex at http://web.cvs.savannah.nongnu.org/viewvc/bool2/bool2/theory/

That file is very incomplete and sloppy and all over the place, but gets right a few definitions and properties.
The new portion that I'm excited about beginning in GAP, bestfo, will in contrast to bool2, be real executable code for finite Boolean algebras with operators, and their automorphism groups.  My hopes is that this will bridge a computational gap between Boolean algebras with operators and 2-modular representation theory of the symmetric group, and more.
The Coq development itself is more geared towards eccentric system researchers and digital alchemists, but the computational group theory will be more universal, hopefully, modeling some of the mystery of bool2,in the form of calculations of the group action of a symmetric group on, not only the atoms of a finite Boolean algebra, but on a finite set of normal Boolean operators, and computing setwise and pointwise stabilizers in a sort of game algorithm, which I am in the process of working out, and which I've begun delineating in goodaut.tex above.  T
The hopes is that the GAP companion bestfo, will not only serve me with some variety, but get more people interested in finite computational Boolean algebra with operators, even ultimately in its connection with finite model theory. (A relational structure is conceptually the same as a Boolean Algebra with operators).

Regarding bool2 proper, I'm planning on persisting with it through free algebreas and hopefully Stone's Representation Theorem, which is one of the most underrated theorems of all time.  And essential for intellectual sensitives.

 

Back to the top

Powered by Savane 3.13-f8d8.
Corresponding source code