Tag Info

Every assumption that is introduced between brackets has to be discharged at some point for the proof to be complete. Otherwise, we could prove that $A$ is true for any given $A$ as follows. [A]¹ ─── A This proof is incorrect, we have not discharged the initial assumption. The following proof of $A\to A$ would be correct, as it discharges the assumption (...

I recommend Mario Román's answer, particularly the connection to the lambda calculus, but I'll add a third perspective. I dislike the natural deduction notation, but I do like the natural deduction rules of inference. Instead, I prefer a notation more like the one used in the sequent calculus, and nothing stops us from using that notation with the rules of ...

In order to eliminate $\exists x$ i must thus have a formula $\exists x \phi$ as my premise, and the other premise as described in the link above. However, my first premise in this case is $S \to \exists x Q(x)$, which makes me think my second move is illegal. Exactly right. Your second move was illegal for the reason you said. The problem is a bit tricky ...

Usually we require the theorems of a proof system to be recursively enumerable, so you can at least write an algorithm that will eventually produce a proof of any theorem. This is usually a relatively easy algorithm to implement. Of course, if you give it something that is a non-theorem, you won't be able to tell with this approach. For classical ...

It is a bit hard to say exactly which introductions you should perform since we don't have your rule set, but I think the over all strategy should be as follows: From $\neg (S \lor (P \to Q))$ you get $\neg (P \to Q)$. Since you have $\neg Q$, you should try to introduce $\neg P$ and thus obtain $P \to Q$. That should be a contradiction and you can ...

Usually in practice we weld the two steps together and just say that from $p$ and $\lnot p$ anything follows, but in formal logic this is a combination of two rules of inference: $p$ and $\lnot p$ both together entail falsehood $\bot$, from $\bot$ anything follows. These are precisely lines 9 and 10 in your proof. We often take $\lnot p$ to be an ...

I'm guessing your first rule is: \begin{align*} &[A]\\ &~~\vdots\\ &~\bot\\ &\overline{\lnot A}\qquad (I\lnot) \end{align*} This means that in order to derive $\lnot A$ one must first assume $A$ (that is $[A]$) and derive a contradiction ($\bot$), the dots between mean a finite number of steps. $$ \frac{A \quad \lnot A}{D} \qquad (E\...

I don't believe the Existential elimination in your step two is correct. On page 16 of your text, the $\phi$ is scoped within the Existential Quantifier expression, and you've tried to eliminate it in the scope of the implication $S \rightarrow \exists x Q(x) $. I believe you can use a subproof to show $\exists x Q(x) \dashv \vdash Q(x_0)$. I.e. That the ...