How do I show that A iff B proves A implies B?

Question

Prove that $ {A} \leftrightarrow B $ proves $ A \to B $

I have tried to use some logical axioms but can see no obvious one other than $$ (A \rightarrow B) \leftrightarrow ((A \lor B) \leftrightarrow B) $$.

Answer 1

Hint:

$$p\leftrightarrow{q}\iff((p\rightarrow{q})\land(q\rightarrow{p}))$$

Answer 2

Depends on what method of proof you are using ... and even within those methods there are typically different options. Here are some of those methods and options:

Truth-table

Strategy 1: Put both $A \leftrightarrow B$ and $A \rightarrow B$ as separate entries on a table:

\begin{array}{cc|c|c} A & B & A \leftrightarrow B & A \rightarrow B\\ \hline T & T & T & T\\ T & F & F & F\\ F & T & F & T\\ F & F & T & T\\ \end{array}

We see that whenever $A \leftrightarrow B$ is true, $A \rightarrow B$ is also true. Hence, $A \leftrightarrow B \Rightarrow A \rightarrow B$

Strategy 2: Write the implication as a logical conditional, and evaluate that:

\begin{array}{cc|ccc} A & B & (A & \leftrightarrow & B) \rightarrow (A & \rightarrow & B)\\ \hline T & T && T & T &T\\ T & F && F & T &F\\ F & T && F & T &T\\ F & F && T & T &T\\ \end{array}

We see that $(A \leftrightarrow B) \rightarrow (A \rightarrow B)$ is a tautology, and that means $A \leftrightarrow B \Rightarrow A \rightarrow B$

Algebra

Strategy 1: Take $A \leftrightarrow B$ and rewrite:

$$A \leftrightarrow B \Leftrightarrow (A \rightarrow B) \land (B \rightarrow A)$$

With $A \rightarrow B$ being one of the conjuncts, it should now be clear that $A \leftrightarrow B \Rightarrow A \rightarrow B$

Strategy 2: Write the implication as a logical conditional, and rewrite that:

$$(A \leftrightarrow B) \rightarrow (A \rightarrow B) \Leftrightarrow$$

$$((A \rightarrow B) \land (B \rightarrow A)) \rightarrow (A \rightarrow B) \Leftrightarrow$$

$$ \neg ((A \rightarrow B) \land (B \rightarrow A)) \lor (A \rightarrow B) \Leftrightarrow$$

$$ \neg (A \rightarrow B) \lor \neg (B \rightarrow A) \lor (A \rightarrow B) \Leftrightarrow$$

$$ \neg (B \rightarrow A) \lor \top \Leftrightarrow$$

$$ \top$$

So, as with the second truth-table strategy, since $(A \leftrightarrow B) \rightarrow (A \rightarrow B)$ is a tautology, we have $A \leftrightarrow B \Rightarrow A \rightarrow B$

Short Truth-Table

Assume what happens when you set $A \leftrightarrow B$ to true, and $A \rightarrow B$ to false:

\begin{array}{cccccc} A & \leftrightarrow & B & A & \rightarrow & B\\ &T&&&F&\\ \end{array}

There is only one way to set $A \rightarrow B$ to false: $A$ should be true and $B$ should be false:

\begin{array}{cccccc} A & \leftrightarrow & B & A & \rightarrow & B\\ &T&&T&F&F\\ \end{array}

Copying the values of $A$ and $B$:

\begin{array}{cccccc} A & \leftrightarrow & B & A & \rightarrow & B\\ T&T&F&T&F&F\\ \end{array}

But now we have a contradiction: $A \Leftrightarrow B$ is supposed to be $T$, but that is not the case if $A$ is true and $B$ is false. Therefore, we have shown that it is impossible to have $A \Leftrightarrow B$ be True and $A \rightarrow B$ be False. And so we have $A \leftrightarrow B \Rightarrow A \rightarrow B$

This method is called the short truth-table method in that you are trying to find a row in the truth-table where the premises(s) are true and the conclusion is false (and if you succeed in finding such a counterexample, then the logical implication does not hold, but if you run into a contradiction (as we did), then the logical implication does hold, as that shows there is no counterexample). By using indices to indicate the order in which we put down the truth-values, we can keep this method to one row:

\begin{array}{cccccc} A & \leftrightarrow & B & A & \rightarrow & B\\ T_3&T_1&F_3&T_2&F_1&F_2\\ \end{array}

Truth-Trees/Semantic Tableaux

Trees and tableaux are really just a way to expand the short-truth table method by systematically incorporating the possible ways in which one might search for possible counterexamples. Various variants exist (there are annotated and non-annotated trees, differences in lay-out, differences in decomposition rules, etc.), but I'll do just one:

$\hspace{260px}$

Again, the indices reflect the order in which the steps are taken. This particular tree is a non-annotated tree, and so we only write down statements we are trying to make true (satisfy). And, since like the short truth-table method we are interesting in the possibility of $A \leftrightarrow B$ being True, and $A \rightarrow B$ being False, we put down the statements $A \leftrightarrow B$ and $\neg(A \rightarrow B)$ in the 'root' of the tree. OK, so then we do the following steps:

