1
$\begingroup$

(This is an assignment)

To prove:

$$\frac{\Gamma \vdash_N B}{\Gamma, A \vdash_N B}$$

($\Gamma, A = \Gamma \cup \{A\}$)

I have what I think is a proof for this. I would like and be grateful for some feedback.

Axioms:

A0: $\Gamma \vdash_N B$, whenever $B \in \Gamma$

A1: $\Gamma \vdash_N A → (B → A)$

A2: $\Gamma \vdash_N (A → (B → C)) → ((A → B) → (A → C))$

A3: $\Gamma \vdash_N (\neg B → \neg A) → (A → B)$

Proof rule: Modus Ponens

Proof

By induction on the length of the proof of $\Gamma \vdash_N B$.

Base cases: length 1, axioms:

A0 :: If $ B \in \Gamma$, then $B \in \Gamma \cup \{A\} $

A1 - A3 :: same argument as for A0

MP :: $$\frac{\Gamma \vdash_N C ; \Gamma \vdash_N C → B}{\Gamma \vdash_N B} $$

IH : $\Gamma, D \vdash_N C$

IH : $\Gamma, D \vdash_N C → B$

1: $\Gamma, D \vdash_N C$ (IH)

2: $\Gamma, D \vdash_N C → B$ (IH)

3: $\Gamma, D \vdash_N B$ (MP: 1,2)

Since $D$ is arbitrary: $A = D$, so

$\Gamma, A \vdash_N B$

as we were after.

$\endgroup$
1
  • $\begingroup$ Your proof seems to me more complex than necessary. I suppose that you have a definition of $\Gamma \vdash B$; it must be teh definition of derivation, i.e. a finite sequence of formulas $D_1, ..., D_n$ where $D_n$ is $B$ and for each $D_i$ ($i \le n$) we have three possible cases : (i) $D_i$ is an axiom, or (ii) $D_i \in \Gamma$ or (iii) exists $j,k < i$ such that $D_k$ is $D_j \rightarrow D_i$. If so, the def of derivation does not force us "to use" all formulas in $\Gamma$. So the above derivation of $B$ from $\Gamma$ is still a derivation of $B$ if we add $A$ to $\Gamma$. $\endgroup$ Mar 8, 2014 at 20:15

1 Answer 1

1
$\begingroup$

Your proof seems valid. You probably could have avoided a completely formal proof by noticing the following fact:

The notation $\Gamma\vdash B$ means that $B$ belongs to $Con(\Gamma)$ - the inductive set generated by the basis: $\mathcal{B}_1=\{A_0,A_1,A_2,A_3\}\cup \Gamma$, and the operation: $\{MP\}$. The notation $\Gamma,A\vdash B$ means that $B$ belongs to $Con(\Gamma \cup \{A\})$ the inductive set generated by the basis: $\mathcal{B}_2=\{A_0,A_1,A_2,A_3\}\cup \Gamma \cup \{A\}$, and the operation: $\{MP\}$.

It is a general result is set theory that "if you start with a larger basis, you will end up with a larger set", formally, in this case since $\mathcal{B}_1 \subseteq \mathcal{B}_2$ then $Con(\Gamma)\subseteq Con(\Gamma \cup \{A\})$ which means: $\Gamma\vdash B\Rightarrow\Gamma,A\vdash B$.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .