Deductive logic counter-intuitive result I am working on a small proof in deductive logic. Here is what must be proved:
$(\exists x \in T \mid A \implies P(x)) \implies A \implies (\forall x \in T \mid P(x))$
To me that looks unprovable and even false in term of classical logic, but I am using Tutch (http://www2.tcs.ifi.lmu.de/~abel/tutch/ for those who don't know it) which actually tells me it is true.
proof nonsense : (?x:t.(A => P(x))) => A => !x:t.P(x) =
begin
[?x:t.(A => P(x));
    [A;
        [a:t;
            [a:t, A => P(a);
                P(a)];
            P(a)];
        !x:t.P(x)];
    A => !x:t.P(x)];
(?x:t.(A => P(x))) => A => !x:t.P(x)
end;

Tutch returns me QED, meaning that the proof is correct. Although it looks like a scoping error.
Did I just find a bug in Tutch or is this actually true in deductive logic?
Thank you!
 A: As far as I can tell, your 'proof' involves an existential elimination to witness ($a$), then universal introduction to discharge this witness.   This is not valid, because a witness is not an arbitrary value.
$\require{enclose}\require{cancel}\begin{array}{l|l:l:l}
1 & \exists x\in T: (A \to P(x)) & \text{assume} & +1
\\ \quad 2 & \quad A & \text{assume} & +2
\\ \qquad 3. & \qquad A \to P(a) & 1,\exists{-} & +3\vert^{x\in T}_{a:\textsf{witness}}
\\ \qquad\quad 4. & \qquad\quad P(a) & 2,3,\to{-}
\\ \hdashline \qquad 5. & \qquad \forall x\in T: P(x) & 4,a,\enclose{circle}[mathcolor="red"]{\forall{+}} & -3\vert^{x\in T}_{a:\enclose{circle}[mathcolor="red"]{\textsf{witness}}}
\\ \hdashline \quad 6. & \quad A \to \forall x\in T:P(x) & 2, 5, \to{+} & -2
\\ \hline 7. & (\exists x\in T:(A \to P(x))) \to (A \to \forall x\in T:P(x)) & 1,6,\to{+} & -1
\end{array}$
A: This tree proof generator provides the following countermodel:

One can make the consequent false by assigning $A$ the value true and letting $P$ be true for only one of the two members of the domain. Since there exists a member of the domain for which $P$ is true, namely $a$, the antecedent is true. 

Tree Proof Generator. https://www.umsu.de/logik/trees/