1. There is only one way for $\neg(A \rightarrow B)$ to be true, and that is when $A$ is true, and $B$ is false, and so we 'decompose' $\neg(A \rightarrow B)$ into $A$ and $\neg B$. Since satisfying both $A$ and $\neg B$ will satisfy $\neg(A \rightarrow B)$, we can 'check' the latter statement to indicate that we are 'done' with it.

2. There are two ways to make $A \leftrightarrow B$ True: either $A$ and $B$ are both True, or they are both False. Thus, we get two branches, one with $A$ and $B$, and the other with $\neg A$ and $\neg B$. Once this is done, we can 'check' $A \leftrightarrow B$ as the two branches exhaust all possible ways for $A \leftrightarrow B$ to be True

3. In the left branch, we have now reached a contradiction. We of course still have $\neg B$ in the main branch, but now we are trying to set $B$ to True as well. So, this is a dead end in our search for a counterexample, and we can 'close' the branch.

4. But the right branch closes as well, between $A$ and $\neg A$.

Since all branches close, we can conclude there is no possible way to make the statements in the root true, and hence there is no way to have $A \Leftrightarrow B$ be True and $A \rightarrow B$ be False. And so we have $A \leftrightarrow B \Rightarrow A \rightarrow B$

The Tree method looks involved, but once you're used to it, it's great! It also has great properties for when you start doing meta-logic.

Resolution

This is yet another method that attempts to find a counterexample. So, yet again we'll work with the statements $A \leftrightarrow B$ and $\neg(A \rightarrow B)$. Now, the first thing we're going to do is put both statements into CNF using Algebra:

$$A \leftrightarrow B \Leftrightarrow (A \rightarrow B) \land (B \rightarrow A) \Leftrightarrow (\neg A \lor B) \land (\neg B \lor A)$$

$$\neg (A \rightarrow B) \Leftrightarrow A \land \neg B$$

Now we take each conjunct and make it into a 'clause': since each conjunct is a disjunct of literals, the clause is simply that set of literals. So, we have $4$ clauses:

$$1. \{ \neg A, B \}$$

$$2. \{ \neg B, A \}$$

$$3: \{ A \}$$

$$4: \{ \neg B \}$$

Now we are going to 'resolve' clauses by finding two clauses, one of which has a literal that is the complement of one of the literals of the other clause. So, for example, we can resolve clauses $1$ and $3$, since $3$ has the literals $A$, and $1$ has its complement $\neg A$. The result of this resolution is a new clause (the 'resolvent clause') that contains all other literals from the clauses, which in this case is just $B$:

$$5. \{ B \} \quad 1,3$$

And now we can resolve clauses $4$ and $5$:

$$6. \{ \} \quad 4,5$$

We have now reached an empty clause, which is a disjunction with $0$ disjuncts, which is a contradiction (makes sense: with $0$ disjuncts, it is impossible to have at least of them being True).

So, having reached a contradiction, we once again know that there is no possible way to make the statements $A \leftrightarrow B$ and $\neg(A \rightarrow B)$ both True, and hence there is no way to have $A \Leftrightarrow B$ be True and $A \rightarrow B$ be False. And so we have $A \leftrightarrow B \Rightarrow A \rightarrow B$

While Trees are pretty human-friendly, Resolution is more computer-friendly. Indeed, many Automated Theorem Provers are built on some version of Resolution.

Formal Proof

There are many different formal proof systems. There are Natural Deduction systems (notably Fitch systems), sequent calculi, and axiom systems, and within each of these classes are many differences between specific systems depending on how exactly they define their rules or axioms. But, to illustrate, I'll just pick one example system for each:

Fitch System

Here is a proof in a Fitch System (F.S):

$\def\fitch#1#2{\begin{array}{|l}#1 \\ \hline #2\end{array}}$

$\hspace{260px} \fitch{ 1. A \leftrightarrow B}{ \fitch{ 2. A}{ 3. B \quad \quad \leftrightarrow E \ 1,2} \\ 4. A \rightarrow B \quad \rightarrow I \ 2-3}$

Since we can derive $A \rightarrow B$ from $A \leftrightarrow B$, we write from $A \leftrightarrow B \vdash_{F.S.} A \rightarrow B$, and since the rules of this Fitch System is sound, we thus have $A \leftrightarrow B \Rightarrow A \rightarrow B$

Sequent System

Here is a sequent system proof:

$$1. \{ A \leftrightarrow B\} \vDash A \leftrightarrow B \ Assumption$$

$$2. \{ A \} \vDash A \ Assumption$$

$$3. \{ A \leftrightarrow B, A \} \vDash B \ \rightarrow E \ 1,2$$

$$4. \{ A \leftrightarrow B\} \vDash A \rightarrow B \ \rightarrow I \ 3$$

Since we were able to prove $\{ A \leftrightarrow B\} \vDash A \rightarrow B$, we have $A \leftrightarrow B \Rightarrow A \rightarrow B$

Axiom System

And here is a proof in an Axiom system that contains axiom $(\varphi \leftrightarrow \psi) \rightarrow (\varphi \rightarrow \psi)$:

$$1. A \leftrightarrow B \ Assumption$$

$$2. (A \leftrightarrow B) \rightarrow (A \rightarrow B) \ Axiom$$

$$3. A \rightarrow B \ MP \ 1,2$$

So yeah, no shortage of proof methods. Hope that answers your question!