Deductive logic counter-intuitive result

Question

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!

Answer 1

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}$

Answer 2

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/