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.

Filter by
Sorted by
Tagged with
1 vote
1 answer
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: ...
user avatar
  • 11
0 votes
0 answers
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 ...
user avatar
0 votes
3 answers
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 ...
user avatar
3 votes
1 answer
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 (...
user avatar
  • 1,727
-1 votes
0 answers
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 ...
user avatar
0 votes
0 answers
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 ∀(_) ...
user avatar
0 votes
1 answer
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, ...
user avatar
0 votes
1 answer
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 ...
user avatar
1 vote
2 answers
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 ...
user avatar
-2 votes
0 answers
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.
user avatar
  • 1
3 votes
2 answers
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 ...
user avatar
  • 4,666
0 votes
0 answers
45 views

A natural deduction proof of $\neg (A \wedge B) \rightarrow (A \rightarrow \neg B)$ without RAA

I am doing (for fun) the exercices of this lean tutorial. For the third exercice of section 3.6. Exercises: "Give a natural deduction proof of $\neg (A \wedge B) \rightarrow (A \rightarrow \neg ...
user avatar
  • 4,666
0 votes
1 answer
33 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 ...
user avatar
  • 55
0 votes
0 answers
36 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 ...
user avatar
  • 55
0 votes
1 answer
67 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 ...
user avatar
0 votes
1 answer
64 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 ...
user avatar
0 votes
1 answer
157 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.....
user avatar
-2 votes
1 answer
49 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 ...
user avatar
  • 19
0 votes
1 answer
68 views

Derivation (¬¬A → A) → (¬¬B → B) → ¬¬(A ∧ B) → A ∧ B.

I am struggling trying to make a derivation of this principle of indirect proof. Starting with the needed assumptions: u: ¬¬A → A v:¬¬B → B w: ¬¬(A ∧ B) I thought that in order to prove A ∧ B I ...
user avatar
0 votes
1 answer
52 views

Natural Deduction with Identity

I am confused on how to deal with identities in natural deduction proofs with predicate logic. More specifically, how would one go about solving this? ...
user avatar
0 votes
1 answer
97 views

Please explain these counter-interpretations to these Natural Deduction arguments

I have attached a screenshot of the arguments, but here they are written out just in case. I am able to prove when sentences are equivalent, but could somebody please explain the counter-...
user avatar
2 votes
2 answers
72 views

Finding three formulas such that they are consistent as pairs, but inconsistent when all three are together.

This problem and several others of a similar nature have shown up in my textbook in introductory logic: "Give formulas $\phi, \psi, \sigma$ such that any pairing of them defines a consistent ...
user avatar
  • 55
2 votes
1 answer
62 views

A simple problem involving natural deduction - so what am I doing wrong?

The problem is straight-forward. I'm supposed to derive the following in propositional logic, using natural deduction: $$ \lnot (A \wedge B) \vdash \lnot A \vee \lnot B $$ Here is my initial attempt ...
user avatar
  • 55
0 votes
0 answers
36 views

How to convert a Gentzen Calculus Formula to a Natural Deduction One

I have a proof on my textbook, which prooves denials of quantified propositions ∀xφ ⊨ ¬∃x¬φ... However it is written in Gentzen calculus style, while what I need it a Natural Deduction style one. Can ...
user avatar
  • 47
1 vote
1 answer
75 views

How to prove that $∀x (p(x) \to ¬ q(x))⊢¬(∃x (p(x)∧q(x)))$ using natural deduction in tree format

I need to prove that using natural deduction in tree format $(\forall x\ p(x)\to \neg q(x)) \vdash \neg (\exists x (p(x)\land q(x)))$ I have built the following proof which is incomplete and I do not ...
user avatar
  • 47
1 vote
2 answers
88 views

What's the name of the rule of inference where we conclude $p$ implies $q$, given the premise $p$ and $q$?

What's the name of the rule of inference where we conclude $p$ implies $q$, given the premise $p$ and $q$? Premise: $p$ and $q$. Conclusion: $p$ implies $q$ (or the converse). What's the name of this ...
user avatar
  • 113
0 votes
0 answers
52 views

Are logical rules logics?

When I asked whether the empty logic (the one on which no argument is valid) is axiomatizable, the consensus was that it is, and that it is axiomatized by a proof system having no rules whatsoever. Is ...
user avatar
2 votes
1 answer
70 views

How do I write a proof for: $\neg p\vdash p\to q$

I haven't seen this question asked here, but I stumbled upon this question while practicing. I couldn't/can't figure it out and it's bugging me, even though it's not mandatory for any exercises, I ...
user avatar
  • 23
1 vote
1 answer
137 views

proof of principle of explosion using natural deduction

That is, I am asked to prove the sequent $A, \neg A \vdash B$ using natural deduction. The inference rules I am allowed to use are: reflexivity, +, $\neg$-elimination, $\vee/\wedge/\to / \...
user avatar
  • 115
1 vote
1 answer
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 ...
user avatar
  • 133
2 votes
1 answer
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.
user avatar
  • 115
-1 votes
1 answer
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
user avatar
0 votes
1 answer
38 views

How do I prove this sequent using natural deduction?

I want to prove the following using natural deduction: $\quad ∃𝑥(𝐹 (𝑥)) → ∃𝑥(K (𝑥)) ⊢ ∃𝑥(K (𝑥)) ∨ ∀𝑥(¬𝐹 (𝑥)) $ If I were to rewrite $ ∃𝑥(𝐹 (𝑥)) → ∃𝑥(K (𝑥))$ to $ ¬∃𝑥(𝐹 (𝑥)) ∨ ∃𝑥(K (...
user avatar
  • 1
0 votes
1 answer
98 views

Prove using minimal logic that $\neg\neg\neg A \rightarrow \neg A$

Prove using natural deduction for minimal logic that $\neg\neg\neg A \rightarrow \neg A$. I'm trying to prove this argument using only the rules of minimal logic. So far I have this. $$1. ⊢ \neg\neg\...
user avatar
  • 133
1 vote
1 answer
64 views

Natural deduction via completeness theorem

I have some question about how to use completeness theorem, I need to show the follow: Let $\Sigma$ be a consistent set of propositions and $\phi, \psi$ formulas. Show that If $\Sigma\not\vdash \phi$ ...
user avatar
  • 688
0 votes
0 answers
45 views

Logical deduction without completeness theorem

I am just learning about deduction and I have to solve the following exercises Let $\Sigma$ be a consistent set of propositions. Which of the following statements are necessarily true? Justify your ...
user avatar
  • 688
4 votes
1 answer
156 views

Proof of double negation elimination using natural deduction

I am trying to prove that $\neg A \to \bot \vdash A$, I can only use double negation elimination to get the conclusion, but I don't know how to prove double negation elimination. Below is my proof for ...
user avatar
  • 115
1 vote
1 answer
175 views

Natural Deduction Proof search algorithm for Classical Propositional logic?

I know of two algorithms for determining classical propositional validity: Convert the problem into a SAT problem, run a SAT solver. These algorithms are efficient, but it seems difficult/infeasible ...
user avatar
1 vote
1 answer
47 views

Help in proving ∀x(¬A(x) → B(d)) ⊢ ∀xA(x) ∨ B(d) without using Disjunctive syllogism in the proof

Stuck on a problem of ∀x(¬A(x) → B(d)) ⊢ ∀xA(x) ∨ B(d), however the system I am using does not allow me to use DS in the proof. Here is another method I tried, but it says that it's wrong on the last ...
user avatar
1 vote
0 answers
41 views

Natural Deduction and Sequent Calculus

Are there any good natural deduction and sequent calculus solvers online for both predicate and propositional logic? Or perhaps forums that specialise in these proof systems?
user avatar
2 votes
1 answer
62 views

Natural deduction and introduction of universal quantifier

I have a hard time with quantification introduction and elimination ; for instance, if I want to prove $$\forall x \quad (Px\rightarrow Px ) $$ I am tempted to do the following : $$\underline{[Py]}_{\,...
user avatar
  • 4,666
1 vote
1 answer
76 views

Show that $∃x[∀yLxy ⇔ ∃z¬Lxz]$ is a contradiction.

I know that to prove contradiction, I need to prove that $∃x[∀yLxy ⇔ ∃z¬Lxz]$ can derive $y$ & not $y.$ I got stuck at formulating the contradiction, because I don't know if $∀yLxy$ is the same as ...
user avatar
  • 21
0 votes
2 answers
111 views

Prove statement using natural deduction rules for propositional logic: $((q → p) → q) → q$ [duplicate]

$$((q → p) → q) → q$$ There are no premises which makes this problem very difficult for me. What I tried was assuming that the whole left side $((q → p) → q)$ then I assumed $¬q$ and tried to find a ...
user avatar
0 votes
0 answers
50 views

Natural deduction: premise with simultaneous negated universal and existential quantifiers

I need to prove this natural deduction theorem: $\neg \exists x.\neg \forall y.S_{1}^{1}(x) \implies S_{2}^{1}(y) \lor S_{3}^{1}(y)$, $S_{1}^{1}(c_1)$, $\neg S_{2}^{1}(c_2)$ $\vdash_{N} \exists z. S_{...
user avatar
1 vote
3 answers
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 ...
user avatar
0 votes
1 answer
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 ...
user avatar
1 vote
2 answers
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 ...
user avatar
-1 votes
1 answer
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 ...
user avatar
0 votes
2 answers
162 views

How can I solve the Disjunctive Syllogism P ∨ Q , -Q ⊢ P

I am trying to figure this out but am stuck. I've gotten this far: 1(1) PvQ A 2(2) -Q A 3(3) Q A 2,3(4) -Q^Q 2,3 ^I Am not sure how to derive P using propositional logic rules. (-E,-I,->I,->E,^...
user avatar
1 vote
2 answers
139 views

Natural deduction, beginning premises

For natural deduction. how do i go about picking how to start off my proof and is there any rules as to how i have to start off my proof. Do i have to individually prove each premise as that's not ...
user avatar

1
2 3 4 5
18