The proof Russel gives is better though, because it captures something essential in why "0=1" and "1=2" are wrong via a natural example in sets. Meanwhile you're effectively invoking in Axiom 1 the principle of explosion, which has some intuition to it—being that since there can be no valid proofs of falsehood, we can derive anything on the basis of case analysis on the possible ways (of which there are zero) we could have derived a falsehood—but not quite as nice as what Russel shows.

Is this standard DSL for formal logic? What's it called?

If I’m understanding your question correctly, this is symbolic logic: https://en.m.wikipedia.org/wiki/List_of_logic_symbols

Not at all standard I'm afraid. "Modus ponens" is a common term to describe inferring B from A->B and A, but that's about as far as I'd be willing to say it resembles any common notation for formal logic.

Can you explain why Axiom 1 is an axiom? I don't understand this

I mostly just figured it was plausible-looking. The axiom-scheme could be "(X && !X) -> Y" for any expressions X and Y. Basically a partial definition of logical implication. The expression LHS->RHS is true when LHS is false, so it should at least be a theorem when the LHS is a contradition, and maybe an axiom depending on your taste. I suspect common taste is for small sets of axioms that don't tend to include this statement/scheme though.

Using the rules of inference from here[1], plus an assumed starting point for arithmetic, another deduction might be

1. Proposed axiom: (1==0)

2. Maybe some arithmetic axiom, humour me: !(1==0)

3. 2, negation elimination: (1==0) -> Pope(Russell)

4. 1, 3 modus ponens: Pope(Russell).

That "negation elimination" rule of inference looks kinda like what I did earlier I guess, but less questionable.

1: https://en.wikipedia.org/wiki/Propositional_calculus#Example...