Difference between $\vdash A\to B$ and $A\vdash B$

185 Views Asked by At

Is $\vdash A\to B$ equivalent to $A\vdash B$, in the sense that if you can prove one, then you can prove the other? I would prove the first by taking $A$ as a hypothesis, and then proving $B$. This would yield $A\to B$ with the introduction rule for $\to$. And for the latter I would take $A$ as a premise, and then show $B$.

So my question is: is there an important difference between the two?

2

There are 2 best solutions below

3
On BEST ANSWER

You right that -- in any halfway sensible logic -- it is the case that $\vdash A\to B$ holds if and only if $A\vdash B$ does.

Both forms exist because they are good for different things in the structure of a proof. The form $A\vdash B$ gives you the possibility of applying further rules that depend on the internal structure of $B$ (or, depending on the system, possibly also $A$). These rules would not be able to "see behind" the $\to$ in the $\vdash A\to B$ form.

On the other hand, $\vdash A\to B$ is what you need if you're matching up with a rule that treats $A\to B$ as a unit. For example, if you want to prove $(A\to B)\land(C\to D)$ you would first need to establish $\vdash A\to B$ and $\vdash C\to D$, and then apply a $\land$ rule. The $\land$ rule knows nothing about $\to$ and wouldn't be able to invent a $\to$ from the $A\vdash B$ form by itself.

The form that's what you need for proving something is not always the same as the form you need when using it, so it is necessary to be able to pass from one to the other and vice versa. Fortunately this is pretty easy in most proof systems. (The major exception is Hilbert-style systems where it may take a major rewriting of the derivation of $A\vdash B$ to derive $\vdash A\to B$).

1
On

They usually are, but the details depend on what logical system you are working with.

For instance, if you have the inference rule modus ponens, then it follows that $\vdash A\to B$ implies $A\vdash B,$ since you take $A$ as an assumption, prove $A\to B$ and then use modus ponens to conclude $B.$ In a natural deduction framework, this is just the elimination rule for $\to.$

On the other hand, the fact that $A\vdash B$ implies $\vdash A\to B$ is usually proved as a theorem and called the deduction theorem in the study of Hilbert Style systems (e.g. in Mendelson). In a natural deduction system, it would typically just be an introduction rule for $\to.$

The equivalence is contingent on your formal system having the above features, but most systems of practical import do.