Talk:Craig's theorem

The lead para says:

Craig's theorem states that any recursively enumerable set of well-formed formulas of a first-order language is (primitively) recursively axiomatizable.

Now, this is so replete with jargon, that a general reader will not grasp why this theorem matters, or even what it's about. Mathematically, it's admirably succinct. And the jargon has appropriate wikilinks. But for a general intro, we need to at least introduce these notions right here, without sending the reader off into the wilderness, chasing the meanings of four different expressions.

If I can make time to do this, I will, but please don't wait for that to happen! yoyo (talk) 02:13, 13 July 2018 (UTC)