From Newsgroup: sci.logic
On 03/13/2015 02:47 PM, Jack Campin wrote:
knowing what to call "the hypothes(e/i)s of" the completeness
theorem depends on knowing what axioms you are proving it from
and what framework you are in -- something we don't usually
bother with because we already know what a first-order language
is.
Proving it needs some set theory, including a form of choice principle
(the Boolean Prime Ideal Theorem, at least). It is not constructively provable (unless you restrict the object language somehow).
The reason people don't ordinarily bother specifying meta-formalism
is because ZFC provides all that is needed - not because the proof
is conducted in a first order language. But weaker systems can prove
it, and there is some non-trivial reverse mathematics involved.
----------------------------------------------------------------------------- e m a i l : j a c k @ c a m p i n . m e . u k Jack Campin, 11 Third Street, Newtongrange, Midlothian EH22 4PU, Scotland mobile 07800 739 557 <http://www.campin.me.uk> Twitter: JackCampin
--- Synchronet 3.22a-Linux NewsLink 1.2