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.
...
- 281
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 ...
- 11.8k
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 \...
- 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 ...
- 11.8k
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 ...
- 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$ ...
- 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 ...
- 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 ...
- 131
Only top scored, non community-wiki answers of a minimum length are eligible