The Coq mailing list

[Ken Kubota <mail AT kenkubota.de>]

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