Implication and the Deduction theorem

Question

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?

Answer 1

Add first question: Indeed, in classical logic it is enough to consider functionally complete sets of connectives like $\{\vee,\neg\},\{\to\neg\},\{\downarrow\}$. whereas intuitionistic logic is a different matter. Here you usually start with $\{\to,\vee,\wedge,0\}$ (which are mutualy nondefinable) and you consider negation as defined $\neg x:=x\to0$. Note that type theory is usually based on intutionistic logic, not classical!

Add second one: you are right that in the presence of weakening one side of the deduction theorem is trivial. If you have any propositional logic (with $\to$ in language) which is given by some hilbert style presentation with the only rule being modus ponens (if $A$ and $A\to B$, then $B$). Then it satisfies the deduction theorem if and only if it proves the two well known theorems.

• Weekening $A\to(B\to A)$, and
• Transivity/exchange: $(A\to(B\to C))\to ((A\to B)\to(A\to C)) $

It follows that $\to$-fragment of intuituionistic logic is the weakest among such logics.

Try to follow the basic proof of DT where you use the induction on the lenght of the proof and see the essentiality of these rules. The above mentioned proof is not difficult.

Answer 2

I think these should really be two separate questions.

Re: your first question, in classical logic, implication is indeed definable from $\vee$ and $\neg$, so if you want to dispense with it, you can. (Of course, you can also go the other way, and keep implication and dispense with $\vee$!)

I don't understand your comment about types and constructors. While the distinction you mention is real (if I recall correctly) in intuitionistic logic, it doesn't exist in classical logic. In classical logic the sentences "$A\rightarrow B$" and "$\neg A\vee B$" are indeed equivalent.

---

Re: your second question, look at Carl Mummert's answer to the first linked question. The proof of the deduction theorem breaks down right at the base case: $A\vdash B$ is true in his system, but $\vdash A\rightarrow B$ is not.

Answer 3

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