Stack Exchange Network

Stack Exchange network consists of 175 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

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.

0
votes
1answer
50 views

how to prove C when given A ∨ (B ∧ C) and A → C [on hold]

can somebody help me to prove this using natural deduction fitch style: A ∨ (B ∧ C), A → C ∴ C here, what i got so far and i dont know if i am on the right track:
1
vote
1answer
32 views

$\vdash\phi \land \diamond\psi \to \diamond(\psi\land\diamond\phi)$ in KB

I've been trying to prove $\vdash\phi \land \diamond\psi \to \diamond(\psi\land\diamond \phi)$ in natural deduction where it's allowed to use $\phi\to \square \diamond \phi$ and/or $\diamond\square\...
1
vote
1answer
39 views

Prove $\vdash \neg(\square F\land p)$ in $KD$

How to prove that $\vdash \neg(\square F\land p)$ in $KD$? The allowed rules are natural deduction rules and the axiom $\square p\to\diamond p$ where $\diamond p=\neg\square\neg p$. I actually don't ...
1
vote
2answers
64 views

Help with natural deduction

I was able to get this one, it was fairly simple. ...
0
votes
0answers
36 views

Proof using natural deduction of $\small\forall x~[A(x)\to\exists y~[B(y)\land C(y,x)]] \vdash\forall x~[\exists y~[A(x)\to(B(y)\land C(y,x))]]$

I am trying to construct a formal proof of the argument: $$\forall x~\Big[A(x)\to\exists y~\big[B(y)\land C(y,x)\big]\Big] ~\vdash~\forall x~\Big[\exists y~\big[A(x)\to(B(y)\land C(y,x))\big]\Big]$$ ...
1
vote
1answer
34 views

Counterexample for the invalidity of the following [closed]

Premise 1: $\quad \exists x \ [A(x) \lor B(x)]$ Premise 2:$\quad \exists x \ \lnot A(x)$ Conclusion: $\quad \exists x \ B(x)$ The argument is invalid, but I can't find a counterexample.
3
votes
1answer
51 views

Don't the natural deduction inference rules assume semantics?

I read that one should separate syntax snd semantics in logic but then how come we have things like this: $a \land b \vdash a$ $a \land b \vdash b$ Which says "If we know $a \land b$ then we also ...
2
votes
2answers
56 views

Is it possible to prove a contradiction with natural deduction by negating the formula?

