Answer by Dan Doel for Is "all categorical reasoning formally contradictory"?

2010-05-05T20:08:42Z

With regard to what Darij said, if Haskell is viewed as a formal system, it's quite easy to derive contradictions; they correspond to infinite loops:

loop :: forall a. a
loop = loop

However, when viewed in this light, the quote becomes something like:

Nowadays, one of the most interesting things in computer programming is that, although most languages allow one to write infinite loops, most programs that people write aren't infinite loops.

But this isn't surprising at all, because most people construct programs with some productive activity in mind, rather than just spinning in a vicious loop. And similarly, most mathematicians presumably choose theorems and proofs that they find to be similarly productive, rather than a masquerading paradox, even if the formal system would allow the latter. Just because the formal system allows paradox doesn't mean that there aren't non-paradoxical ways to prove things in the system, or that most proofs people write wouldn't be the latter.

Now, one might say, "people do write infinite loops." And this is true. But, the analogy with Haskell breaks down a bit at that point, because Haskell makes it easy to write infinite loops. It's just a given in the language, like mine above. With inconsistent formal systems, it's typically not as easy to get a proof of false. People did a lot of naive set theory without noticing that you could do it for instance. Russel's paradox is probably the easiest of the bunch, but it's quite easy to break it. For instance, you could have a naive set theory with more typing restrictions, such that propositions like x ∉ x aren't well-formed. It will still be inconsistent, but you'll have to do more work to construct a paradox. As another example, a type theory with Type : Type (that is, there's a type of all types) is inconsistent, but proving false is a lot of work.

So, to posit a reason for why people never make mistakes with their categorical proofs, despite it being a possibility given that people typically work in a naive system: it may well be much harder to construct circular proofs (in category theory) for most theorems that people are interested in than it is to write good proofs. For one, it might be hard to prove false. For two, proving false and then inferring whatever you want is obviously bad, so the paradoxical logic would have to be disguised as a legitimate argument. And that's unlikely to be the sort of reasoning a mathematician has in mind to prove things that aren't fairly related to paradoxes.

Comment by Dan Doel

2010-08-14T08:27:54Z

I think I agree, although I'm certainly no expert. It seems like the Turing machines get metatheoretic gifts (the oracles) that ZFC does not, and the latter has no way of gaining the same (if it even could) due to the restrictions. To be comparable, shouldn't we consider $ZFC_0$ to be the usual ZFC axioms, and then talk about the metatheoretic $g_0(n)$ being defined similar to $z(n)$ above? Then we can talk about $ZFC_1$ being $ZFC_0$ augmented with $g_0(n)$, which is allowed to be used in the formulas we will use to define $g_1(n)$. And so on, with ordinals and whatnot.

User dan doel - MathOverflow

Answer by Dan Doel for Is "all categorical reasoning formally contradictory"?

Comment by Dan Doel