2 ms·
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 logica
by repsilat 6y ago
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_2._Natural_deduction_system https://en.wikipedia.org/wiki/Propositional_calculus#Example...