# Questions tagged [natural-deduction]

For questions concerning natural deduction, a formal proof system studied in proof theory. A natural deduction proof starts with a set of premises and applies introduction and elimination rules to arrive at the conclusion. This tag is not specific to any particular logic, classical or intuitionistic, propositional or allowing quantifiers.

891 questions
Filter by
Sorted by
Tagged with
42 views

• 4,741
36 views

### Given the following rule for implication-introduction, is this the same rule that discharges assumptions? [duplicate]

The following is an example that my teacher came up with during one of our earlier lectures on natural deduction. "Given the rules of inference that we have introduced so far, reflect on whether ...
• 55
85 views

### Tips on initial assumptions for proofs using natural deduction - with a specific example.

Here is a question that's been bugging me: "Derive the following, using the rules of natural deduction: $$\vdash \neg(P_{1} \rightarrow P_{2}) \rightarrow P_{1} \vee P_{2}$$ That is, give a ...
• 55
103 views

### How to prove that $P_b \leftrightarrow (P_a \land P_b), P_a \leftrightarrow \neg P_b \vdash P_a$ with natural deduction

I need to build a proof for $P_b \leftrightarrow (P_a \land P_b), P_a \leftrightarrow \neg P_b \vdash P_a$ with natural deduction... I have built the following proof, however I am stuck in the middle ...
• 17
72 views

### How to build a proof for $\vdash \exists y \forall x P(x,y) \rightarrow \forall x \exists y P(x,y)$ using the software Fitch

I want to build a proof for $\vdash \exists y \forall P(x,y) \rightarrow \forall x \exists y P(x,y)$ using the software Fitch... I have the above proof and I want to test it to be sure I have done ...
• 17
233 views

### How to prove that $\vdash \exists y \forall x P(x,y) \rightarrow \forall x \exists y P(x,y)$ with natural deduction in tree style

I have built the following proof for $\vdash \exists y \forall x P(x,y) \rightarrow \forall x \exists y P(x,y)$ with natural deduction in tree style. However, I am stuck in the middle of the problem.....
• 17
91 views

### ¬A → B , ¬B ⊢ A [closed]

not A > B :PR not B :PR PR = Premises This is the strategy of the Conditional Introduction. On line 3 I'm assuming the antecedent of my goal sentence. (You don’t have to use this vv but it’s what ...
• 19 