5 votes
Accepted

Explanation of implication-introduction rule

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. ...
user avatar
3 votes

Explanation of implication-introduction rule

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 ...
user avatar
3 votes
Accepted

Predicate Logic - Natural Deduction; Assumptions about exists-elimination

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 \...
user avatar
  • 5,214
3 votes
Accepted

Algorithm for automatic construction of natural deduction proofs

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 ...
user avatar
2 votes
Accepted

Formal Logic - Natural deduction: Problem with assumptions about exists-negation

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 ...
user avatar
  • 13.3k
2 votes
Accepted

Natural deduction: understanding bottom elimination (¬e)

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$ ...
user avatar
  • 28.4k
1 vote
Accepted

Some explanations needed about Negation in Gentzen's Natural Deduction rules

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 ...
user avatar
  • 1,483
1 vote

Predicate Logic - Natural Deduction; Assumptions about exists-elimination

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 ...
user avatar
  • 131

Only top scored, non community-wiki answers of a minimum length are eligible