Hacker News Reader

I love the fact that it's interactive. Wish more articles were written that way. It was also relatively easy for me to follow up till "Consistency":

> But what if theorems() contains both coll_conj and ¬coll_conj? Is that possible?

> ...

> But in general, a formal system can have both S and ¬S as theorems.

Is there an intuitive explanation for this?

View on HN

Formal systems need not be consistent; if a formal system assumes both P and ~P as axioms, you can derive S and ~S (for any S) by explosion.

Is the problem that you can't proof consistency? Because if it's consistent then shouldn't either P or ~P be true or the axiom doesn't exist?

It is possible to prove consistency but to do so requires using a more powerful system of axioms which in turn might be inconsistent. What Goedel showed is that in any system that can encode arithmetic (and consequently some notion of computation, e.g. lambda calculus) can not be complete if it is consistent.

Ah, thank you, that makes more sense. Maybe a weird follow-up question: Is it possible (or does it make sense) to find a proof in an inconsistent system and to try to "transform" it into a consistent one?

Yes, paraconsistent logic could be considered an instance of such a system: https://en.wikipedia.org/wiki/Paraconsistent_logic.

Reply on news.ycombinator.com