The motivation of your interest in finding the proof of the general first incompleteness theorem which does not 'naturally' (whatever you mean by that) imply the non-existence of finitely axiomatizable extensions of PA is unclear to me. For I would not overestimate the significance of the later (as long as you do not restrict yourself to the language of PA only, which seems unnecessarily restrictive to me). For if just one new unary predicate symbol is added to the language of PA, then the finitely axiomatized conservative extension of PA can already be constructed. This follows from the general result of Craig and Vaught extended from the one of Kleene. You can find the details and references herehere.
Martin Sleziak
- 4.7k
- 4
- 35
- 40