Replies

• 

  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