Not sure about your first question: (So I don't even bother about the second)
What does $K \cup \{ \lnot A \}$ mean if there is no deduction theorem?
- Is A an extra axiom and all universal substitutions of $ \lnot A $ also part of $K \cup \{ \lnot A \}$?
Then the system itself is inconsistent and nothing else is to do.
- Or is $ \lnot A $ a singular (extra logical) true formula?
That also doesn't make any sense, you have allready declared it true so it isn't anything else.
Without the deduction theorem you don't have hypothesis so $K \cup \{ \lnot A \}$ has no meaning other than K itself (assuming that K is description of an axiom system)
But having said that maybe you just mean that 1) and 2) are true formula's
1) $ (K \land \lnot A) \to C $
2) $ (K \land \lnot A) \to \lnot C $
Then with a little frobelen (exportation) you can get
3) $ K \to ( \lnot A \to C ) $
4) $ K \to ( \lnot A \to \lnot C) $
what can make(adjunction)
5) $ K \to ((\lnot A \to C ) \to (\lnot A \to \lnot C )) $
and that with help of axiom (A3) that becomes:
6) $ K \to A $
maybe this helps
You are right to suspect that your described method does not work to prove the Deduction Theorem: if you simply extend the existing deduction of $B$ from $\Delta \cup \{ A \}$ by adding $B \rightarrow (A \rightarrow B)$ (from axiom 1) and then getting $A \rightarrow B$ through Modus Ponens, then all you have ended up showing is that there is a deduction of $\Delta \cup \{ A\} \vdash A \rightarrow B$, because the original set of premises is still $\Delta \cup \{ A \}$. And you can't just throw out the $A$, since in the extended derivation, you still need to get to $B$ by itself, which may well depend on $A$.
So ... you need to do something else to show $\Delta \vdash A \rightarrow B$
Here is what you need to do. Transform the deduction of $\Delta \cup \{A \} \vdash B$ into a deduction of $\Delta \vdash A \rightarrow B$ by showing how you can get a deduction $\Delta \vdash A \rightarrow \varphi_i$ for $\varphi_i$ of the original deduction. And that you can show by strong induction, where you have to consider that every $\varphi_i$ comes about as one of the three cases: as an element of $\Delta$, an instance of some axiom, or by the use of Modus Ponens.
Here is a simple example:
If we take that $\Delta = \{ A \rightarrow B \}$, then we know that $\Delta \cup \{ A \} \vdash B$, i.e. that $\{ A \rightarrow B, A \} \vdash B$. Indeed, here is a derivation for that:
\begin{array}{ccc}
1 & A \rightarrow B & Given\\
2 & A & Given\\
3 & B & \text{Modus Ponens } 2,3
\end{array}
OK, so now we want to convert this to a derivation of $\Delta \vdash A \rightarrow B$, i.e. of $\{ A \rightarrow B \} \vdash A \rightarrow B$
Now, there is of course a very simple derivation for $\{ A \rightarrow B \} \vdash A \rightarrow B$, but what I want to show below is that we can systematically convert the earlier derivation of $\{ A \rightarrow B, A \} \vdash B$ into a new derivation of $\{ A \rightarrow B \} \vdash A \rightarrow B$
Again, the basic idea is that, since we are 'pulling out' $A$ from the set of assumptions, in the new derivation we want to get a statement of the form $A \rightarrow \varphi_i$ for every line $\varphi_i$ from the original derivation. Think of this as 'conditionalizing' every statement with the condition $A$. So, the basic scheme for the derivation will look like:
\begin{array}{ccc}
..\\
k & A \rightarrow (A \rightarrow B) & ??\\
..\\
l & A \rightarrow A & ??\\
..\\
m & A \rightarrow B & ??
\end{array}
Now, notice that the last line is $A \rightarrow B$, which is exactly what we are trying to get, so that's already good. But of course, we have yet to figure out how to actually get there. In fact, let's first enter the givens, which are all the same givens as in the original derivation, excvept for $A$, since that's the one we're 'pulling out':
\begin{array}{ccc}
1 & A \rightarrow B & Given\\
..\\
k & A \rightarrow (A \rightarrow B) & ??\\
..\\
l & A \rightarrow A & ??\\
..\\
m & A \rightarrow B & ??
\end{array}
OK, now, note that we put down line $k$ exactly because we had line $1$ as a given in the original derivation. That is, for tevery $\varphi_i \in \Delta$, we put down, and are trying to get to, $A \rightarrow \varphi_i$ .. how can we do that? Easy: just exploit axiom $1$:
\begin{array}{ccc}
1 & A \rightarrow B & Given\\
2 & (A \rightarrow B) \rightarrow (A \rightarrow (A \rightarrow B)) & \text{ Axiom } 1\\
3 & A \rightarrow (A \rightarrow B) & \text{ Modus Ponens } 1,2 \\
..\\
l & A \rightarrow A & ??\\
..\\
m & A \rightarrow B & ??
\end{array}
Now, the $A \rightarrow A$ is because the $A$ was in the original set of givens as well, but since in the new derivation we no longer have $A$ as a given, we need to derive $A \rightarrow A$ in a different way. But, as you found, such a derivation can always be done:
\begin{array}{ccc}
1 & A \rightarrow B & Given\\
2 & (A \rightarrow B) \rightarrow (A \rightarrow (A \rightarrow B)) & \text{ Axiom } 1\\
3 & A \rightarrow (A \rightarrow B) & \text{ Modus Ponens } 1,2 \\
4 & (A \rightarrow ((A \rightarrow A) \rightarrow A) \rightarrow ((A \rightarrow (A \rightarrow A)) \rightarrow (A \rightarrow A)) & \text{ Axiom } 2\\
5 & A \rightarrow ((A \rightarrow A) \rightarrow A) & \text{ Axiom } 1\\
6 & (A \rightarrow (A \rightarrow A)) \rightarrow (A \rightarrow A) & \text{ Modus Ponens } 4,5 \\
7 & A \rightarrow (A \rightarrow A) & \text{ Axiom } 1\\
8 & A \rightarrow A & \text{ Modus Ponens } 6,7 \\
..\\
m & A \rightarrow B & ??
\end{array}
OK, almost done. Now we need to show how line $m$ can be derived from the original lines $k$ and $l$, i.e. lines $3$ and $8$. Well, for this you use axiom 2. That is, since in the original derivation we went from $A \rightarrow B$ and $A$ to $B$ via Modus Ponens, in the new derivation we need to do this using the conditionalized statements, i.e. we need to go from $A \rightarrow (A \rightarrow B)$ and $A \rightarrow A$ to $A \rightarrow B$. How do we do this? Well, this is exactly what Axiom 2 is for: Axiom 2 always looks a ittle weird if you first see it, but Axiom 2 is actually the embodiment of this kind of 'conditionalized Modus Ponens'. Here is how it goes:
\begin{array}{ccc}
1 & A \rightarrow B & Given\\
2 & (A \rightarrow B) \rightarrow (A \rightarrow (A \rightarrow B)) & \text{ Axiom } 1\\
3 & A \rightarrow (A \rightarrow B) & \text{ Modus Ponens } 1,2 \\
4 & (A \rightarrow ((A \rightarrow A) \rightarrow A) \rightarrow ((A \rightarrow (A \rightarrow A)) \rightarrow (A \rightarrow A)) & \text{ Axiom } 2\\
5 & A \rightarrow ((A \rightarrow A) \rightarrow A) & \text{ Axiom } 1\\
6 & (A \rightarrow (A \rightarrow A)) \rightarrow (A \rightarrow A) & \text{ Modus Ponens } 4,5 \\
7 & A \rightarrow (A \rightarrow A) & \text{ Axiom } 1\\
8 & A \rightarrow A & \text{ Modus Ponens } 6,7 \\
9 & (A \rightarrow (A \rightarrow B))\rightarrow ((A \rightarrow A) \rightarrow (A \rightarrow B)) & \text{ Axiom } 2\\
10 & (A \rightarrow A) \rightarrow (A \rightarrow B) & \text{ Modus Ponens } 3,9 \\
11 & A \rightarrow B & \text{ Modus Ponens } 8,10
\end{array}
.... and we're done!
OK, so this was just a simple example, but I think you can see how this general technique always works: Your goal is to conditionalize all statements from the original derivation with the '$A$' that you pull out, and you derive those as follows:
Derive $A \rightarrow A$ for that $A$.
Derive $A \rightarrow \varphi_i$ for every $\varphi_i \in \Delta$ using the $\varphi_i$ you still have as a given in the new derivation, and using axiom 1.
Derive any $A \rightarrow \varphi_k$ where in the original derivation $\varphi_k$ was derived using Modus Ponens from earlier $\varphi_i$ and $\varphi_j = \varphi_i \rightarrow \varphi_k$ from the conditionalized $A \rightarrow \varphi_i$ and $A \rightarrow \varphi_j = A \rightarrow (\varphi_i \rightarrow \varphi_k)$ using axiom 2
Best Answer
The statement is known as Peirce's Law, and the proof is pretty nasty. I can believe someone can spend $10$ years on it without cracking it!
The proof uses some helpful Lemma's.
First, let's prove: $\phi \to \psi, \psi \to \chi, \phi \vdash \chi$:
$\phi \to \psi$ Premise
$\psi \to \chi$ Premise
$\phi$ Premise
$\psi$ MP 1,3
$\chi$ MP 2,4
By the Deduction Theorem, this gives us Hypothetical Syllogism (HS): $\phi \to \psi, \psi \to \chi \vdash \phi \to \chi$
Now let's prove the general principle that $\neg \phi \vdash (\phi \to \psi)$:
$\neg \phi$ Premise
$\neg \phi \to (\neg \psi \to \neg \phi)$ Axiom1
$\neg \psi \to \neg \phi$ MP 1,2
$(\neg \psi \to \neg \phi) \to (\phi \to \psi)$ Axiom2
$\phi \to \psi$ MP 3,4
With the Deduction Theorem, this means $\vdash \neg \phi \to (\phi \to \psi)$ (Duns Scotus Law)
Let's use Duns Scotus to show that $\neg \phi \to \phi \vdash \phi$ (Law of Clavius):
$\neg \phi \to \phi$ Premise
$\neg \phi \to (\phi \to \neg (\neg \phi \to \phi))$ (Duns Scotus Law)
$(\neg \phi \to (\phi \to \neg (\neg \phi \to \phi))) \to ((\neg \phi \to \phi) \to (\neg \phi \to \neg (\neg \phi \to \phi)))$ Axiom3
$(\neg \phi \to \phi) \to (\neg \phi \to \neg (\neg \phi \to \phi))$ MP 2,3
$\neg \phi \to \neg (\neg \phi \to \phi)$ MP 1,4
$(\neg \phi \to \neg (\neg \phi \to \phi)) \to ((\neg \phi \to \phi) \to \phi)$ Axiom2
$(\neg \phi \to \phi) \to \phi$ MP 5,6
$\phi$ MP 1,7
Using Duns Scotus and the Law of Clavius, we can now show that $ (\phi \to \psi) \to \phi \vdash \phi$:
$(\phi \to \psi) \to \phi$ Premise
$\neg \phi \to (\phi \to \psi)$ Duns Scotus
$\neg \phi \to \phi$ HS 1,2
$\phi$ Law of Clavius 3
And so finally, by the Deduction Theorem, we have: $\vdash ((\phi \to \psi) \to \phi) \to \phi$