1. ## The system L

How do we show that $\displaystyle A \vdash_L \neg \neg A$ without giving a derivation?

I know that the derivation for $\displaystyle \neg \neg A \vdash_L A$ is trivial, but the derivation of $\displaystyle A \vdash_L \neg \neg A$ is pretty long. But the question is how to show that without presenting a derivation. How can we do that? Any help and suggestions are greatly appreciated.

The system L: http://img405.imageshack.us/img405/4208/systemli.jpg

2. ## Re: The system L

Originally Posted by demode
How do we show that $\displaystyle A \vdash_L \neg \neg A$ without giving a derivation?
$\displaystyle A\rightarrow \neg \neg A$ is clearly a tautology wich implies (Adequacy Theorem) $\displaystyle \vdash_L (A\rightarrow\neg \neg A)$ . But according to the converse of the Deduction Theorem, $\displaystyle A \vdash_L \neg \neg A$ .

3. ## Re: The system L

The converse of the Deduction theorem is, of course, just an application of Modus Ponens.

Weak completeness theorem says that all tautologies are derivable. In contrast, strong completeness theorem says that all logical consequences of an arbitrary set of formulas are derivable from this set. One gets weak completeness when the set of formulas is empty. Therefore, it is enough to use strong completeness theorem here.

Edit: Strong completeness follows trivially from weak completeness for a finite set of assumptions because they can be turned into premises of an implication.

4. ## Re: The system L

Originally Posted by emakarov
The converse of the Deduction theorem is, of course, just an application of Modus Ponens.

Weak completeness theorem says that all tautologies are derivable. In contrast, strong completeness theorem says that all logical consequences of an arbitrary set of formulas are derivable from this set. One gets weak completeness when the set of formulas is empty. Therefore, it is enough to use strong completeness theorem here.
Yes, yes. There are several ways of solving a question.