Dear Hugo Herbelin,
Thank you very much for your email, including your kind efforts to begin a
formalization of Andrews' counterexample to functional extensionality in
Henkin's notion of general model for Church's theory of types within the Coq
software.
I apologize for the delay in answering. The email exchange with other
scientists is quite time consuming. As they wrote earlier, I felt the need to
answer them first, too. And I replied to an email of Peter Andrews I received
just a few days ago.
For now, I have updated my overview at
http://doi.org/10.4444/100.111
in order to clearly distinguish between approaches that rely on the
Curry-Howard isomorphism, and those that do not.
An adequate answer to the many arguments you gave will require some more time.
Thank you very much for your patience in advance.
Kind regards,
Ken Kubota
____________________
Ken Kubota
http://doi.org/10.4444/100
> Am 08.12.2016 um 21:15 schrieb Hugo Herbelin <hugo.herbe...@inria.fr>:
>
> Dear Ken Kubota,
>
> On Sun, Dec 04, 2016 at 02:31:16PM +0100, Ken Kubota wrote:
>> 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.
>
> As far as I can judge, [Andrews, 1972] is more than a claim. It is a
> theorem showing that the statement of Theorem 2 of [Henkin, 1950] is
> incorrect as stated, since the given definition of general models
> fails to ensure that functional extensionality necessarily holds. So,
> there is little hope to have Theorem 2 of [Henkin, 1950] being
> formally provable as it is, unless changing the definition of models
> as suggested e.g. by [Andrews, 1972].
>
> On the other side, I see hope to formally verify the theorem proved in
> [Andrews, 1972], what I started to do for the fun of it in the
> attached file, if ever you are interested to see how such a
> formalization could look like.
>
> Incidentally, since you are interested in Henkin's completeness
> proofs, you may be interested in a draft paper I wrote with Danko Ilik
> on the computational content of Henkin's proof in the first-order case
> with recursively enumerable theories [1], trying to answer the
> following question: assume you have a proof of validity of a formula;
> by Henkin's proof of completeness you know that there is a proof of
> this formula; which it is effectively?
>
> [1] http://pauillac.inria.fr/~herbelin/articles/godel-completeness-draft16.pdf
>
>> 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
>
> I read your document and I would like to make 2 remarks.
>
> About Coq, it would like to clarify for the record that the logical
> formalism which is implemented keeps evolving. In the very first
> versions, it was just Coquand and Huet's Calculus of Constructions,
> i.e. the functional pure type system with all dependent products over
> the two sorts Prop:Type. In version 2.9, a cumulative hierarchy of
> universes was added giving the equivalent of Luo's Extended Calculus
> of Constructions without Σ-types (or alternatively Miquel's CCω, i.e.,
> if my memories are correct, Coquand's Generalized Calculus of
> Constructions with an additional subtyping Prop ⊂ Type(1) which it did
> not have). In version 4.3, a universe of impredicative types (intended
> to be inhabited by relevant "programs") was explicitly separated from
> the isomorphic universe of impredicative propositions (intended to be
> proof-irrelevant). Then, the next radical change was in version 5.0
> which introduced native inductive types. This made the new system,
> which Coquand and Paulin designed, a variant of Martin-Löf's
> intensional type theory with an impredicative universe of propositions
> and an impredicative universe of types. It is at this time that the
> logic underlying Coq started to be called the Calculus of Inductive
> Constructions. Another significant change arrived in version 8.0 with
> the renouncement to the impredicative universe of types. With this
> impredicative universe, Coq was strongly committed to a setting
> inconsistent with the combination of classical logic and of the
> intensional axiom of choice stated in the impredicative universe of
> propositions. By dropping it, Coq started to be usable as a framework
> for "classical" mathematics, with a range of axioms available in the
> standard library as extensions of the core logic. Later, in version
> 8.5, a subtle feature of the criterion for ensuring well-foundedness
> of functions was dropped so as to make the system compatible with
> propositional extensionality. And this is certainly not the end of the
> story since other evolutions are in the implementation pipeline:
> inductive-inductive types, inductive-recursive types and higher
> inductive types, thanks to Matthieu Sozeau and Cyprien Mangin.
>
> My second remark is about the classical vs constructive foundations,
> which makes sense historically but which I believe tends to be
> replaced by approaches where logics are assembled from basic
> components which can be consistently combined or not together, and for
> which even the components traditionally considered as "classical" have
> "constructive" contents.
>
> For instance, on a domain I'm familiar with, classical reasoning is
> "constructive" and the technical apparatus beyond it is actually known
> for several decades. It is Kolmogorov's double negation translation
> for reduction of classical reasoning to intuitionistic reasoning and
> Gentzen-Prawitz's cut-elimination procedure for computing with
> classical proofs. That classical logic computes became clear
> retrospectively thanks to Griffin, Parigot, Krivine, Murthy, and
> others, who made an explicit connection with programming
> languages. Even if classical reasoning introduces ideal objects
> (e.g. the "platonistic" witness of ∃b(b=0 ↔ A)), any proof using
> classical reasoning eventually computes effective witnesses for simple
> enough formulas such as Σ⁰₁-formulas, getting rid in the process of
> the ideal objects involved in the proof.
>
> As another example, the intensional axiom of choice has an immediate
> constructive interpretation given by Σ-types in Martin-Löf's type
> theory, but restrictions of it can still be combined in a constructive
> way with classical logic using Spector's bar recursion and variants of
> it.
>
> In any case, thanks for your interest in logical foundations.
>
> Hugo Herbelin
> <andrews72.v>
------------------------------------------------------------------------------
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
