Replies

• 

  Lain(e/o/a) Taffin Altmanpthariensflame@treehouse.systems

  Aug 11, 2023, 9:27 AM

  The final axiom is thankfully much more intuitive. It’s a kind of double-exchange rule, letting us swap between inner and outer sides when the nesting is in the center:

  a ⟪ (b ⟪ c ⟫ d) ⟫ e = b ⟪ (a ⟪ c ⟫ e) ⟫ d

  💬 1🔄 0⭐ 0
• 

  Lain(e/o/a) Taffin Altmanpthariensflame@treehouse.systems

  Aug 11, 2023, 9:27 AM

  There’s an optional additional axiom, which further constrains our structure.

  a ⟪ b ⟫ c = c ⟪ b ⟫ a

  We won’t assume it by default but some instances of the structure usefully satisfy it. I’ll call it the reversibility axiom, and say that our structure is reversible if it satisfies it.

  💬 1🔄 0⭐ 0
• 

  Lain(e/o/a) Taffin Altmanpthariensflame@treehouse.systems

  Aug 11, 2023, 9:27 AM

  Here you should pause and contemplate this structure! What is it, exactly? How does it behave? What intuition can you gain for these axioms and how they interact?

  Here are some theorems I’ve proven about this structure, without commentary; see if you can prove them too:

  ● ⟪ a ⟫ (● ⟪ b ⟫ c) = ● ⟪ (● ⟪ a ⟫ b) ⟫ c

  ● ⟪ a ⟫ (b ⟪ c ⟫ d) = ● ⟪ c ⟫ (b ⟪ a ⟫ d)

  ● ⟪ a ⟫ (b ⟪ ⬥ ⟫ c) = b ⟪ a ⟫ c

  When you feel like you have a decent grasp of how this structure operates, proceed!

  💬 1🔄 0⭐ 0
• 

  Lain(e/o/a) Taffin Altmanpthariensflame@treehouse.systems

  Aug 11, 2023, 9:27 AM

  Surprise! This structure is completely isomorphic to the standard notion of a ring. Making the structure reversible gets us a commutative ring.

  As partial proof, here is the conversion from our structure to the typical notation:

  a + b = ● ⟪ a ⟫ b

  a - b = ▪︎ ⟪ a ⟫ b

  -a = ▪︎ ⟪ ⬥ ⟫ a

  a • b = a ⟪ ⬥ ⟫ b

  0 = ⬥

  1 = ●

  And here is the conversion in the other direction:

  ▪︎ = -1

  a ⟪ b ⟫ c = (a • c) + b

  The successor operation from the very beginning is just adding one!

  The proofs of the axioms in each direction are left as exercises for the reader…

  💬 1🔄 0⭐ 0
• 

  Lain(e/o/a) Taffin Altmanpthariensflame@treehouse.systems

  Aug 11, 2023, 9:27 AM

  …or you can inspect the Agda file I’ve linked here, which contains all of the above and more formalized and computer-checked! (Note that the notation is slightly different in the code; I use -𝟷# instead of ▪︎ and 𝚏𝚖𝚊 𝚊 𝚋 𝚌 instead of a ⟪ c ⟫ b.)

  https://gist.github.com/pthariensflame/4063a4ecfd6db8e7e744dae5b9cdeb3b

  💬 1🔄 0⭐ 0
• 

  Lain(e/o/a) Taffin Altmanpthariensflame@treehouse.systems

  Aug 11, 2023, 9:39 AM

  As a bonus (not formalized in the linked file), think about what the ring of n×n square matrices with elements taken from a given ring looks like when both the element ring and the matrix ring are represented this way! What is negative one for matrices? What is our ternary operator? (Hint: you can express it with just the ternary operator on the element ring, and don’t need any of our specific values.)

  💬 1🔄 0⭐ 0
• 

  Lain(e/o/a) Taffin Altmanpthariensflame@treehouse.systems

  Aug 12, 2023, 12:40 AM

  So I decided to give these structures a name, despite being “just” rings by a different characterization, because that difference puts them in a new conceptual hierarchy of mathematical objects that just so happens to coincide with rings at that point. I call one of these things a “fumula” (/ˈfju.mju.lə/, FYOO-myoo-luh), after FUsed MULtiply-Add.

  💬 1🔄 0⭐ 0
• 

  Lain(e/o/a) Taffin Altmanpthariensflame@treehouse.systems

  Aug 12, 2023, 12:40 AM

  One reason I wanted to give them a name is because there’s a further structure I call a “fupomula” (/fju.ˈpɔu.mju.lə/, fyoo-POH-myoo-luh), after FUsed POwer-MULtiply-Add. As the naming suggests, this is a structure with a specified element (intended as -1) and a tetrary operator (intended as (aᵇ • c) + d), along with a predicate that calls certain elements “purely negative” and an allowance that the tetrary operator is undefined when a = 0 and b is purely negative.

  From here we construct a successor function similarly to a fumula, by filling in a = b = c = -1, and define 0 as the successor of -1 and 1 as the successor of 0 just as before.

  We then need axioms that say -1 and 0 are purely negative and 1 isn’t, and some generalization of the fumula axioms to account for the additional power input, plus probably a few more axioms to handle pure negativity and the power input more generally.

  💬 1🔄 0⭐ 0
• 

  Lain(e/o/a) Taffin Altmanpthariensflame@treehouse.systems

  Aug 12, 2023, 12:40 AM

  So what does this get us? Well, we can take reciprocals by setting the power to -1, so we have arbitrary division and thus arbitrary rationals. But that means we can take rational powers, so we have all algebraic numbers. And moreover we can take rational powers of -1 too, so we have all complex roots of unity! I’m not entirely sure what structure this gets us (it’s a skew field with all exponents that don’t imply a division by 0, but I’m not aware of a specific name for that).

  That feels specifically weird enough to me to give the higher members of this hierarchy new names. (The member below fumulas should just be the usual characterization of Abelian groups, I think.)

  💬 0🔄 0⭐ 0