I have complained that I could not find a definition of Mizar’s proof theory. I have not looked recently. It recently occurred to me that there is a strategy of improving mathematics, thru Mizar, that does not depend on any official theory thereof. Better than an official theory, several working theories.

The real Mizar asset is a growing collection of proofs written in a machinable format. There are at least informal understandings of these proofs and I can think of nothing better than several projects to produce programs to read these proofs and provide their own judgements. Some of these programs might mechanically transform some of the proofs into proofs in simpler logic systems. Such transforms would generally be expansions. Other transformations might go the other way, but that’s harder

It would be nice to know which theorems rely on the axiom of choice, the continuum hypothesis, or even the law of the excluded middle. I remember being recently terrified when I learned that AC was necessary to show that the union of a denumerable number of denumerable sets was denumerable.

As I took courses in formal logic I slowly came to believe that such logic sufficed for the math that I was otherwise interested in. Such is the inspiration behind Mizar.

Relates to: this, & this 
Robbins conjecture
+ is or
0011 x
0101 y
1100 n(x)
1101 n(x) + y
0010 n(n(x) + y)
1010 n(y)
1110 n(x) + n(y)
0001 n(n(x) + n(y))
0011 n(n(x) + y) + n(n(x) + n(y)) which is x.