Let $\phi$ denote the statement "There is no proof of $\phi$". Is it possible to prove $\phi$? I'm assuming that this is a paradox, as any attempt to show that a proof of the statement exists would be a contradiction, but agreement that no proof exists is itself acceptance that a proof exists.
Is there anything that could be added to my reasoning here?
 A: A proof presupposes an axiom system. The statement "There is no proof of me" is too unclear to be meaningful: what is clear is a statement like, $\varphi_{ZFC}=$"There is no proof from the ZFC axioms of me" (for example).
Actually, that statement isn't really that clear. It's clear, if you believe it can be expressed in the language of ZFC! See my second bullet at the end of this answer.
Such a statement can indeed be proved - in a stronger axiom system. This is a key part of Goedel's Incompleteness Theorems: if ZFC is "reasonably nice," then ZFC can't prove $\varphi_{ZFC}$; but the theory ZFC+"ZFC is reasonably nice" can prove $\varphi_{ZFC}$. This shows, among other things, that:

If ZFC is "reasonably nice," then ZFC is incomplete.

So even though the sentence you've described looks a lot like the Liar Paradox, it's not paradoxical, and indeed can be used to prove theorems (this is a common theme in logic: paradoxes, when studied more closely, become theorems).

Now let me point out some subtleties in the above.


*

*First off, what does "reasonably nice" mean? Well, it's not hard to show that it's enough for ZFC to be consistent: if ZFC were to prove $\varphi_{ZFC}=$"There is no ZFC-proof of this statement," then ZFC would know that; so ZFC would also prove $\neg\varphi_{ZFC}$. So why did I go vague and write "reasonably nice?" Well, the mere consistency of ZFC leaves open the possibility that it disproves $\varphi_{ZFC}$ but doesn't prove it - that is, it could prove "$\varphi_{ZFC}$ is provable in ZFC" but not actually prove $\varphi_{ZFC}$. So to get the "right" behavior, we need a bit more than mere consistency - $\omega$-consistency is enough, and indeed more than we need. (Alternatively, we could replace the sentence "$\varphi_{ZFC}$" with a slightly more complicated sentence - for a theory $T$, let $\psi_T$ be the sentence "For every proof from $T$ of me, there is a shorter disproof from $T$ of me." Then Rosser showed that if ZFC is consistent, then ZFC neither proves nor disproves $\psi_T$.)

*Second, what the heck is $\varphi_{ZFC}$ (or related)? When we talk about proving a statement from some axioms, it's implicit that the statement in question is expressed in the same language as those axioms: e.g. it doesn't make sense to ask whether the axioms for groups prove that $\pi$ is irrational. But the language of ZFC is just the language of set theory, and $\varphi_{ZFC}$ doesn't seem to be about sets - first of all, it talks about sentences (or rather, proofs - but those are just sequences of sentences), and second, it refers to itself. Both of those things are weird! This is actually the meat of Goedel's proof: first, he shows how the language of set theory (actually, he proved it for the language of arithmetic, but set theory is even more powerful than arithmetic, so my statement is true) can talk about sentences and proofs, and second he shows that self-reference can arise in this context. But this is extremely non-trivial, and is really the revolutionary part of Goedel's arguments: with these facts in hand, the rest of the proof is quite easy. (In particular, there are many theories $T$ such that $\varphi_T$ is not expressible in the language of $T$!)

*Finally, going back to paradoxes in natural language: what if we switch from the Liar to the Used Car Salesman? By "USC" I mean the statement, "This statement is true." This is sort of the opposite of the Liar - we can't seem to prove anything about it! Its analogue in mathematics proper is the statement $\theta_T=$"This statement is provable in $T$", which - surprisingly - is provable in $T$! (Assuming $T$ is strong enough, that is.) This is Lob's theorem, and is really really weird - it represents a bizarre (to me at least) symmetry breaking between truth and falsity.
