Dear Members of the Research Community,
Concerning Henkin's paper "Completeness in the Theory of Types" (1950), I have
a question.
Theorem 2 is claimed to be false in Andrews' newest publication that forms part
of the volume on Leon Henkin edited by Manzano et al.: "Thus, Theorem 2 of
[Henkin, 1950] (which asserts the completeness and soundness of C) is
technically incorrect. The apparently trivial soundness assertion is false."
[Andrews, 2014b, p. 70]
For an extended quote, see the very end of the section "Criticism" of
http://doi.org/10.4444/100.111
Have there been any formalization efforts for Theorem 2 of [Henkin, 1950], such
that the above claim can be verified (or refuted) by mechanized reasoning
(formalization in a computer)?
Following a purely syntactic approach, I usually skip semantic issues, but
this nevertheless seems an interesting question to me.
According to Roger Bishop Jones's advice at
https://sourceforge.net/p/hol/mailman/message/35435344/
now Ramsey (and Chwistek) was added to the diagram at
http://doi.org/10.4444/100.111
who first suggested the simple theory of types according to footnote 1 of
[Church, 1940],
Both Chwistek and Ramsey are mentioned in the "Introduction to the Second
Edition" of "Principia Mathematica" in some way, but I am not familiar with the
details of how strong the impact on Russell's own theory was.
In paragraph 9 of Carnap's 1929 German-language "Abriss der Logistik"
(referenced in Church's footnote 1), Ramsey is mentioned, but not Chwistek (who
is referenced indirectly through p. xiv of the Introduction to the 2nd ed. of
PM - see Carnap, pp. 21 f.).
In Quine's introduction to Russell's 1908 essay "Mathematical Logic as Based on
the Theory of Types" only Ramsey is mentioned (van Heijenoort, 1967, p. 152).
It is interesting to see that both Ramsey and Henkin ("Identity as a logical
primitive", 1975) prefer the term 'identity' rather than 'equality', which is
also my preference, as mentioned at
https://sourceforge.net/p/hol/mailman/message/35446249/
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-October/msg00070.html
Ramsey: "[M]athematics does not consist of tautologies, but of [...]
'equations', for which I should prefer to substitute 'identities'. [...] [I]t
is interesting to see whether a theory of mathematics could not be constructed
with identities for its foundation. I have spent a lot of time developing such
a theory, and found that it was faced with what seemed to me insuperable
difficulties."
Quoted in: [Andrews, 2014b, p. 67]
Available online at: http://www.hist-analytic.com/Ramsey.htm
For the references, please see:
http://doi.org/10.4444/100.111
Kind regards,
Ken Kubota
____________________
Ken Kubota
http://doi.org/10.4444/100
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, SlashDot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
