Implication
Implication $A\rightarrow B$ is on occasion introduced as shorthand for $B \vee \neg A$. Their truth tables certainly match, and regardless of the valuations of $A$ and $B$, mappings to truth (a.k.a. interpretations in $ \{ T,F \}$) of both logical formula with coincide.Does this mean implication is superfluous shorthand?
I don't think so because $\rightarrow ,\vee$ are distinct logical connectives and types ($\neg A$ is shorthand for $A \rightarrow \bot$ in intuitionistic logic, but if I'm not mistaken, a seperate type in classical logic). In particular,as the type theory is concerned, separate constructor/eliminator rules will apply to $A\rightarrow B$ and $B \vee \neg A$.
I'm unconvinced and sense a contradiction (they look the same but are built differently). Can someone explain what I'm missing?
Deduction Theorem
I've gone through these questions: related question 1 ,related question 2 but don't seem to quite get it.
So long rules of weakening and modus ponens are part of the logic, it seems easy to prove $A \vdash B$ from $\vdash A \rightarrow B$. Is it therefore only in the other direction that the deduction theorems can fail (if $A \vdash B$ then $\vdash A \rightarrow B$)?
When the deduction theorem does fail, where exactly does it fail in the proof? The base step or the inductive step?
Best Answer
"Does this mean implication is superfluous shorthand?"
No. Implication might come as a pre-assumed notion. It can qualify as a superfluous shorthand in a system where the meaning of implication is not pre-assumed. But, that all depends on the system at hand.
"So long rules of weakening and modus ponens are part of the logic, it seems easy to prove A⊢B from ⊢A→B."
Yes, that's true. Also, you can prove it just from modus ponens.
"Is it therefore only in the other direction that the deduction theorems can fail (if A⊢B then ⊢A→B)?"
No. Logical systems for classical propositional calculus without modus ponens do exist. John Halleck's page indicates that Jean Porte described such a system a while back. If modus ponens fails, you don't have the first direction.
"When the deduction theorem does fail, where exactly does it fail in the proof? The base step or the inductive step?"
It can fail in either step. I'll note that your source on The Deduction Theorem uses an axiomatic context. Suppose we have some system with modus ponens still in place.
First, suppose that the well-formed formula (A -> (B -> A)) does not qualify as provable in the system. Then, the part of the meta-proof for the base case does not go through. This is the case in relevance logic.
Second, suppose that the well-formed formula ((A -> (B -> C)) -> ((A -> B) -> (A -> C))) does not qualify as provable in the system, but (A -> (B -> A)) does qualify as provable. Then, the base case will go through, but then case iv. of the inductive step does not go through. This is the case in 3-valued Lukasiewicz logic, and in infinite-valued Lukasiewicz logic.