Calculas F0 - Deduction Theorem

Question

By using the deduction theorem, and other formulas (i.e Transitivity of implication, inconsistency, double negation etc.) we can prove something like below.

$⊢(¬q→¬(q→r))→¬¬q$

By applying deduction theorem, it is sufficient to show $(¬q→¬(q→r))⊢¬¬q$.

My question is, what is the rule to make assumptions to do the proof?

i.e I found below example from a book

${A→(B→C),B,A} ⊢ C$

steps

${A→(B→C),B,A} ⊢ A$ Assumption

${A→(B→C),B,A} ⊢ A→(B→C)$ Assumption

${A→(B→C),B,A} ⊢ (B→C)$ Assumption

and so on.

I want to know how can I make those assumptions? What is the theory behind it? It would be nice if someone can explain it using this problem $⊢(¬q→¬(q→r))→¬¬q$.

Answer 1

Typically, the Assumption rule is that at any point in the proof you can add a line that looks like:

$\{ \varphi \} \vdash \varphi$ Assumption

So your example is a bit weird. It would make more sense as:

1. $\{ A \} \vdash A$ Assumption

2. $\{ A \rightarrow (B \rightarrow C) \} \vdash A \rightarrow (B \rightarrow C)$ Assumption

3. $\{ A, A \rightarrow (B \rightarrow C) \} \vdash B \rightarrow C$ MP 1,2

etc.

Answer 2

The assumptions are listed to the left of the $\vdash$ symbol. That is, statement $$\{A, B, \ldots \} \vdash C$$ means $C$ is provable from the assumptions $A, B, \ldots$. In particular this is true "by assumption" if $C$ is one of $A, B, \ldots$.

Answer 3

\begin{array}{rcll} \{A→(B→C),B,A\} &⊢& A &\text{Assumption}\\[2ex] \{A→(B→C),B,A\} &⊢& A→(B→C) &\text{Assumption}\\[1ex] \{A→(B→C),B,A\} &⊢& (B→C) &\require{cancel}\cancelto{\text{Modus Ponens}}{\text{Assumption}}\\ \end{array}

The "Assumptions" here are really just the rule of identity: $\Sigma\cup\{\phi\}\vdash \phi$.

The other rule is modus ponens, $\frac{\Gamma\vdash \phi\quad\Delta\vdash \phi\to\psi}{\Gamma\cup\Delta\vdash \psi}$ , or "conditional eliminaton".

$\begin{array}{r:rcll} 1&\{A\} &⊢& A &\text{Assumption}\\[1ex] 2&\{A→(B→C)\} &⊢& A→(B→C) &\text{Assumption}\\[1ex] 3&\{A→(B→C),A\} &⊢& (B→C) &\text{Modus Ponens},1,2 \\[1ex] 4&\{B\} &⊢& B &\text{Assumption}\\[1ex] 5&\{A→(B→C),B,A\} &⊢& C &\text{Modus Ponens}, 3,4\\[1ex] \end{array}$