Do Hindley-Milner theories have a Deduction Theorem?

Question

Deduction Theorem: Given $\Gamma \cup \{A\} \vdash B$, we can deduce $\Gamma \vdash A \to B$

HM Counter-Example (?):

Take $A$ to be $\forall f : \alpha \to \alpha, \forall x : \alpha, f(x) = f(f(f(x)))$

Take $B$ to be $\forall g : \beta \to \beta, \forall y : \beta, g(y) = g(g(g(y)))$

Clearly $\Gamma \cup \{A\} \vdash B$, but the resulting proposition is problematic:

$[\forall f : \alpha \to \alpha, \forall x : \alpha, f(x) = f(f(f(x)))] \to [\forall g : \beta \to \beta, \forall x : \beta, g(x) = g(g(g(x)))]$

If we then instantiate $\alpha$ to be the boolean type $\mathtt{Bool}$, we get that an easily-provable proposition $\forall f : \mathtt{Bool} \to \mathtt{Bool}, \forall x : \mathtt{Bool}, f(x) = f(f(f(x)))$ implies $B$, which is clearly false.

$\Rightarrow\!\Leftarrow$

Is this a legitimate issue with Hindley-Milner formulations like $\textbf{Q}_0$? Or did I do math wrong? If it is valid, what are the implications of this unintuitive result? I imagine it is quite limiting to have a deductive system without the Deduction Theorem. Is this phenomenon well-documented somewhere?

Answer 1

This doesn't really have anything to do with the deduction theorem, but rather with how instantiation does(n't) play with conditionals.

Per the comments, both $\alpha$ and $\beta$ are implicitily universally quantified, so let's consider a simpler example where the corresponding quantifiers are explicit. The sentence "If all $x$ are even, then all $y$ are odd" is vacuously provable from any reasonable theory of arithmetic. However, "If $4$ is even, then $6$ is odd" trivially disprovable from any reasnoable theory of arithmetic.

It may be helpful to keep in mind that the hypothesis of a conditional is secretely negated: if we rewrite $$[\forall xP(x)]\rightarrow [\forall yQ(y)]$$ as $$[\exists x\neg P(x)]\vee[\forall yQ(y)]$$ I think it becomes clearer why the kind of "simultaneous instantiation" you're trying to do doesn't actually work. (This also plays a key role in uncovering the notationally-obscured symmetry behind "bounded" quantifiers, per this old answer of mine.) Consider as well the distinction between "$\forall x(A\rightarrow B)$" and "$\forall xA\rightarrow\forall xB$."

Answer 2

After some more research, I realize now that I had one main misconception.

This question was originally inspired by $\textbf{Q}_0$, but the standard formal formulation of $\textbf{Q}_0$ is not actually a Hindley-Milner theory, it is just simply-typed lambda calculus. All uses of $\alpha$ and $\beta$ in its formulation are used to represent infinite schemas of constants, axioms, and theorems. The formulation seems valid in STLC, including its proof of the deduction theorem.

That being said, there are still a few open questions:

1. It seems like $\textbf{Q}_0$ should be formulatable in a Hindley-Milner system, which could better and more easily represent $\textbf{Q}_0$'s infinite definition, axiom, and theorem schemas. Has anyone done this before? If so, would my original question apply in such a formulation?
2. I do believe that my original question would still apply to other Hindley Milner theories, but I don't know much about other HM theories. Maybe the HOL family is affected by this? I don't know how rigorously people have studied the metamathic properties of those systems. But I imagine a weaker version of the Deduction Theorem would still hold when $A$ is restricted to only monomorphic terms.

Answer 3

I think the theorem you try to prove is this: For all instantiations of $\alpha, \beta$ in the terms $A,B$ with variables of the calculus, whenever $A \vdash B$ holds, then $\vdash A \to B$ holds as well.

This statement is true. But your claim in your question that "after instantiating $\alpha \mapsto Bool$ we can deduce $B$ for all $\beta$" is false. Certainly, after this instantiation $A$ will be a valid statement. But the deduction theorem only says that $A \vdash B$ implies (or stronger, that it is equiv. to) $\vdash A \to B$. Since $A$ is valid in our case, we can replace it with truth, i.e. $\top$ and after further simplification this instance of the deduction theorem becomes equivalent to "$\vdash B$ implies $\vdash B$, for arbitrary $\beta$". Which isn't problematic.

All systems that you mention have (iirc) a corresponding deduction theorem, but by being careful with the quantifiers and variables, none lead to contradictions.