Hacker News new | comments | ask | show | jobs | submit login
Set Theory and Axiomatic Systems (0a.io)
30 points by archibaldJ on Feb 19, 2015 | hide | past | web | favorite | 9 comments

Interesting that the first axiom he highlights is considered rather controversial. I only have a layman's understanding, but my sense is that the answer to "(If A is true) Do you believe not-not-A is true?" points to whether you subscribe more to classical logic or intuitionist/constructive logic.

It's double-negative elimination that does hold constructively, namely, not-not-A => A. In both classical and constructive logic, A implies not-not-A.

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.

I'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.

... had to think about it, but that makes sense. It usually helps me to think of "provable" instead of "true".

So, not-not-provable doesn't necessarily imply provable (since it could just be an open question). But, provable does imply not-not-provable (since by definition it isn't unprovable).

So, I should have said, "do you believe not-not-A implies A?" without the initial assumption that A is true (which, ironically, I added later in a comment edit thinking I was adding clarity...)

FWIW, I believe you intended to say "It's double-negative elimination that doesN'T hold constructively...".

(Which is correct, and what I was about to point out until I saw you already did!)

Yes, I mean't "... doesN'T hold constructively". Thanks for catching that! Too late to edit the post.

A small error I noticed:

After explaining the difference between subset and strict_subset, they claim that for all A

empty_set strict_subset A

which obviously fails when A is itself empty.

Nice! I was just waiting for someone to point it out.

Applications are open for YC Summer 2019

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact