While I'm fooling around with other stuff, enjoy something I learned in freenode's #math channel a few minutes ago (after the break, with names omitted)
<P> help, I'm engaged in a pointless internet argument. is there some weird logic in which a proof that X is provable is not a proof of X?
<A> P: well, it's true if we're being sufficiently formal
<A> X is a very different statement from provable(X), and a proof of one is a different thing from a proof of the other
<P> true. I'm asking about provable(X) => X
<A> there are consistent extensions of PA that prove provable(FALSE), but do not prove FALSE
<P> ok
<A> that's just incompleteness
<s> P: holy shit that's a trippy question, lol
<t> A: Got any links/books I should look at if I want to follow up on those extensions of PA?
<A> t: anything about Godel's second incompleteness theorem
<A> which is (a generalization of) the statement that the theory PA + "PA proves FALSE" is consistent
<t> Ohhh
<t> Wow. That is trippy.
<A> for added fun, throw in Godel's completeness theorem and conclude that this theory has models. I.e. models of PA which actually contain objects which "are" proofs of FALSE
<A> they're infinitely long ill-founded pseudoproofs, but still
<A> first-order PA is too weak to realize this
No comments:
Post a Comment