$(A \lor B) \implies (((A \lor B) \implies A) \lor ((A \lor B) \implies B))$?

Question

Is the implication in the title true?

I haven't studied logic formally yet, so I can't precisely say what A, B exactly are. Perhaps "predicates in first-order logic"?

Answer 1

The implication in the title is true.

This is because if $A\lor B$ is true, then either $A$ is true or $B$ is true. If $A$ is true, then $P\implies A$ is true for any $P$, so in particular $(A\lor B)\implies A$ is true. And similarly if $B$ is true then $(A\lor B)\implies B$ is true. So since either $A$ or $B$ is true, one of $(A\lor B)\implies A$ and $(A\lor B)\implies B$ is true, so $((A\lor B)\implies A)\lor((A\lor B)\implies B)$ is true.

Another way to show this would be to construct a truth table.

Another way would be to present a program with that type; then the Curry-Howard isomorphism allows one to translate the program directly into a proof of the theorem:

    f :: (Either a b) -> (Either (Either a b -> a) (Either a b -> b))
    f (Left a)  = Left  (\e -> a)
    f (Right b) = Right (\e -> b)

(Either a b is Haskell notation for the type $a \lor b$. The most general type of this program is actually $(A \lor B) \implies ((X\implies A)\lor (Y\implies B))$, which is a true theorem of which your desired theorem is a special case.)