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.

  • 1
    $\begingroup$ the write-up could be better, but I think you're right that both are valid. $\endgroup$ – Henno Brandsma Apr 17 '16 at 21:12
  • $\begingroup$ Cool. Many thanks. I was somewhat insecure about it :) $\endgroup$ – LiorGolan Apr 17 '16 at 21:23

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).

| cite | improve this answer | |
  • $\begingroup$ Could you elaborate what's the problem with my proof? $\endgroup$ – LiorGolan Apr 18 '16 at 8:39
  • $\begingroup$ @LiorGolan As I said, your proof was correct. The issue was that structurally your proof was like: "To prove 1+1=2, assume that it does not, now by calculation we see that 1+1 does equal 2, hence we have a contradiction, therefore it must have been the case that 1+1=2." The proof by contradiction is just a detour here. You could have just said, "by calculation, 1+1 does equal 2" without the detour. Stepping back, in general, regardless of your philosophical position, constructive proofs are more valuable than non-constructive proofs since they apply in more situations, i.e. there are more ... $\endgroup$ – Derek Elkins left SE Apr 18 '16 at 9:08
  • $\begingroup$ ... models of constructive logic. This is trivially true as constructive logic makes less assumptions, but the actual explosion in variety of models is staggering. The distinction (and this is more than an analogy) is akin to considering only discrete topological spaces versus all topological spaces. A constructive proof is a statement about far more things than a non-constructive one. Most dear to me personally, is that constructive proofs can be interpreted as programs. $\endgroup$ – Derek Elkins left SE Apr 18 '16 at 9:08

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.