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
(** A formalization of Andrew's counterexample to functional extensionality in
*)
(** Henkin's notion of general model for Church's theory of types *)
(** (to be continued) *)
Require Import Utf8.
(** Simple types *)
Inductive types := ι | ο | Arrow : types -> types -> types.
(* The notation "αβ" for arrow types would not be easy to implement, we use an
arrow instead *)
Infix "-->" := Arrow (at level 30, right associativity).
(** The interpretation of ι *)
Inductive I := l | m | n.
(** The interpretation of ο *)
Inductive O := t | f.
(** A domain equipped with 3 relations *)
Inductive domrel3 :=
{ dom :> Type;
eq₁ : dom -> dom -> Prop;
eq₂ : dom -> dom -> Prop;
eq₃ : dom -> dom -> Prop;
}.
Notation "x ≡₁ y" := (eq₁ _ x y) (at level 70).
Notation "x ≡₂ y" := (eq₂ _ x y) (at level 70).
Notation "x ≡₃ y" := (eq₃ _ x y) (at level 70).
(* A notation for extracting the inhabitant of a subset type {x:A|B} *)
Notation "[ x ]" := (exist _ x _).
(* The definition of the model which does not satisfy functional extensionality
*)
Fixpoint D t := match t with
| ι => {| dom := I;
eq₁ u v := u = l ∧ v = l ∨ u <> l ∧ v <> l;
eq₂ u v := u = m ∧ v = m ∨ u <> m ∧ v <> m;
eq₃ u v := u = n ∧ v = n ∨ u <> n ∧ v <> n |}
| ο => {| dom := O;
eq₁ u v := u = v;
eq₂ u v := u = v;
eq₃ u v := u = v |}
| β --> α => {| dom := {f : D β -> D α | ∀ u v, (u ≡₁ v -> f u ≡₁ f v) ∧ (u ≡₂
v -> f u ≡₂ f v) ∧ (u ≡₃ v -> f u ≡₃ f v)};
eq₁ := fun '[g] '[h] => ∀ x, g x ≡₁ h x;
eq₂ := fun '[g] '[h] => ∀ x, g x ≡₂ h x;
eq₃ := fun '[g] '[h] => ∀ x, g x ≡₃ h x |}
end.
(* A notation to tell that a function satisfies the condition to be in some
subset type *)
Notation "f ∈ A" := (exists '([f'] : A), f' = f) (at level 70).
Theorem allOO : ∀ g : O -> O, g ∈ D (ο --> ο).
Proof.
intros g.
eexists [g].
reflexivity.
Unshelve.
repeat split; intros ->; reflexivity.
Qed.
Definition neg (b:O) : O := match b with t => f | f => t end.
Theorem a1 : neg ∈ D (ο --> ο).
Proof.
apply allOO.
Qed.
Definition cst_t (b:O) : O := t.
Theorem a2 : cst_t ∈ D (ο --> ο).
Proof.
apply allOO.
Qed.
Definition id (b:O) : O := b.
Theorem a2' : id ∈ D (ο --> ο).
Proof.
apply allOO.
Qed.
(* etc *)
------------------------------------------------------------------------------
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
