/sci/ - Science & Math

>>11060256
>getting in the way
There's logics that don't have LEM but still have explosion, e.g. intuition logic.
If you drop explosion, you get Minimal logic
which is actually weaker than classical/intuitionist logic.
https://en.wikipedia.org/wiki/Minimal_logic

>>11060619
That's just one example. LEM says that it holds for all proposition.
For one type of interesting proposition, the Mortal Matrix problem shows that it's undecidable, if you're given any two 15x15 matrices A and B, whether they can be multiplied in some way (possibly with repetition, e.g. as AABBABBAAABB), such that they yield the zero matrix. There's provably no algorithm that would correctly work for all matrices, to decide whether it's true that they can be multiplied to zero or not.
https://en.wikipedia.org/wiki/List_of_undecidable_problems#Problems_about_matrices
If you now say that LEM holds, you make the claim about some propositions (those involving some of the matrices where it's not possible). You make a statement that's inaccessible to any human proof system.
But the computationally undecidably variant of proposition is only one point of criticism that relates to it.

E.g. >>11060144 says
>Give me any formal system. Anyone and I can give you an equivalent one with LEM.
But that's not the case. There's axiom systems (say that axioms are "a","b","c") such that if you also adopt "lem", then some particular axiom "d" would make the system inconsistent (i.e. "a","b","c", "d", "lem" is an inconsistent system), while at the same time, the system given by the four axioms "a","b","c", "d" is an interesting theory. That is to say, adopting "lem" means you restrict the range of theories you can work with. E.g.
https://en.wikipedia.org/wiki/Synthetic_differential_geometry

Meanwhile, "lem" doesn't help you prove more, from a classical interpretation.

>>11060105
No, Topos theory just don't necessitate hard compliments, but see
https://ncatlab.org/nlab/show/Boolean+category