MathOverflow will be down for maintenance for approximately 3 hours, starting Monday evening (06/24/2013) at approximately 9:00 PM Eastern time (UTC-4).

2 edited body

To add to Joel's answer, in the most common theories (for instance, ordinary first-order logic), these are equivalent (by the deduction theorem), but there are plenty of theories where they aren't.

One classic example is conventional model modal logic, where

$\vdash\phi$

............

$\vdash\Box\phi$

is a rule, but $\phi\rightarrow\Box\phi$ is definitely not provable. It we interpret $\Box\phi$ as "$\phi$ is true in all situations", it's clear why: if $\phi$ is a logical tautology, it will always be a logical tautology, and therefore always true. But something true of a particular situation need not be true in all situations.

There are similar situations in certain subsystems of second order arithmetic (note that, despite the name, this is a first-order theory with two types); there are theories where the deduction theorem fails because "from $\phi$ infer $\phi'$" is added as a rule, but the axiom $\phi\rightarrow\phi'$ is not. (And why would we do this? Because we don't want $\phi'$ to contain free variables---probably set variables---which could appear in premises to $\phi$; that is, we don't want to allow the deduction from $\psi\rightarrow\phi$ to $\psi\rightarrow\phi'$ where $\psi$ and $\phi'$ might share free set variables.)

1

To add to Joel's answer, in the most common theories (for instance, ordinary first-order logic), these are equivalent (by the deduction theorem), but there are plenty of theories where they aren't.

One classic example is conventional model logic, where

$\vdash\phi$

............

$\vdash\Box\phi$

is a rule, but $\phi\rightarrow\Box\phi$ is definitely not provable. It we interpret $\Box\phi$ as "$\phi$ is true in all situations", it's clear why: if $\phi$ is a logical tautology, it will always be a logical tautology, and therefore always true. But something true of a particular situation need not be true in all situations.

There are similar situations in certain subsystems of second order arithmetic (note that, despite the name, this is a first-order theory with two types); there are theories where the deduction theorem fails because "from $\phi$ infer $\phi'$" is added as a rule, but the axiom $\phi\rightarrow\phi'$ is not. (And why would we do this? Because we don't want $\phi'$ to contain free variables---probably set variables---which could appear in premises to $\phi$; that is, we don't want to allow the deduction from $\psi\rightarrow\phi$ to $\psi\rightarrow\phi'$ where $\psi$ and $\phi'$ might share free set variables.)