nLab Magari algebra





higher algebra

universal algebra

Algebraic theories

Algebras and modules

Higher algebras

Model category presentations

Geometry on formal duals of algebras



The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms



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,)(M,\diamond) where MM is a Boolean algebra and :MM\diamond:M\to M is an operator satisfying:

  1. =\diamond\bot=\bot and (xy)=xy\diamond (x\vee y) =\diamond x\vee \diamond y .

  2. x=(x¬x)\diamond x=\diamond (x\wedge \neg\diamond x).


Suppose that TT is a ‘Gödelian’ theory containing enough arithmetics in order to admit a formula Cons\mathsf{Cons} internalizing consistency. Cons\mathsf{Cons} induces an operator T\diamond_T on the Lindenbaum-Tarski algebra of provable equivalence classes of formulas of TT by [φ][Cons(T+φ)][\varphi]\to [\mathsf{Cons}(T+\varphi)].

Then the condition M2 for T\diamond_T can be viewed as expressing the non-provability of the consistency of the theory T=T+φT'=T+\varphi since Cons(T)\mathsf{Cons}(T') says that TT' is consistent whereas Cons(T+¬Cons(T))\mathsf{Cons}(T'+\neg\mathsf{Cons}(T')) says that T+¬Cons(T)T'+\neg\mathsf{Cons}(T') is consistent i.e. not TCons(T)T'\vdash\mathsf{Cons}(T') (For more details see Beklemishev-Gabelaia 2012).


From M1 it follows that \diamond is monotone: xyx\leq y implies xy\diamond x\leq \diamond y.

Moreover, \diamond satisfies the following transitivity property:

xx,xM.\diamond\diamond x\leq\diamond x\quad ,\forall x\in M.

To see this, consider xxx=(xx)\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=xxy=x\vee\diamond x whence sofar we have got : xy\diamond\diamond x\leq\diamond y. Now we want to show that yx\diamond y\leq\diamond x:

From M2 plus the definition of yy: y=(y¬y)=((xx)¬y)=((x¬y)(x¬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 x¬y=\diamond x\wedge\neg\diamond y=\bot since the expanded left side is a \wedge containing a factor x¬x\diamond x\wedge\neg\diamond x. Whence ((x¬y)(x¬y))=((x¬y))=(x¬y)\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 (x¬y)x\diamond(x\wedge\neg\diamond y)\leq\diamond x since x¬yxx\wedge\neg\diamond y\leq x and \diamond is monotone. Whence all in all we get yx\diamond y\leq\diamond x and we are done.



  • L. Beklemishev, D. Gabelaia, Topological interpretations of provability logic , arXiv:1210.7317 (2012). (abstract)

  • A. Macintyre, H. Simmons, Gödel’s diagonalization technique and related properties of theories , Coll. Math. 28 no.2 (1973) pp.165-180. (pdf)

Last revised on July 16, 2017 at 17:56:58. See the history of this page for a list of all contributions to it.