I want to show that a formula is a contradiction. Assume a very simple one like $$ 1. \exists x Px \land \neg\exists x Px $$ Now negate the formula to $$ 2. \neg(\exists x Px \land \neg\exists x ...
1
vote
1answer
95 views

Can anyone clarify the rules for $\forall$ intro and elimination, and $\exists$ intro and elimination?

I am trying to better understand the introduction and elimination rules for quantifiers and in particular the syntax / proof system aspect. I'm currently using Fitch-style proofs. I asked a recent ...
1
vote
1answer
51 views

Proof with natural deduction [closed]

$(p\rightarrow \bot)\rightarrow \bot \vdash p$ I need to prove this using natural deduction. I tried assuming that $\neg p$ is true, so I can prove $p$ by contradiction. I do not have $\neg p$ ...
0
votes
0answers
50 views

Prove $\vdash ((p\to q)\to p)\to p$ [duplicate]

I'm trying to prove $\vdash ((p\to q)\to p)\to p$: ...
3
votes
2answers
32 views

Formal proof of distributivity of conjuction

I'm trying to prove that $\vdash p\land (q\lor r)\to(p\land q)\lor (p\land r)$ in natural deduction. ...
3
votes
2answers
65 views

Trouble with negation introduction with Fitch natural deduction proof

I've recently posted another question regarding natural deduction proofs and I've definitely made some progress, but I'm now stuck with a proof which seems like it could be flawed. Now as you can see,...
3
votes
3answers
55 views

Formal proof of one of De Morgan's laws

How to give a formal proof of $\vdash \neg (p\land q)\to\neg p\lor \neg q$ in the natural deduction proof system? Here is what I have: ...
2
votes
2answers
48 views

Is this proof in natural deduction proof system correct?

Consider a natural deduction proof system. Suppose I know that $\vdash \phi$ (the sentence $\phi$ is provable from no premises). If I'm proving something like $\vdash \psi$, can I just use that $\phi$ ...
2
votes
2answers
30 views

Natural deduction - formal proof troubles

I'm pretty new to the topic of natural deduction using the Fitch method. I found a very helpful site (http://proofs.openlogicproject.org/) in which you can construct your proofs, but I'm having a lot ...
2
votes
4answers
97 views

Proof of $(P\to Q) \vee (Q\to P)$ with natural deduction

I need to prove the following statement in natural deduction: $$(P\rightarrow Q) \lor (Q\rightarrow P)$$ I tried assuming not (target statement) and assuming the left hand side, but I don't know ...
1
vote
4answers
66 views

Formal Deduction (logic) Question: $\lnot C, (B \to \lnot C) \to A \vdash (A \to C) \to F$

I've been stuck on this question for around two hours now. I'm trying to prove that: $\lnot C, \ (B \to \lnot C)\to A \vdash (A \to C)\to F $ I'm trying to get my second last step to be: $\lnot C,...
1
vote
2answers
79 views

Proving $\exists ! x (t = x)$ constructively without double negation axiom

I am wondering how one would go about this. I am using Hilbert style proof system as described in Kleene's "Introduction to Metamathematics" or "Mathematical logic". I am pretty sure that if you can ...
3
votes
3answers
81 views

How to prove the following formula using an indirect proof

I need to prove that the premise $A \to (B \vee C)$ leads to the conclusion $(A \to B) \vee (A \to C)$. Here's what I have so far. From here I'm stuck (and I'm not even sure if this is correct). My ...
3
votes
1answer
31 views

How can I prove the following with natural deduction rules? ¬∀x∃yP(x,y) ⊢ ∃x∀y¬P(x,y)

I have been stuck with this problem for a long time, I tried reductio ad absurdum and I got the hypothesys [¬∃x∀y¬P(x,y)], then I try to eliminate the negation of the premise, but I have to prove ∀x∃...
3
votes
2answers
53 views

translating a usual proof into natural deduction.

I have some trouble with proving stuff with natural deduction formalism. Let $R$ be a binary relation. For instance I want to prove $\phi,\psi \vdash \theta$ Where $\phi : \forall x \forall y \forall ...
0
votes
0answers
8 views

First order natural deduction proof [duplicate]

I have been stuck with a natural deduction proof of a first-order logic theorem, which has already been discussed here Tricky proof in Natural Deduction [¬∀x∃y¬Rxy ⊢ ∃x∀yRxy]-help ...
3
votes
2answers
78 views

How to use natural deduction to show $\neg (P \land Q) \vdash \neg P \lor \neg Q$?

How to use natural deduction to show $\lnot (P \land Q) \vdash \lnot P \lor \lnot Q$? I think I need to first assume $\neg(\neg P \lor \neg Q)$ and then find a contradiction but I cannot see how to do ...
1
vote
0answers
24 views

What workbooks (guidelines) can be helpful for solving math logical exercies?

I am wondering which workbooks can be helpful in solving following task: For an individual range I = {a,b} show that: Math logic exercise As I understood, this task is connected to Horn clause, math ...
2
votes
1answer
46 views

Why is “If ψ ∈ Γ then the sequent (Γ ⊢ ψ) is correct” true?

In Chiswell and Hodges Mathematical Logic the authors define a sequent as such "A sequent is an expression (Γ ⊢ ψ) (or Γ ⊢ ψ when there is no ambiguity) where ψ is a statement (the conclusion ...
2
votes
1answer
60 views

Show that the proof rule is not sound and proof question

I'm asked to show that the proof rule \begin{equation} \dfrac{\varphi \to \psi}{\lnot \varphi \to \lnot \psi} \end{equation} is not sound. To show this would I just make the truth tables for the ...
3
votes
1answer
71 views

Proof using natural deduction (Tautology)

I've been asked to prove the following tautology via natural deduction: $\forall x \, (\lnot Px \lor Qx) \rightarrow (\forall y \, Py \rightarrow \forall z \,Qz)$ I normally use tree proofs, but I ...
2
votes
4answers
60 views

Natural deduction proof of $(A \to \lnot B \lor C), ((\lnot D \land A) \to B), (\lnot E \to A) \vdash D \lor (C \lor E)$

I'm struggling to proof this both if I use or introduction rule $\lor_{I_1}$ (to work on $D$) or or introduction rule $\lor_{I_2}$ (to work on $C \lor E$). Could you help me?
2
votes
1answer
56 views

When should I use RAA in natural deduction proofs?

I can't understand exactly when should I use RAA (reductio ad absurdum) rule in natural deduction proofs? What situation should "trigger" me to think "Now it's time to use RAA"?
2
votes
1answer
77 views

Predicate Logic Natural Deduction: $∃x P(x) ⊢P(x)$

I am really puzzled right now. To solve the issue, I need to prove this formular: $$ \exists x P(x) \vdash P(x) $$ with the natural deduction rules for propositional and predicate logic. I am ...
1
vote
2answers
95 views

formal proof of $(p → q) → (¬q → ¬p)$

I'm asked to give a formal proof of $(p → q) → (¬q → ¬p)$ using natural deduction. Is that like saying prove $⊢ (p → q) → (¬q → ¬p$), where it should be proved from nothing?
1
vote
1answer
66 views

Would natural deduction maintain its soundness with introduction of new rule?

I'm asked if adding the following rule to natural deduction would maintain the soundness and completeness of natural deduction. I think with the first one, natural deduction would maintain its ...
1
vote
3answers
89 views

Trouble understanding proof to $\vdash ((\neg(\phi\rightarrow \psi))\rightarrow\phi)$?

I am having trouble understanding the natural deduction proof of $\vdash ((\neg(\phi\rightarrow \psi))\rightarrow\phi)$ (question 2.6.2 (b)) in Hodges and Chiswell's Mathemaical Logic. The natural ...
0
votes
0answers
48 views

Help with the natural deduction proof to the sequent ⊢ (φ → ((¬φ) → ψ))

I am working through Chriswell and Hodge's Mathematical Logic and am confused by the answer to the question 2.6.2 (b). In particular why ...
1
vote
1answer
41 views

Prove propositional formulas using Natural Deduction

(e) Show that $\vdash \lnot(p \lor \lnot p) \to p \land \lnot p$ (f) Show that $\models p \lor \lnot p$ and $\vdash p \lor \lnot p$. For the second part, you can assume (e), i.e. you can treat $\...
2
votes
2answers
40 views

How to prove B from a premise in which B does not occur using natural deduction?

I am preparing for my first logic exam and in the test examples I've come across the following question: Prove by natural deduction: B from premise A ∧ ¬A I am ...
1
vote
1answer
41 views

$Pa\rightarrow \exists y Qy \vdash \exists y (Pa\rightarrow Qy)$ using natural deduction

$Pa\rightarrow \exists y Qy \vdash \exists y (Pa\rightarrow Qy)$ My friend asked me to prove this using natural deduction. He knows I studied logic but I know little about natural deduction since I ...
1
vote
2answers
31 views

Natural Deduction Rules

I am familiar with the main rules of natural deduction: $∧i, ∧e1, ¬¬e, ⇒e, ⇒i, ∨i, ∨e$ (slightly). However, when presented with the following premise: $$\sim a ∧ (a ∨ b)$$ I used $∧ e$ to obtain:...
2
votes
1answer
30 views

Can composition of morphisms in a category be carried out on any subgraph of a commutative diagram, in-place?

Here is what the rule looks like to us and how we specify it to the app I'm writing. I was wondering can you take any commutative diagram $J$ and apply this rule to a subgraph matching $A \...
2
votes
2answers
52 views

Natural deduction: predicate logic proof (Prenex form)

I'm pretty familiar with proofs in propositional logic, but not so much with predicate logic. I'm trying to prove the following (which can be used during construction of prenex normal form). If $x$ ...
-3
votes
1answer
49 views

Natural deduction proof - is this correct?

I don't know of any means to check my work, can anyone point out if they're any mistakes?
1
vote
1answer
52 views

Proving ∀x(A(x) ∨ B) → ∀xA(x) ∨ B, with x is not in B, by natural deduction

how can prove ∀x(A(x) ∨ B) → ∀xA(x) ∨ B where x is not in B using natural deduction. i am not sure how should use for all introduction rule here. any help wpuld be highly appreciate. Cheers
1
vote
1answer
31 views

How to prove ~($\forall$x Q(x)) is logically equivalent to $\exists$x(~Q(x)) using natural deduction for first order logic

I am thinking of assuming Q(x1) and then deriving to reach to a contradiction but I have not been able to do so.
2
votes
1answer
100 views

Relationship between sequent calculus and Hilbert systems, natural deduction, etc

I am trying to learn the basics of logic and I'm confused on how these proof systems work together. The big ones I see are Hilbert style, and then Gentzen style which includes natural deduction, and ...
2
votes
1answer
52 views

Natural deduction without premises given?

Normally when given a question like $Q \wedge P, R \vdash P \wedge R$ I can do box proof like: $\dfrac{\dfrac{Q \wedge P^{~\text{(assumption)}}}{P}{^\text{($\wedge$-elimination)}}\quad R^{~\text{(...
0
votes
2answers
43 views

Proof for $\lor$ Elim: rule in Soundness Theorem

So far I have been told to assume the line is invalid and then arrive at a contradiction. Suppose the first invalid step derives the sentence $C$ by an application of $\lor$ Elim to the sentences $A\...
3
votes
1answer
60 views

Find a natural deduction proof to show ∃x∃y (S(x,y) ∨ S(y,x)) ⊢ ∃x∃y S(x,y) by predicate logic.

I'm trying to prove $\exists x \exists y (S(x,y) \lor S(y,x)) \vdash \exists x \exists y S(x,y)$ in natural deduction, and I have already applied existential elimination to get $S(x_0,y_0)$, with $x_0$...
2
votes
2answers
196 views

Prove (¬(∀𝑥(¬𝑃(𝑥)))) ⊢ (∃𝑥 𝑃(𝑥)) by Natural Deduction

I want to prove (¬(∀𝑥(¬𝑃(𝑥)))) ⊢ (∃𝑥𝑃(𝑥)) using only the basic rules of the Natural Deduction system for propositional logic and predicate logic. I am not sure how to get rid of the negation ...
2
votes
1answer
35 views

Showing a Set is Inconsistent In Logic

Let $\Phi = \left \{ \alpha, \beta, \gamma \right \}$ be a set of three well-formed formulas. To show $\Phi$ is inconsistent, should I use deduction to show that $\Phi \vdash \phi$ for all $\phi \in \...