# 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.

863 questions
Filter by
Sorted by
Tagged with
1 vote
68 views

### What strategies could be used to prove the validity of this argument in order to not violate restrictions on universal generalization (Hurley)

I'm considering a particular argument while working through Hurley's Concise Introduction: ...
• 11
30 views

### can I falsify a traditional inference with modern natural deduction like system?

I can represent a traditional syllogism with the language of first-order predicate logic. and If the syllogism is valid, then I can prove it with natural deduction system or tableaux. If the syllogism ...
• 67
90 views

### How to prove $A \to (B \lor C)$ therefore $(A \to B) \lor (A \to C)$? [closed]

In doing this proof I found a solution, but I believe it to be incorrect because within the proof it uses assume A . . . . . assume C . . . A -> C Is it valid to conclude A -> C in the same ...
93 views

### Natural Deduction: An unusual presentation?

1. Context On page 241 of their paper Natural deduction and coherence for weakly distributive categories Blute et al give the right- and left-introduction rules of multiplicative conjunction for (...
• 1,727
32 views

### Proving Identity Laws in Logic using Natural Deduction

We know that there are identity laws in formal proofs in a system of natural deduction like =In, =Out. So, I am stuck at such a problem where we have to prove an equality i.e. q = u using the ...
37 views

### Predicate Logic: Deduction for Quantifiers

So, I was bothered by the question of natural deduction wherein we have to prove ∀h(Fh ⇒ Fk) from premise ∃g Fg ⇒ Fk given that k is a constant which isn't used before To get the conclusion in ∀(_) ...
25 views

### Natural Deduction: Universal Quantifiers in Predicate

How do we prove the conclusion: ∀x(Ax ∨ ⇁Ax) This is also called LEM, i.e. the Law of Excluded Middle. I'm confused while proving this because for ∀x, deduction assuming some constant is required. So, ...
39 views

### Propositional Logic: Natural Deduction using Elimination and Introduction rules

So, we have to prove ⇁Y as conclusion from premises: A. (X ∨ Y) ⇒ (X ∧ Y) B. ⇁X What I’ve tried so far is basically: ⇁X [Premise] ⇁X ∨ (X ∧ Y) [∨In, 1] (X ∨ Y) ⇒ (X ∧ Y) [Premise] . . . n. X ...
1 vote
87 views

### Proving $\exists x\lnot R(x), \forall x(P(x)\to Q(x)), \forall x(\lnot Q(x) \lor R(x)) \vdash \exists x\lnot P(x)$

This is the proof we have to prove: $$\exists x\lnot R(x), \forall x(P(x)\to Q(x)), \forall x(\lnot Q(x) \lor R(x)) \vdash \exists x\lnot P(x)$$ My proof: $∀x(P(x)→Q(x))$ From data $∃x¬R(x)$ From ...
20 views

### Natural Deduction using Inference Rules

Prove by natural deduction that A AND ¬B -> (C -> D) ├ A -> B v ¬C v D You may assume C-> D equivalent to ¬C v D.
89 views

### A natural deduction proof of $\neg (A \leftrightarrow \neg A )$.

I want to prove $\neg (A \leftrightarrow \neg A )$ in natural deduction: I tried first But I can't figure how to discharge the hypothesis $A$ and $\neg A$. I then tried Here I just need to ...
• 4,666
45 views

• 115
1 vote
97 views

### Prove using classical logic that $q \to r, r \to p \vdash_c \neg (\neg p \land q)$

Prove using classical logic that $q \to r, r \to p \vdash_c \neg (\neg p \land q)$ Hello, I'm finding hard to prove this... I've been to use the left implication rule, Modus Tollens, Disjunctive ...
• 133
110 views

### Using limited natural deduction rules to prove de morgan's law

I am trying to prove something reversely, but always get stuck when it comes to $\neg r\wedge \neg q\vdash \neg (r\vee q)$. How can I prove it using the following rules? Here's where I get stucked.
• 115
80 views

### Help with $(P\wedge Q) \vee\neg P \vdash \neg Q \rightarrow \neg P$

$$(P ∧ Q) ∨ ¬P ⊢ ¬Q → ¬P,\qquad P, ¬(¬Q → R) ⊢ ¬(P↔ Q)$$ I am stuck in this, can't wrap my head around it. Need to prove fitch style
38 views

1 vote
102 views

### Complex Natural Deduction proof

How do I provide a Natural Deduction proof for (¬A ∨ ¬B) → (C → A ∧ B)→ ¬C? I know I can work backwards and i managed to get rid of the implications: ¬C (C → A ∧ B)→ ¬C (¬A ∨ ¬B) → (C → A ∧ B)→ ¬C ...
• 19
78 views

### Sequent Calculus vs Natural Deduction

Can I prove all implication proofs like $A \to A$ or $A \to B \to A$ in both Sequent Calculus and Natural Deduction or just in one of them? So for $A \to A$ can I use the right implication ...
1 vote
60 views

### How to prove this: ¬C → B , C → ¬B ⊢ ¬B ↔ C in TFL with natural deduction?

I'm really stuck on how to prove ¬C → B , C → ¬B ⊢ ¬B ↔ C. I know I have $C \implies \sim B$ but in order to introduce the biconditional I have to prove $\sim B \implies C$ and I have no idea how. Any ...
84 views

### How can I solve -P ∧ -Q ⊢ -(P ∨ Q) using deMorgan's Law?

Using propositional logic rules (--E, -I, ^I, ^E, vI, vE, ->I, ->E) how can I solve -P ∧ -Q ⊢ -(P ∨ Q)? I don't know if I'm going in the correct direction. Would appreciate some help in solving ...