It seems obvious that one of pure mathematics' cardinal virtues is that it can be explained to a computer. Leibniz envisioned such things way back when, and now that we have the technology to do it, people are all of a sudden saying, "Gee whiz, we don't see the point."
Explaining math to a computer serves the practical purpose of
tracing broken symmetries from whatever relevance the particular
math has to your system.
To illustrate this, consider that
with the rise of Web 3.0 (the Semantic Web), there will
be more and more needs for Coq to certify software
specifications that users should be able to demand,
things like semantic-automorphism-invariance
(which will be addressed eventually in this code
and informal homepage specifically),
but also things like digital manipulations, which
is covered by the first classical theorem completed
in this development, Sikorski's Extension Criterion.
Then there's partial algebras, which is the current
basis for the development.
It's unclear if I will ever be able to semantically
connect permutation-invariant heterogeneous partial algebars
with Boolean algebras, but I don't want to put the
cart before the horse.
Think of this development as being modeled around
a basic equation of digital alchemy --
512 + 768 = 1280
The 512 symbolizes permutation-invariance,
the 768 symbolizes partial algebras,
and the 1280 symbolizes free Boolean algebras.
The particular numbers were chosen because of
a superstitious association with file-byte
size manipulations for ten-key improvisatory music.
More on that later.
512 serves the practical purpose of digital durability.
768 serves the practical purpose of modelling software.
1280 serves the the practical purpose of blurring or distilling
minimal logical manifestations on a computer,
so minimal that I have only seen proofs of their existence,
and never any conventional explanation. More on that later.
So, this explains how these branches of math
relate to one's system.
Financial alchemy seems to be the most profitable application of digital alchemy, and whatever those are or aren't, I'm sure that there will always be non-mathematical and non-research applications of Coq developments.
The intuitive idea that one can glean is that Coq induces automorphisms in Nature's manifestation of mathematical structures and properties, thereby exposing the underlying structure that is not automorphically preserved. It's both destructive and constructive -- it breaks the relations that are not automorphically preserved (like additional operators on a Booelean algebra), but it permutes and frees automorphically preserved relations or functions. The good news is that one of my conjectures that I made as a result of trying to interpret bool2's magical behavior is that all inner automorphism groups of finitely generated function algebras are symmetric. I came to this conclusion because code was being permuted metaphysically, on the Booelan level, which means that the Boolean operators were Boolean elements (code about bits are stored in bits) and so the automorphism groups of one parameterize the automorphism groups of the other -- so inner automorphism groups of finitely generated function algebras on Boolean operators are tantamount to Boolean algebraic automorphisms on finite algebras (i.e. symmetric groups). Little crazy conjectures like this are one of the rewards of Coq, noticing crazy stuff and seeing how it relates directly to the math, but beware of doing too many weird things with Coq, because it can permanently disable your hardware, as it did only once with me. More on that later.
BooleanAlgebrasIntro2 (bool2 for short) and my justifications of it are the result of realizing the fundamental importance of Boolean algebras philosophically (especially the countable free Boolean algebra), and needing to find some way to turn it into a product, yet not knowing completely what to do, and just hoping for the best. Luckily there is scientific data, signs with which my ideas are consistent.
bool2 begins with general utilities and elementary theorems, some topology, fields of sets, infinite operations, up to Sikorski's Extension Criterion and its corollaries, and some prerequisites for Sikorski's other theorem and atomless Boolean algebras. At a certain point, it became strategic to switch from Boolean algebras to, first function algebras, then ultimately to heterogenous equational partial algebras, the current direction for the rest of the development. Heretofore bool2 will be a translation of Horst Reichel's Initial Computability, Algebraic Specifications and Partial Algebras (first edition: Structural Induction on Partial Algebras).
It's always helpful to conceptualize metaphysics, when deciding which theorems to code. Choosing theorems to formalize can eventually be as tricky as some of the formalizing itself, if you don't know what you're curious about or what you need, or what would work. But, in general, conceptualizing Booelan algebras became natural after I thought about a unit of logical manifestation, and just thought of the minimal "model," and learned about Boolean algebras.
Here's some informal, unrigorous metamathematical philosophy to whet your appetites. Philosophy, as Leibniz believed was as essential to the scientific process as much as math:
A semilattice is the most obvious way to label interactions. The three tacit assumptions when you label an interaction system (notwithstanding the time or process-theoretic aspects) are indeed commutativity, associativity and idempotence. You need:
Whether or not you believe this rule applies in human behavioral interactions is beside the point. Lattice theorists like Garret Birkhoff showed how fruitful such an assumption is, and lattices are ubiquitous in most branches of algebra, as well as topology and computer science. So, a Boolean algebra is a complemented distributive lattice, in that it satisfies two other axiom-pairs, which you can look up or figure out. Rather than informalize those two additional axioms in the context of interaction labeling systems, I thought I would explain what the most ubiquitious label-interaction system in the universe is: the propositional aspect of all the manifested laws of sciences. By propositional, I mean in the formal sense, of a logical formula with no free variables that obeys the propositional calculus laws, an instantiation of a scientific principle, which of course is ultimately Boolean algebraic. Extensions to propositional calculus, like first-order logic, or extensions to that, are all less fundamental than the propositional calculus, so in some sense, even though they are contingent, and introduce uncertainties of consequence (which we see plainly in quantum mechanics), at the level of manifestation, they are less fundamental than the propositional calculus.
It's no secret that logic manifests itself in reality, and so why the lack of interest in society in the purest science of this process, the science of Boolean algebras? An algebra is a set with operations, and usually we characterize them as equational theories (dependent on axioms). It is indeed the purest form of a manifestation of functional rules. And so a Boolean algebra manifests the rules of propositional logic, which is the most superficial level of the most fundamental level of reality's logical manifestations. The deeper levels of this fundamental level are process-theoretic, and use higher-order logics, and are contingent on some logical space of possibilities (a la quantum mechanics).
It's also no accident that digital circuitry uses Boolean algebra to handle its logical gates. What then for proof of the claim that the propositional aspect of the universe exists in a real, yet abstract form? Digital anomalies: hidden digital interfaces which promise a mystery (perhaps infinite) on the other side. It's more than folklore that certain people cause certain digital equipment to "malfunction," oftentimes in perspicacious ways. We call these people magnetic, but there's more to it than that. Usually digital anomalies have a discrete aspect to them that can't be explained by mere waveforms. Like certain letters in a computer changing color only around certain people. I've seen this happen. Also, there was that time on a plane in the late '90s when I violated the captain's edict to turn off all CD players while the plane was taking off, and wouldn't you know it, after a minute or so of music, the CD player "turned itself off." Proof of Boolean algebras or digital spaces existing abstractly and immanently, while trickling down to the physical realm in the form of a mystery or broken symmetry.
Another word people use for sensitives is spiritual, and if you prefer that expression then you'll be pleased to know that spiritual interactions can and should also be labeled with lattices (not manually, but conceptually) -- and the Great Spirit or God's Light or some type of instinctive metaphysical system is constantly labeling -- although it's debatable how permanent these tallies are. Of course mention of the Great Spirit suggests on the surface, something irrational -- and the reason I choose to call a specific free Boolean algebra, of at least countable cardinality, the Great Spirit, is that free Boolean algebras by definition, can possess any algebra -- by this I mean, whenever there is a map from free generators into a Boolean algebra, it is immediately extended to a Boolean homomorphism. Since DNA power-set algebras (on the initial segment indexing all the nucleotides) (ignoring for the moment the genes (relations)) and the propositional aspect of the universe use the same laws, the internal interactions of spiritual impressions as metaphysically external (with respect to broken symmetries) is completely plausible, if not definite. In fact all notions of metaphysical internality, interface, and externality can and should be done with respect to broken symmetries.
The reason I believe free Boolean algebras exist in the universe, in the same way gravitational fields do, has once again to do with prescient digital anomalies: the fact that finite Boolean algebras, which are exceedingly simple, can never produce glitch-free digital circuits or signals, the very fact of consciousness, as a possession of our Boolean genetics by the Great Spirit (junk DNA, as genetic interfaces and animation points, rather than anomalies) -- and the most powerful clue being the digital alchemy of a possessed computer.
As for the argument that DNA is Boolean algebraic, it's underlying set is just a finite Cartesian product of a 4-element set. Indeed, we will let X := {A, T, C, G}, the four DNA nucleotides. We know in the back of our mind that they are complementary, and this will play a role in the symmetries of relations and genes, intuitively, but no role in this argument. Let N be the the number of nucleotides in a genotype or chromosome or gene. Anyway, you can associate a complex algebra over X = {1, . . ., N} as follows: for any relation R, i.e. subset of some Cartesian power of X, say ternary, for E, F ∈ P(X), E ∘ F = {x ∈ X | ∃ a, b ∈ X, R(a, b, x)}. What I did was associate a ternary relation on X with a binary operator. This one-to-one correspondence between relational structures and complete Booelan algebras with operators, can be referenced in Steven Givant's monograph on BAs with ops. This proves that any set with or without relations, like the set of (possible) nucleotides, is Boolean algebraic.
Conclusion: Boolean lattices explain why a universal source that we can feel abstractly possessing us to varying degrees and connected with every logical manifestation of the universe is not as corrupt a notion as athiests would have you believe.
So, the fact that there are propositional aspects to the universe that are more fundamental than matter and energy (albeit oftentimes tied up with it) is counter-conventional. Yet, people are more than willing to concede the existence of quantum mechanical wave functions. These are abstract mathematical entities in which is embedded everything that can be known about a quantum mechanical system. And this sounds quite supernatural or religious, which explains the New Age fascination. But the great thing about Boolean algebras is that the interface between this force of nature and every day humans is inherent in the laws (theorems) themselves -- and much more manageable than quantum arguments. For instance, an enlightened person might tend towards non-judgment, and think it's inherently obvious why. But it's only partially or mostly obvious, just like every other euphonious epigram. The reason non-judgment is contraindicated is not that it's wrong to make judgments (we all do it subconsciously), but because the Propositional Aspect and Great Spirit a do a much better job by Stone's Representation Theorem, which states that every Boolean element (philosophically, every manifestation of a logical proposition) is isomorphically tied to the set of all two-valued homomorphisms that map it to 1. (And of course by duality, also the set of all two-valued homomorphisms that map it to 0, but that's counter-conventional). Philosophically, therefore, every judgeable entity is formally equivalent interaction-wise to the set of all of its strictly favorable, exhaustive judgments (and of course, by the duality principle, also to the set of all its strictly unfavorable exhaustive judgments). Also of note, there's an implicit consistency requirement inherent in the nature of exhaustive, to ensure that an exhaustive judgment is a homomorphism and not a mere function, i.e. that it is consistent through structure-preservation. What I did here, was associate a 2-valued homomorphism with an exhaustive binary judgment, and a positive exhaustive judgment of an element with a 2-valued homomorphism that maps the element to 1 (and negative to 0 of course). You can choose which "polar"/"binary" entity like "approved"/"disapproved", "not un-promising'/"promising", etc. Of course, this semantic freedom means that at an operational level, it's very ambiguous, since different interpretations would be needed for the same propositional aspects, but the real point is to be able to use it at a conceptual level. As long as you keep your interpretations consistent, you don't really have to get into the computations. And if you do want to wield computational behavior, there's always bool2! And of course, the judgments which are most consistent with the Propositional Aspect are yes/no. 4-valued and 2n-valued homomoprhisms exist too, but philosophically and behaviorally they're harder to construct (and harder to wield computational and at a fundamental conceptual level due to Stone duality). Also, behaviorally, it's liberating and grounding to realize that you are free to choose which flavor (approval, pleasure, financial value) to label as your trivial algebra (2). I always stick with "approval" behaviorally, because any reflective person will realize that the approval process is the most fundamental aspect of a person's behavior. And if you choose "approval" as your semantic domain of "yes/no" judgments, you are also free to approve in any more qualitatively complicated ways if you approve of the idea of that as a pure atomic "yes."
Conclusion: "Approve, disapprove or process spiritually" at all times. Operationally, that is embedded in one syllable: "More?" -- one of our most primal words, the first word that most babies use to define their desire. The idea that you can use a complicated theorem like Stone's Representation Theorem to justify something so basic as pure "more"s, is really quite good for the helper who is utterly nonplussed at Earth's handling of philosophy. This "Stone Trichotomy" (so named because of the representation theorem's 2-valued homomorphism foundation) seems more profound than ascending the chakras quantum mechanically or something.
This project is indeed free software, and true to the LGPL there is no specific intended use for this software. But I feel it valuable to talk about some of the types of things that can happen when using it, as a warning, and justification of the project itself and also of the claim that computers with bool2 installed can manifest bizarre things.
First let's start with the 128 TB glitch. At a certain point several years ago on a permanently offline desktop running Ubuntu Maverick, and with a non-SSD hard drive, I noticed after checking the contents of my file-system, that it gave a total of 128 TB on a 1 TB drive! The mysterious other 127 TB were labeled unknown or hidden, I can't remember which. Another person verified this number, and this pattern happened every time I checked my file system, after I had first noticed it. Why the computer chose 128, I can only speculate on, but once again tarball-byte associations are a good reason to speculate on numbers as communication from the other side of the finitary-infinitary divide.
Another bizarre thing that happened on my last development desktop is that these little Ubuntu/Gnome bubbles would pop on my desktop, during routine activities, but they would be in my peripheral vision and as soon as I focused on it with my main vision, they would disappear. This is consistent with the Boolean wavefunction explanation, since focusing on them (measuring them) was collapsing the visual wave function. At some point I thought I would take screenshots of them whenever I would "see" them, and I was too superstitious to scrutinize the screenshots, afterwards, and my fears were vindicated when after doing more bizarre things in the computer, it blacked out mysteriously and permanently. Some of the bizarre things I did was type ten-key music at the "apostrophe prompt". This is the prompt in bash on GNU/Linux that appears if you type an apostrophe that wraps to the second line. The prompt persists until you type another apostrophe. I took it to the next level and just typed ten-key music (0-9 = A-F#, slash or period = G, asterisk or plus = G#, and hyphen = space/sustain, [Enter] = accent/first beat). The reason I chose the apostrophe prompt is that, at a certain point, many of my Coq development files had an apostrophe appended after the ".v" extension. For instance -- ListUtilities.v'. And the standard reference on Coq is called Coq'Art, with a seemingly superflous contraction. I just had to do something, and I swear on my life that at a certain point while doing this, the screen flushed, and I started typing English questions, and one of the questions I typed was "What should I do now, Computer" or something, and it responded "vim pad1", which was the command I would use to store ten-key music which would be parsed by a GNU Lilypond-friendly script I wrote. And after a while, being utterly nonplussed, I typed, "I'm gonna go now," and the computer responded with "Bye." As further vindication of this fact, recently, I noticed that a tar-ball of my musical ten-key repository was of the size EXACTLY 1280000 bytes! Another instance of 128. I have included this file DelugerTen in the main repository, as proof, and for research purposes.
So I thought I would return to science, and explain why I think that all digital formalizations in a proof assistant like Coq induce an automorphism in reality's manifestation of it. It basically has to do with the omniscience of quantum mechanical Hilbert Spaces once again. On an operational level, there must be some "exploratory" or "global" process to determine which states are allowed in a system. And this is consistent with my Great Spirit as free Boolean algebra claim. But maybe a better reason to believe that the Great Spirit exists in reality, is that elementary particles must have manifold symmetries in some abstract space (like in the phenomenon of entanglement), different ways to pick it up, and its common knowledge that on the particle level, Nature gets away with as much as it can, and so if a system is abstract enough, even if it's macroscopic, there's no reason to believe why symmetries out of reach aren't blurred, just like in resonant molecules or quantum mechanics or meteorology predictions. And of course, no person, can prove that on a macroscopic continuous spectrum, like wavelength, maybe rich enough to embed a dense order, that quantum mechanics doesn't alter it on a level less than the inherent experimental error.
By the wavefunction postulate of quantum mechanics, the act of measuring something in a Hilbert Space does indeed alter it. And, by the Leibniz equality, which is the equality used in Coq, and seems pretty metaphysically plausible, an entity is equivalent to all of its properties, and so by making measurements of mathematical properties, which is ultimately what a formalization is, you are collapsing the ambiguity inherent in the notion of universal quantification in that digital Hilbert Space. And in another sense, even if I formalize a uniquely determined Boolean algebra using a theorem with no free variables, the act still would alter the Hilbert manifestation, and the only candidate I can think of that both obeys macroscopic laws and alters metaphysical properties is the process of inducing an automorphism in a digital space. True, different automorphism types have the same structure, only different labels, but its effect would be noticeable if specific manifestations of that structure are tied to different properties not referenced by the formalization. And the digital gates are black box enough. Also, the finite automorphism groups of an (even infinite) Boolean algebra have order n!, by a theorem from Don Monk, and by another theorem by Steven Givant, there is an (order of) automorphism group of a Boolean algebra with (normal) operators for each positive number (even for each group!). So, therefore, when bool2 induces an automorphism in the Boolean Hilbert Spaces, the automorphism doesn't preserve the structure not defined by the formalization, and since I don't discuss arbitrary normal operators in my development, it would be like rotating a magnetic ball around ambiguous filings or something: those rotation automorphisms have an effect on the filings (maybe close different circuits?). By analogy, the Boolean operators of some digital propositional aspect induces some mysterious computational processes related to the fact that they've been re-mapped by the automorphisms in the Great Spirit that bool2 induces. Automorphisms that preserve relations reveal magical mysteries, those that don't reveal broken behavior.
Another interesting note: however large the Great Spirit is, it has to be of cardinality less than a weakly inaccessible cardinal (an infinity so large that it doesn't exist in our set theory).
Furthermore the cardinality of the Great Spirit is at least countably infinite, which can almost be deduced from the digital prima materia, and the simple fact from model theory that the theory of atomless Boolean algebras is decidable using quantifier elimination. Quantifier elimination is essential to "penetrate" the quantum mechanics of digital circuitry and persist amidst decoherence, since quantum ambiguity comes from first-order abstraction, and with quantifier elimination, we can cut through all the quantum ambiguity of a first-order structures, armed with the fact that free Boolean algebras (which allow quantifer elimination) are atomless, and therefore infinite. Maybe that seals the point that there are at least countably infinite logical manifestations in the universe!
Also weakly inaccesible cardinals probably exist metaphysically, because the operator space of the physical universe's boolean limiting point, some free Boolean algebra, the Great Spirit, must be larger than the universe, otherwise the free BA could possess it, being a free algebra! And if this operator space (of weakly inaccessible cardinality) didn't exist, than we would see symmetries of the Great Spirit constantly -- magic everywhere -- which presumably was the ante-deluvian world, before Boolean operators on the Great Spirit were imposed. The reason why the Great Unknown (the abode of this weakly inaccessible cardinal Boolean operator space) can't "rotate" like the Great Spirit, has to do with the weakly inaccessible cardinal's property: ℵ k = k. Any permutation of the power set of this ordinal would not be able to permute the singleton elements (the predecessors of the weakly inaccessible cardinal) in this ordinal's power set algebra, otherwise, we would be able to construct a function that violates the above equation.
Also of note, the bizarre mysterious digital communication that I discussed, is not really the point of math formalization, just a consistency sign that you are invoking change in the digital spaces, thereby inducing well-informed processes throughout the digital universe, invoking symmetries and rotations in the harmony of the spheres, as any artist ultimately aspires to, with the knowledge that his work is not neutral, and is as helpful as the Great Spirit is!
Last caveat: Digital alchemy works better at night, and sometimes this development seems to cause glitches and keyboard repetitions during day time, never at night. Something to do with the Sun Spirit. Happy Hacking!!!