2 ms·
The double-negation holds in propositional logic (law of the excluded middle) but definitely not in constructive logic: You don't get that for free, you need a
by PeterWhittaker 12y ago
The double-negation holds in propositional logic (law of the excluded middle) but definitely not in constructive logic: You don't get that for free, you need a path from ~A to ~~A to A.
(And, refining the logical system to include bounds due to computational complexity, you need a path that is realistic in finite time.)
It also doesn't apply in Hegelian logic: ~A is literally everything that isn't A - and negating is likely undefined, since there is nothing in the universe that makes it necessary (regardless of sufficiency) for ~EverythingElse to necessarily mean that anything is left over, let along something as specific as A.
Unless A is somehow unspecific, in which case even ~A is likely defined and potentially meaningless.
I think the two worst intellectual holdovers in Western thought are Aristotelianism - and especially the law of the excluded middle - and Descartes' broader thinking - and especially his duality and "Cogito Ergo Sum": Both were really useful as developments in epistemology and logic, but both have outlived their then-value. We have moved on.
They are not even particularly useful as logical pablum for children, because it is too easy to assume forever that they are 100% reliable and valid - they are useful rules of thumb, they apply in many common, real world cases, but they are, logically, nothing more than extremely useful heuristics.
One can build vast systems with them, but one eventually hits Gödel and Aaronson, e.g., and one realizes the systems are built on less than sand.
Once one gets past them, one can begin to grok where mathematics and physics are now. But they are hard to break away from.
- cottonseed 12y agoI'm a mathematician. I can't understand your post at all. > The double-negation holds in propositional logic Double-negation isn't a proposition, so don't know what this means. Double-negation elimination, that is, the proposition: for all A, ~ (~ A) -> A does not hold in constructive logic. However, double-negation introduction, that is, the proposition: for all A, A -> ~(~ A) does definitely hold in constructive logic. Here is a proof in Coq: Theorem A_implies_not_not_A : forall A : Prop, A -> ~ (~ A). unfold not. intros. apply (H0 H). Qed.