symmetric monoidal (∞,1)-category of spectra
basic constructions:
strong axioms
further
A diagonizable or Magari algebra is a Boolean algebra together with a modal operator internalizing the diagonalization properties involved in Gödel's second incompleteness theorem.
A Magari algebra is a pair $(M,\diamond)$ where $M$ is a Boolean algebra and $\diamond:M\to M$ is an operator satisfying:
$\diamond\bot=\bot$ and $\diamond (x\vee y) =\diamond x\vee \diamond y$ .
$\diamond x=\diamond (x\wedge \neg\diamond x)$.
Suppose that $T$ is a ‘Gödelian’ theory containing enough arithmetics in order to admit a formula $\mathsf{Cons}$ internalizing consistency. $\mathsf{Cons}$ induces an operator $\diamond_T$ on the Lindenbaum-Tarski algebra of provable equivalence classes of formulas of $T$ by $[\varphi]\to [\mathsf{Cons}(T+\varphi)]$.
Then the condition M2 for $\diamond_T$ can be viewed as expressing the non-provability of the consistency of the theory $T'=T+\varphi$ since $\mathsf{Cons}(T')$ says that $T'$ is consistent whereas $\mathsf{Cons}(T'+\neg\mathsf{Cons}(T'))$ says that $T'+\neg\mathsf{Cons}(T')$ is consistent i.e. not $T'\vdash\mathsf{Cons}(T')$ (For more details see Beklemishev-Gabelaia 2012).
From M1 it follows that $\diamond$ is monotone: $x\leq y$ implies $\diamond x\leq \diamond y$.
Moreover, $\diamond$ satisfies the following transitivity property:
To see this, consider $\diamond\diamond x\leq\diamond\diamond x\vee\diamond x=\diamond (x\vee \diamond x)$ where the last equation follows from the commutativity of $\vee$ together with M1.
Set $y=x\vee\diamond x$ whence sofar we have got : $\diamond\diamond x\leq\diamond y$. Now we want to show that $\diamond y\leq\diamond x$:
From M2 plus the definition of $y$: $\diamond y=\diamond(y\wedge\neg\diamond y)=\diamond((x\vee\diamond x)\wedge \neg\diamond y)=\diamond((x\wedge\neg\diamond y)\vee(\diamond x\wedge\neg\diamond y))$. But $\diamond x\wedge\neg\diamond y=\bot$ since the expanded left side is a $\wedge$ containing a factor $\diamond x\wedge\neg\diamond x$. Whence $\diamond((x\wedge\neg\diamond y)\vee(\diamond x\wedge\neg\diamond y))=\diamond((x\wedge\neg\diamond y)\vee\bot)=\diamond(x\wedge\neg\diamond y)$ but $\diamond(x\wedge\neg\diamond y)\leq\diamond x$ since $x\wedge\neg\diamond y\leq x$ and $\diamond$ is monotone. Whence all in all we get $\diamond y\leq\diamond x$ and we are done.