A peculiarity of Henkin's 1950 proof of completeness for higher order logic











up vote
12
down vote

favorite
2












My question concerns Henkin's original (1950) completeness proof https://projecteuclid.org/euclid.jsl/1183730860 for classical higher order logic and type theory relative to so-called general models.



His 1950 proof seems quite different to his (1949) completeness proof of first order logic https://projecteuclid.org/euclid.jsl/1183730666.



In particular, the 1950 completeness proof for classical type theory does not, at first sight, seem to employ the famous construction whereby the language is expanded by adjoining constants to it thereby providing witness to existential formulae, whereas his 1949 completeness proof does. (The main body of his 1950 proof is on p.85-88 of https://projecteuclid.org/euclid.jsl/1183730860, which constructs a maximally consistent set of formulae, but surprisingly does not mention constants and their role as witnesses for existential formulae)



I mentioned this to a colleague who expressed surprise/incredulity that the completeness proof for classical type theory does not employ this construction. He suggested that it might be hidden somewhere in the proof, and that perhaps the $iota$ operator employed by Henkin plays the role of supplying fresh constants with which to witness existential formulae.



Indeed, it is clear from Henkin's comments in that he views the $iota$ as playing an important role in the completeness proof, and this passage suggests he views it as a way of providing witnesses for existential formulae:






"The very first question I asked myself was whether I could use the method
that gave me completeness for type theory, to get a new proof of Godel's
completeness for first-order logic. It seemed, at first, that there was no
possibility to do so. The reason is that the axiom of choice, and in particular Church's neat formulation of it via the constants $i_{a(Oa)}$, played a crucial role in the proof for type theory, while in first order logic there is no axiom of choice, and no way to formulate one.
I decided to analyze carefully the role of the axiom of choice in the completeness proof, to see whether there was some other way of accomplishing it in first-order logic. The role that I saw first was performed in the proof by induction, sketched above, that domains $D_{alpha}^{'}$ satisfying conditions (i)-(iii), could be constructed. But when I wrote down details of the proof that the resulting hierarchy of domains $D_{alpha}^{'}$ satisfy the maximal consistent set of (added) axioms, I saw that the axiom of choice is needed there in a more general way, of which the earlier use is just a special case. The more general need is to show that whenever we have a wff $textbf{M_0}$ such that $vdash (exists x_b)M_0$, then we also have $vdash (lambda x_b. textbf{M_0 }) (iota_{b,(0b)}(lambda x_{beta}.textbf{M_{0}}))$. The fact that this condition holds is a direct consequence of having Axiom Schema $11^b$ in the deductive system that Church had set up for the theory $mathscr{T}$, as that schema is trivially equivalent to $(exists x_b f_{0b} x_b) supset f_{0b}(iota_{b(0b)} f_{0b})$...I did not altogether hide the symbols $i_{b(0b)}$ from the reader of my dissertation,
for in passing from Theorem VI to Theorem VII, in which the
generalized completeness theorem is extended to languages that can be nondenumerable or have additional constants, I cited Church's system in which the axiom schemas of description and choice are formulated with the symbols $iota{b(0b)}$, as an example. With that example is a brief note to the effect
that when this formulation of the axiom of choice is made, the adjunction of special constants $u_b, u_{b}^{'}, u_{b}^{''},...$ for each type symbol $b$ becomes unnecessary in the completeness proof, as their role can be taken over by the symbols $iota_{b(0b)}$. Still, it would be a very sharp-eyed historian who could detect in that brief note appended to Theorem VII, the origin of the proof of Theorem I!" (from http://www2.mat.ulaval.ca/fileadmin/Cours/MAT-10391/Henkin_BSL_1996.pdf)






So is my colleague right about this?



Does the 1950 proof implicitly contain the relevant construction?





$Edit$:



The mystery is made worse by the fact that Henkin in his 1949 paper writes that his proof "suggests a new approach to the problem of completeness for functional calculi of higher order" to be "taken up" in a further paper (presumably his 1950 paper). In the 1950 paper he writes (ft6, p.82) that a completeness proof of second order logic relative to general models "can be carried out along the lines of the author's recent paper" (i.e his 1949 paper). So what precisely is the link between the earlier paper and the later (presuming it is not the famous construction involving adjoining constants to the language)?










share|cite|improve this question




























    up vote
    12
    down vote

    favorite
    2












    My question concerns Henkin's original (1950) completeness proof https://projecteuclid.org/euclid.jsl/1183730860 for classical higher order logic and type theory relative to so-called general models.



    His 1950 proof seems quite different to his (1949) completeness proof of first order logic https://projecteuclid.org/euclid.jsl/1183730666.



    In particular, the 1950 completeness proof for classical type theory does not, at first sight, seem to employ the famous construction whereby the language is expanded by adjoining constants to it thereby providing witness to existential formulae, whereas his 1949 completeness proof does. (The main body of his 1950 proof is on p.85-88 of https://projecteuclid.org/euclid.jsl/1183730860, which constructs a maximally consistent set of formulae, but surprisingly does not mention constants and their role as witnesses for existential formulae)



    I mentioned this to a colleague who expressed surprise/incredulity that the completeness proof for classical type theory does not employ this construction. He suggested that it might be hidden somewhere in the proof, and that perhaps the $iota$ operator employed by Henkin plays the role of supplying fresh constants with which to witness existential formulae.



    Indeed, it is clear from Henkin's comments in that he views the $iota$ as playing an important role in the completeness proof, and this passage suggests he views it as a way of providing witnesses for existential formulae:






    "The very first question I asked myself was whether I could use the method
    that gave me completeness for type theory, to get a new proof of Godel's
    completeness for first-order logic. It seemed, at first, that there was no
    possibility to do so. The reason is that the axiom of choice, and in particular Church's neat formulation of it via the constants $i_{a(Oa)}$, played a crucial role in the proof for type theory, while in first order logic there is no axiom of choice, and no way to formulate one.
    I decided to analyze carefully the role of the axiom of choice in the completeness proof, to see whether there was some other way of accomplishing it in first-order logic. The role that I saw first was performed in the proof by induction, sketched above, that domains $D_{alpha}^{'}$ satisfying conditions (i)-(iii), could be constructed. But when I wrote down details of the proof that the resulting hierarchy of domains $D_{alpha}^{'}$ satisfy the maximal consistent set of (added) axioms, I saw that the axiom of choice is needed there in a more general way, of which the earlier use is just a special case. The more general need is to show that whenever we have a wff $textbf{M_0}$ such that $vdash (exists x_b)M_0$, then we also have $vdash (lambda x_b. textbf{M_0 }) (iota_{b,(0b)}(lambda x_{beta}.textbf{M_{0}}))$. The fact that this condition holds is a direct consequence of having Axiom Schema $11^b$ in the deductive system that Church had set up for the theory $mathscr{T}$, as that schema is trivially equivalent to $(exists x_b f_{0b} x_b) supset f_{0b}(iota_{b(0b)} f_{0b})$...I did not altogether hide the symbols $i_{b(0b)}$ from the reader of my dissertation,
    for in passing from Theorem VI to Theorem VII, in which the
    generalized completeness theorem is extended to languages that can be nondenumerable or have additional constants, I cited Church's system in which the axiom schemas of description and choice are formulated with the symbols $iota{b(0b)}$, as an example. With that example is a brief note to the effect
    that when this formulation of the axiom of choice is made, the adjunction of special constants $u_b, u_{b}^{'}, u_{b}^{''},...$ for each type symbol $b$ becomes unnecessary in the completeness proof, as their role can be taken over by the symbols $iota_{b(0b)}$. Still, it would be a very sharp-eyed historian who could detect in that brief note appended to Theorem VII, the origin of the proof of Theorem I!" (from http://www2.mat.ulaval.ca/fileadmin/Cours/MAT-10391/Henkin_BSL_1996.pdf)






    So is my colleague right about this?



    Does the 1950 proof implicitly contain the relevant construction?





    $Edit$:



    The mystery is made worse by the fact that Henkin in his 1949 paper writes that his proof "suggests a new approach to the problem of completeness for functional calculi of higher order" to be "taken up" in a further paper (presumably his 1950 paper). In the 1950 paper he writes (ft6, p.82) that a completeness proof of second order logic relative to general models "can be carried out along the lines of the author's recent paper" (i.e his 1949 paper). So what precisely is the link between the earlier paper and the later (presuming it is not the famous construction involving adjoining constants to the language)?










    share|cite|improve this question


























      up vote
      12
      down vote

      favorite
      2









      up vote
      12
      down vote

      favorite
      2






      2





      My question concerns Henkin's original (1950) completeness proof https://projecteuclid.org/euclid.jsl/1183730860 for classical higher order logic and type theory relative to so-called general models.



      His 1950 proof seems quite different to his (1949) completeness proof of first order logic https://projecteuclid.org/euclid.jsl/1183730666.



      In particular, the 1950 completeness proof for classical type theory does not, at first sight, seem to employ the famous construction whereby the language is expanded by adjoining constants to it thereby providing witness to existential formulae, whereas his 1949 completeness proof does. (The main body of his 1950 proof is on p.85-88 of https://projecteuclid.org/euclid.jsl/1183730860, which constructs a maximally consistent set of formulae, but surprisingly does not mention constants and their role as witnesses for existential formulae)



      I mentioned this to a colleague who expressed surprise/incredulity that the completeness proof for classical type theory does not employ this construction. He suggested that it might be hidden somewhere in the proof, and that perhaps the $iota$ operator employed by Henkin plays the role of supplying fresh constants with which to witness existential formulae.



      Indeed, it is clear from Henkin's comments in that he views the $iota$ as playing an important role in the completeness proof, and this passage suggests he views it as a way of providing witnesses for existential formulae:






      "The very first question I asked myself was whether I could use the method
      that gave me completeness for type theory, to get a new proof of Godel's
      completeness for first-order logic. It seemed, at first, that there was no
      possibility to do so. The reason is that the axiom of choice, and in particular Church's neat formulation of it via the constants $i_{a(Oa)}$, played a crucial role in the proof for type theory, while in first order logic there is no axiom of choice, and no way to formulate one.
      I decided to analyze carefully the role of the axiom of choice in the completeness proof, to see whether there was some other way of accomplishing it in first-order logic. The role that I saw first was performed in the proof by induction, sketched above, that domains $D_{alpha}^{'}$ satisfying conditions (i)-(iii), could be constructed. But when I wrote down details of the proof that the resulting hierarchy of domains $D_{alpha}^{'}$ satisfy the maximal consistent set of (added) axioms, I saw that the axiom of choice is needed there in a more general way, of which the earlier use is just a special case. The more general need is to show that whenever we have a wff $textbf{M_0}$ such that $vdash (exists x_b)M_0$, then we also have $vdash (lambda x_b. textbf{M_0 }) (iota_{b,(0b)}(lambda x_{beta}.textbf{M_{0}}))$. The fact that this condition holds is a direct consequence of having Axiom Schema $11^b$ in the deductive system that Church had set up for the theory $mathscr{T}$, as that schema is trivially equivalent to $(exists x_b f_{0b} x_b) supset f_{0b}(iota_{b(0b)} f_{0b})$...I did not altogether hide the symbols $i_{b(0b)}$ from the reader of my dissertation,
      for in passing from Theorem VI to Theorem VII, in which the
      generalized completeness theorem is extended to languages that can be nondenumerable or have additional constants, I cited Church's system in which the axiom schemas of description and choice are formulated with the symbols $iota{b(0b)}$, as an example. With that example is a brief note to the effect
      that when this formulation of the axiom of choice is made, the adjunction of special constants $u_b, u_{b}^{'}, u_{b}^{''},...$ for each type symbol $b$ becomes unnecessary in the completeness proof, as their role can be taken over by the symbols $iota_{b(0b)}$. Still, it would be a very sharp-eyed historian who could detect in that brief note appended to Theorem VII, the origin of the proof of Theorem I!" (from http://www2.mat.ulaval.ca/fileadmin/Cours/MAT-10391/Henkin_BSL_1996.pdf)






      So is my colleague right about this?



      Does the 1950 proof implicitly contain the relevant construction?





      $Edit$:



      The mystery is made worse by the fact that Henkin in his 1949 paper writes that his proof "suggests a new approach to the problem of completeness for functional calculi of higher order" to be "taken up" in a further paper (presumably his 1950 paper). In the 1950 paper he writes (ft6, p.82) that a completeness proof of second order logic relative to general models "can be carried out along the lines of the author's recent paper" (i.e his 1949 paper). So what precisely is the link between the earlier paper and the later (presuming it is not the famous construction involving adjoining constants to the language)?










      share|cite|improve this question















      My question concerns Henkin's original (1950) completeness proof https://projecteuclid.org/euclid.jsl/1183730860 for classical higher order logic and type theory relative to so-called general models.



      His 1950 proof seems quite different to his (1949) completeness proof of first order logic https://projecteuclid.org/euclid.jsl/1183730666.



      In particular, the 1950 completeness proof for classical type theory does not, at first sight, seem to employ the famous construction whereby the language is expanded by adjoining constants to it thereby providing witness to existential formulae, whereas his 1949 completeness proof does. (The main body of his 1950 proof is on p.85-88 of https://projecteuclid.org/euclid.jsl/1183730860, which constructs a maximally consistent set of formulae, but surprisingly does not mention constants and their role as witnesses for existential formulae)



      I mentioned this to a colleague who expressed surprise/incredulity that the completeness proof for classical type theory does not employ this construction. He suggested that it might be hidden somewhere in the proof, and that perhaps the $iota$ operator employed by Henkin plays the role of supplying fresh constants with which to witness existential formulae.



      Indeed, it is clear from Henkin's comments in that he views the $iota$ as playing an important role in the completeness proof, and this passage suggests he views it as a way of providing witnesses for existential formulae:






      "The very first question I asked myself was whether I could use the method
      that gave me completeness for type theory, to get a new proof of Godel's
      completeness for first-order logic. It seemed, at first, that there was no
      possibility to do so. The reason is that the axiom of choice, and in particular Church's neat formulation of it via the constants $i_{a(Oa)}$, played a crucial role in the proof for type theory, while in first order logic there is no axiom of choice, and no way to formulate one.
      I decided to analyze carefully the role of the axiom of choice in the completeness proof, to see whether there was some other way of accomplishing it in first-order logic. The role that I saw first was performed in the proof by induction, sketched above, that domains $D_{alpha}^{'}$ satisfying conditions (i)-(iii), could be constructed. But when I wrote down details of the proof that the resulting hierarchy of domains $D_{alpha}^{'}$ satisfy the maximal consistent set of (added) axioms, I saw that the axiom of choice is needed there in a more general way, of which the earlier use is just a special case. The more general need is to show that whenever we have a wff $textbf{M_0}$ such that $vdash (exists x_b)M_0$, then we also have $vdash (lambda x_b. textbf{M_0 }) (iota_{b,(0b)}(lambda x_{beta}.textbf{M_{0}}))$. The fact that this condition holds is a direct consequence of having Axiom Schema $11^b$ in the deductive system that Church had set up for the theory $mathscr{T}$, as that schema is trivially equivalent to $(exists x_b f_{0b} x_b) supset f_{0b}(iota_{b(0b)} f_{0b})$...I did not altogether hide the symbols $i_{b(0b)}$ from the reader of my dissertation,
      for in passing from Theorem VI to Theorem VII, in which the
      generalized completeness theorem is extended to languages that can be nondenumerable or have additional constants, I cited Church's system in which the axiom schemas of description and choice are formulated with the symbols $iota{b(0b)}$, as an example. With that example is a brief note to the effect
      that when this formulation of the axiom of choice is made, the adjunction of special constants $u_b, u_{b}^{'}, u_{b}^{''},...$ for each type symbol $b$ becomes unnecessary in the completeness proof, as their role can be taken over by the symbols $iota_{b(0b)}$. Still, it would be a very sharp-eyed historian who could detect in that brief note appended to Theorem VII, the origin of the proof of Theorem I!" (from http://www2.mat.ulaval.ca/fileadmin/Cours/MAT-10391/Henkin_BSL_1996.pdf)






      So is my colleague right about this?



      Does the 1950 proof implicitly contain the relevant construction?





      $Edit$:



      The mystery is made worse by the fact that Henkin in his 1949 paper writes that his proof "suggests a new approach to the problem of completeness for functional calculi of higher order" to be "taken up" in a further paper (presumably his 1950 paper). In the 1950 paper he writes (ft6, p.82) that a completeness proof of second order logic relative to general models "can be carried out along the lines of the author's recent paper" (i.e his 1949 paper). So what precisely is the link between the earlier paper and the later (presuming it is not the famous construction involving adjoining constants to the language)?







      lo.logic model-theory foundations type-theory






      share|cite|improve this question















      share|cite|improve this question













      share|cite|improve this question




      share|cite|improve this question








      edited Nov 23 at 15:08

























      asked Nov 23 at 10:19









      user65526

      2429




      2429






















          1 Answer
          1






          active

          oldest

          votes

















          up vote
          8
          down vote













          Henkin's completness proof for first order logic (using his method of constants) and Henkin's work on the completeness of type theory were both carried out in his doctoral 1947 dissertation written under the direction of Alonzo Church. The dissertation was never published, but Henkin wrote a fascinating and detailed article about the genesis of the intertwining ideas in his thesis in 1996 (The Discovery of My Completeness Proofs, The Bulletin of Symbolic Logic, Vol. 2, No. 2 (Jun., 1996), pp. 127-158).



          The following quote from the above paper (starting in the bottom of page 154 and continued to the next page) seems to answer your question (and vindicate your colleague). Henkin uses "cwff" for closed well-formed formulae; i.e., those with no free variables.




          As indicated, in addition to putting the first-discovered proof into Part
          III of the dissertation, I hid the discovery process in another way. Namely,
          in setting forth the formal language for type theory, in Part III, I deleted
          from Church's system the symbols $iota_b(0b)$ and the axiom of choice for which they were used! Those symbols, and that axiom, which quintessential role in the discovery process, were omitted in Theorem VI, and the role of the symbols $iota_b(0b)$ in forming "witnesses" cwffs of the form $exists x_bM_0$ was taken over by the adjunction of constants $u_b$, $u'_{b}$, $u''_{b}$ for each type symbol $b$.







          share|cite|improve this answer





















          • Just saw your comment after posting my update. So the $iota$ operator provides witnesses. Given this is not immediately obvious in the published article, why didn't he make it more clear? There is no mention at all of the construction. Can we see any precise point in the article in which he is implicitly referring to it?
            – user65526
            Nov 23 at 15:10











          Your Answer





          StackExchange.ifUsing("editor", function () {
          return StackExchange.using("mathjaxEditing", function () {
          StackExchange.MarkdownEditor.creationCallbacks.add(function (editor, postfix) {
          StackExchange.mathjaxEditing.prepareWmdForMathJax(editor, postfix, [["$", "$"], ["\\(","\\)"]]);
          });
          });
          }, "mathjax-editing");

          StackExchange.ready(function() {
          var channelOptions = {
          tags: "".split(" "),
          id: "504"
          };
          initTagRenderer("".split(" "), "".split(" "), channelOptions);

          StackExchange.using("externalEditor", function() {
          // Have to fire editor after snippets, if snippets enabled
          if (StackExchange.settings.snippets.snippetsEnabled) {
          StackExchange.using("snippets", function() {
          createEditor();
          });
          }
          else {
          createEditor();
          }
          });

          function createEditor() {
          StackExchange.prepareEditor({
          heartbeatType: 'answer',
          convertImagesToLinks: true,
          noModals: true,
          showLowRepImageUploadWarning: true,
          reputationToPostImages: 10,
          bindNavPrevention: true,
          postfix: "",
          imageUploader: {
          brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
          contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
          allowUrls: true
          },
          noCode: true, onDemand: true,
          discardSelector: ".discard-answer"
          ,immediatelyShowMarkdownHelp:true
          });


          }
          });














          draft saved

          draft discarded


















          StackExchange.ready(
          function () {
          StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmathoverflow.net%2fquestions%2f316024%2fa-peculiarity-of-henkins-1950-proof-of-completeness-for-higher-order-logic%23new-answer', 'question_page');
          }
          );

          Post as a guest















          Required, but never shown

























          1 Answer
          1






          active

          oldest

          votes








          1 Answer
          1






          active

          oldest

          votes









          active

          oldest

          votes






          active

          oldest

          votes








          up vote
          8
          down vote













          Henkin's completness proof for first order logic (using his method of constants) and Henkin's work on the completeness of type theory were both carried out in his doctoral 1947 dissertation written under the direction of Alonzo Church. The dissertation was never published, but Henkin wrote a fascinating and detailed article about the genesis of the intertwining ideas in his thesis in 1996 (The Discovery of My Completeness Proofs, The Bulletin of Symbolic Logic, Vol. 2, No. 2 (Jun., 1996), pp. 127-158).



          The following quote from the above paper (starting in the bottom of page 154 and continued to the next page) seems to answer your question (and vindicate your colleague). Henkin uses "cwff" for closed well-formed formulae; i.e., those with no free variables.




          As indicated, in addition to putting the first-discovered proof into Part
          III of the dissertation, I hid the discovery process in another way. Namely,
          in setting forth the formal language for type theory, in Part III, I deleted
          from Church's system the symbols $iota_b(0b)$ and the axiom of choice for which they were used! Those symbols, and that axiom, which quintessential role in the discovery process, were omitted in Theorem VI, and the role of the symbols $iota_b(0b)$ in forming "witnesses" cwffs of the form $exists x_bM_0$ was taken over by the adjunction of constants $u_b$, $u'_{b}$, $u''_{b}$ for each type symbol $b$.







          share|cite|improve this answer





















          • Just saw your comment after posting my update. So the $iota$ operator provides witnesses. Given this is not immediately obvious in the published article, why didn't he make it more clear? There is no mention at all of the construction. Can we see any precise point in the article in which he is implicitly referring to it?
            – user65526
            Nov 23 at 15:10















          up vote
          8
          down vote













          Henkin's completness proof for first order logic (using his method of constants) and Henkin's work on the completeness of type theory were both carried out in his doctoral 1947 dissertation written under the direction of Alonzo Church. The dissertation was never published, but Henkin wrote a fascinating and detailed article about the genesis of the intertwining ideas in his thesis in 1996 (The Discovery of My Completeness Proofs, The Bulletin of Symbolic Logic, Vol. 2, No. 2 (Jun., 1996), pp. 127-158).



          The following quote from the above paper (starting in the bottom of page 154 and continued to the next page) seems to answer your question (and vindicate your colleague). Henkin uses "cwff" for closed well-formed formulae; i.e., those with no free variables.




          As indicated, in addition to putting the first-discovered proof into Part
          III of the dissertation, I hid the discovery process in another way. Namely,
          in setting forth the formal language for type theory, in Part III, I deleted
          from Church's system the symbols $iota_b(0b)$ and the axiom of choice for which they were used! Those symbols, and that axiom, which quintessential role in the discovery process, were omitted in Theorem VI, and the role of the symbols $iota_b(0b)$ in forming "witnesses" cwffs of the form $exists x_bM_0$ was taken over by the adjunction of constants $u_b$, $u'_{b}$, $u''_{b}$ for each type symbol $b$.







          share|cite|improve this answer





















          • Just saw your comment after posting my update. So the $iota$ operator provides witnesses. Given this is not immediately obvious in the published article, why didn't he make it more clear? There is no mention at all of the construction. Can we see any precise point in the article in which he is implicitly referring to it?
            – user65526
            Nov 23 at 15:10













          up vote
          8
          down vote










          up vote
          8
          down vote









          Henkin's completness proof for first order logic (using his method of constants) and Henkin's work on the completeness of type theory were both carried out in his doctoral 1947 dissertation written under the direction of Alonzo Church. The dissertation was never published, but Henkin wrote a fascinating and detailed article about the genesis of the intertwining ideas in his thesis in 1996 (The Discovery of My Completeness Proofs, The Bulletin of Symbolic Logic, Vol. 2, No. 2 (Jun., 1996), pp. 127-158).



          The following quote from the above paper (starting in the bottom of page 154 and continued to the next page) seems to answer your question (and vindicate your colleague). Henkin uses "cwff" for closed well-formed formulae; i.e., those with no free variables.




          As indicated, in addition to putting the first-discovered proof into Part
          III of the dissertation, I hid the discovery process in another way. Namely,
          in setting forth the formal language for type theory, in Part III, I deleted
          from Church's system the symbols $iota_b(0b)$ and the axiom of choice for which they were used! Those symbols, and that axiom, which quintessential role in the discovery process, were omitted in Theorem VI, and the role of the symbols $iota_b(0b)$ in forming "witnesses" cwffs of the form $exists x_bM_0$ was taken over by the adjunction of constants $u_b$, $u'_{b}$, $u''_{b}$ for each type symbol $b$.







          share|cite|improve this answer












          Henkin's completness proof for first order logic (using his method of constants) and Henkin's work on the completeness of type theory were both carried out in his doctoral 1947 dissertation written under the direction of Alonzo Church. The dissertation was never published, but Henkin wrote a fascinating and detailed article about the genesis of the intertwining ideas in his thesis in 1996 (The Discovery of My Completeness Proofs, The Bulletin of Symbolic Logic, Vol. 2, No. 2 (Jun., 1996), pp. 127-158).



          The following quote from the above paper (starting in the bottom of page 154 and continued to the next page) seems to answer your question (and vindicate your colleague). Henkin uses "cwff" for closed well-formed formulae; i.e., those with no free variables.




          As indicated, in addition to putting the first-discovered proof into Part
          III of the dissertation, I hid the discovery process in another way. Namely,
          in setting forth the formal language for type theory, in Part III, I deleted
          from Church's system the symbols $iota_b(0b)$ and the axiom of choice for which they were used! Those symbols, and that axiom, which quintessential role in the discovery process, were omitted in Theorem VI, and the role of the symbols $iota_b(0b)$ in forming "witnesses" cwffs of the form $exists x_bM_0$ was taken over by the adjunction of constants $u_b$, $u'_{b}$, $u''_{b}$ for each type symbol $b$.








          share|cite|improve this answer












          share|cite|improve this answer



          share|cite|improve this answer










          answered Nov 23 at 15:00









          Ali Enayat

          10.2k13265




          10.2k13265












          • Just saw your comment after posting my update. So the $iota$ operator provides witnesses. Given this is not immediately obvious in the published article, why didn't he make it more clear? There is no mention at all of the construction. Can we see any precise point in the article in which he is implicitly referring to it?
            – user65526
            Nov 23 at 15:10


















          • Just saw your comment after posting my update. So the $iota$ operator provides witnesses. Given this is not immediately obvious in the published article, why didn't he make it more clear? There is no mention at all of the construction. Can we see any precise point in the article in which he is implicitly referring to it?
            – user65526
            Nov 23 at 15:10
















          Just saw your comment after posting my update. So the $iota$ operator provides witnesses. Given this is not immediately obvious in the published article, why didn't he make it more clear? There is no mention at all of the construction. Can we see any precise point in the article in which he is implicitly referring to it?
          – user65526
          Nov 23 at 15:10




          Just saw your comment after posting my update. So the $iota$ operator provides witnesses. Given this is not immediately obvious in the published article, why didn't he make it more clear? There is no mention at all of the construction. Can we see any precise point in the article in which he is implicitly referring to it?
          – user65526
          Nov 23 at 15:10


















          draft saved

          draft discarded




















































          Thanks for contributing an answer to MathOverflow!


          • Please be sure to answer the question. Provide details and share your research!

          But avoid



          • Asking for help, clarification, or responding to other answers.

          • Making statements based on opinion; back them up with references or personal experience.


          Use MathJax to format equations. MathJax reference.


          To learn more, see our tips on writing great answers.





          Some of your past answers have not been well-received, and you're in danger of being blocked from answering.


          Please pay close attention to the following guidance:


          • Please be sure to answer the question. Provide details and share your research!

          But avoid



          • Asking for help, clarification, or responding to other answers.

          • Making statements based on opinion; back them up with references or personal experience.


          To learn more, see our tips on writing great answers.




          draft saved


          draft discarded














          StackExchange.ready(
          function () {
          StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmathoverflow.net%2fquestions%2f316024%2fa-peculiarity-of-henkins-1950-proof-of-completeness-for-higher-order-logic%23new-answer', 'question_page');
          }
          );

          Post as a guest















          Required, but never shown





















































          Required, but never shown














          Required, but never shown












          Required, but never shown







          Required, but never shown

































          Required, but never shown














          Required, but never shown












          Required, but never shown







          Required, but never shown







          Popular posts from this blog

          Berounka

          Sphinx de Gizeh

          Different font size/position of beamer's navigation symbols template's content depending on regular/plain...