5

This question grew out of this question, but my question is on the logic structure to a possible answer to that question.

In that question, the OP was trying to prove a statement of the form

$$(A \implies B) \implies C$$

The way I've learnt this, is that you assume the antedecent $(A \implies B)$ and prove the consequent $C$. My problem with this is that from the given antecedent, we cannot assume $A$, nor $B$, but only that $A$ implies $B$. Yet in the hint to the OP in that question, the answerer seems to reason like this:

"Assume $A$, and that $B$ follows from $A$, now prove C"

I can't justify to myself why I would be allowed to assume $A$. More broadly, what exactly can I use when proving these statements? Can I assume $A$ is true and that $B$ follows?

If I may ask for an example of a proof of some trivial statement in the style of everyday language ("All men are mortal" or the like), I'm sure this will clear up.

Thanks in advance.

JuliusL33t
  • 2,424
  • You're right. The strategy you described can prove $A\to(A\to B)\to C$ or $(A\to B) \to (A\to C)$ not $(A\to B)\to C$. – MJD Oct 22 '17 at 12:18
  • The "trick" is that the theorem of the related question: "if (if ..., then ___), then $f$ is continuous" is not proved by logic alone. It is proved using the mathematical definition of continuity (and maybe also some additonal properties). This is shown by the fact that $(A \to B) \to C$ is not a "law of logic" i.e. a tautology. – Mauro ALLEGRANZA Oct 22 '17 at 12:24
  • The logic in the answer you link to is backwards in several ways -- do not take it as a model of valid proof structure! – hmakholm left over Monica Oct 22 '17 at 12:26
  • @HenningMakholm This is exactly why I'm asking! What would be a model of a valid proof structure? – JuliusL33t Oct 22 '17 at 12:33
  • @JuliusL33t: For the particular statement in the older question, it seems to be much easier to prove the contrapositive, $\neg C\Rightarrow \neg(A\Rightarrow B)$ -- or actually, since the real claim is $(\forall \vec a)(A(\vec a)\Rightarrow B(\vec a))\Rightarrow C$, the contrapositive is $\neg C\Rightarrow (\exists \vec a)\neg(A(\vec a)\Rightarrow B(\vec a))$. So assume $\neg C$ and use that assumption to come up with an $\vec a$ such that $A(\vec a)$ yet not $B(\vec a)$. – hmakholm left over Monica Oct 22 '17 at 12:38
  • @HenningMakholm But this just reduces the problem to one of the form $A \implies $___, which is specifically what I want to avoid. The whole idea is to learn how to use a conditional as an antecedent! – JuliusL33t Oct 22 '17 at 13:00
  • @JuliusL33t: That's not a good example for that, though -- because, as I said, the antecedent doesn't have the form $A\Rightarrow B$ but $(\forall x)(A(x)\Rightarrow B(x))$. The quantifier is important, and where it stands is essential to the claim being true at all. – hmakholm left over Monica Oct 22 '17 at 13:10
  • In addition, you have to note that the continuity condition is of the form: $D \to E$; if $|x-y| < \delta \to |f(x)-f(y)| < \epsilon$. – Mauro ALLEGRANZA Oct 22 '17 at 13:12
  • The proof runs as follows: assume $D$ and "re-write" it in terms of sequence: $A$. Then use $A \to B$ to conclude with $B$, i.e. $E$. Then discharge the assumption and conclude with $D \to E$, that is continuity. – Mauro ALLEGRANZA Oct 22 '17 at 13:13
  • 1
    @Mauro: I'm not sure that plan of attack actually works here. I can't get the details to work out that way, and I suspect "sequential continuity implies continuity" is not constructively valid -- so one has to use something like contraposition in order to get there. – hmakholm left over Monica Oct 22 '17 at 13:18
  • That problem was raised (but not answered) at https://math.stackexchange.com/questions/1312873/show-constructively-that-the-sequence-definition-of-continuity-implies-the-epsil – hmakholm left over Monica Oct 22 '17 at 13:22
  • In some sense, claiming an implication is the antecedent is somewhat misleading as $\Rightarrow$ is just an abbreviation using $\lnot$ and $\lor$ (or, being pedantic, it's logically equivalent to such a formula). Certainly, you can use the fact that $A \Rightarrow B$ is logically equivalent to $\lnot A \lor B$. Now you may assume that (1) $A$ fails or (2) $B$ holds. – MacRance Mar 07 '19 at 21:22

1 Answers1

1

To prove something in a logical theory $\mathfrak{T}$ such as $A\implies B$, one adjoins $A$ to the explicit axioms of $\mathfrak{T}$ and proves $B$ within the newly gained theory. In short, what you stated was right. $A\implies B$ is to be assumed, but nothing about $A$ or $B$.

If you would like to gain grounding in some basic logic, I recommend Bourbaki's Theory of Sets book. It is a bit old (some outdated terminology), but definitely a beautiful resource to learn from.