All of AustinLorenz's Comments + Replies

I finally had time to read this, and I must say, that's an extremely creative premise. I'm puzzled by the proof of theorem 3.1, however. It claims "By inspection of FairBot, PA⊢◻(FB(FB) = C)-->FB(FB=C)."

However, by inspection of fairbot, the antecedent of the conditional should be FB(FB) = C rather than ◻(FB(FB) = C). The code says "if it's a theorem of PA that X cooperates with me, then cooperate." It doesn't say "if it's a theorem of PA that it's provable in PA that X cooperates with me, then cooperate." So I don't believe you can appeal to Lob's theorem in this case. .

I'm not sure if this post is obsolete, but it was linked to by a recent post, so I will provide feedback.

The translation to the formal version goes from "if a theory T has a short proof that any proof of T's inconsistency must be long, then T is inconsistent" to "if T proves in n symbols that 'T can't prove a falsehood in f(n) symbols", then T is inconsistent.'"

But inconsistency is not the same as proving a falsehood. Assuming that PA is consistent, the theory PA+~Con(PA) is consistent, since PA cannot prove its own consistency, b... (read more)

Actually, "not proving a falsehood" is not the same as being consistent; assuming that PA is consistent, the theory PA+~Con(PA) is also consistent, but proves the false statement ~Con(PA). Consistency is the weaker condition of not proving both a formula and its negation.