Are those formulas valid?

Question

Consider the following formulas:

1. $\forall x(A\to B)\to ((\exists x A) \to \exists x B)$
2. $\forall x(A\to B)\to ((\forall x A) \to \forall x B)$

Now, I claim that both formulas are indeed valid.

The proofs are very similar so I'll focus on the first one. What I did is assuming by contradiction that the formula isn't valid, so it has the value $t\to f$. Then, it must be that there's an $a$ which satisfies $A$ but there isn't an $x$ which satisfies $B$.

We assumed that $\forall x(A\to B)$ is $t$, but we get a contradiction because for that $a$ we get $A\to B = f$.

A similar proof can be conducted the second formula.

Am I right here? Or am I missing something?
Because at first I guessed that one of them isn't valid.

Answer 1

There is no need to use proof by contradiction, albeit the proof you gave is not incorrect. The latter is completely provable in a constructive logic. The former is provable with both a constructive interpretation of $\exists$ and a more faithful interpretation of the classical $\exists$ albeit only for "proposition"-valued $B$. Your use of proof by contradiction, though, is not only unnecessary, it's basically superfluous! You assume that the statement is false, then prove that it is true, then use double negation elimination on the resulting contradiction to complete your proof. You could've just used the proof that you made to make a contradiction!

To validate my claim and for a different perspective, here are complete proofs for the constructive versions in Agda:

open import Data.Product -- for Σ, the dependent sum

ex1 : {X : Set}{A B : X → Set} → (∀ x → A x → B x) → (Σ[ x ∈ X ] (A x) → Σ[ x ∈ X ] (B x))
ex1 f (t , a) = t , f t a

ex2 : {X : Set}{A B : X → Set} → (∀ x → A x → B x) → (∀ x → A x) → ∀ x → B x
ex2 f g x = f x (g x)

You can read off a more standard "proof" from the above terms (though personally I find the terms more compelling because they patently have computational content).

For the former, we're given a proof, f, that $\forall x. A(x) \to B(x)$ and a proof, (t , a), that $\exists x.A(x)$, and in particular t is a witness to this, i.e. $A(t)$ holds. We need to provide a $t'$ and a proof that $B(t')$ holds. We choose $t' = t$ and proved $B(t)$ by instantiating $f$ with $t$ and using modus ponens to and a to get a proof of $B(t)$, namely f t a. The only difference for a more classical interpretation of $\exists$ is that we need to make sure the witness is not observable, or to put it another way that all proofs of $\exists x.B(x)$ are the same. This doesn't hold for arbitrary (constructive) predicates $B$, but it does for ones that are "proposition"-valued which I won't explain except to say that in normal, proof-irrelevant logics, everything is proposition valued.

For the latter, we still start with the proof f, but now we're given a proof g that $\forall x.A(x)$ and need to prove that for an arbitrary $x$ we have $B(x)$. We do this by instantiating f with $x$ and g with $x$ and then using modus ponens to get our proof of $B(x)$, namely f x (g x).