Stack Exchange Network

Stack Exchange network consists of 174 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.

2
votes
2answers
50 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
19 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
38 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
0answers
45 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
49 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
48 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
43 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
67 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
73 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
53 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
77 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
40 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
35 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
1answer
26 views

How to proof 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
31 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 ...
0
votes
2answers
24 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:...
1
vote
1answer
28 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 \...
1
vote
2answers
41 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 is ...
-3
votes
1answer
45 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
50 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
27 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
69 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 ...
1
vote
1answer
37 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
39 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\...
2
votes
1answer
55 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$...
1
vote
2answers
151 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
0answers
30 views

Sustainable population - When to breed

I would like advice on an approach to solving this real world problem. I'm not certain if the solution is to solve a system of equations, or something else. The problem is stated below with the ...
1
vote
1answer
33 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 \...
-1
votes
1answer
28 views

Proof 3 sequents with natural deduction

I have to proof 3 sequents and allowed are the basic rules like elimination, implication, pbc and so on. I am kinda struggling with the solutions but maybe you can give me some hints. :) 1) -p -> p ...
2
votes
0answers
44 views

Optimality results for Fitch-style natural deduction proofs

Suppose a student submits a Fitch-style natural deduction proof in propositional or predicate logic. Two natural questions arise (beyond correctness): Is the proof as short as can be? Is the proof as ...
0
votes
2answers
41 views

Do I have to discharge an antecedent that I assume?

For example, if I have the premise: $P \rightarrow (Q \rightarrow R)$ Can I assume P to get: $Q\rightarrow R$ And then assume Q to get R. For reductio ad absurdum and arrow introduction I know ...
1
vote
2answers
119 views

Logical proof using sentential logic $\Big(\big(A \& B \big) \lor \big((\neg{}A \& B) \lor (A \& \neg{}B)\big)\Big)$

I have a premise $(A \lor B)$ and need to achieve the conclusion $\Big(\big(A \& B \big) \lor \big((\neg{}A \& B) \lor (A \& \neg{}B)\big)\Big)$ This intuitively makes sense since $(A \...
1
vote
1answer
76 views

How to prove double negation elimination without using $\bot$?

$\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}}$ I am trying to derive some rules without the use of the $\bot$ symbol. First I want to describe how I am defining certain inference ...
0
votes
0answers
36 views

Fitch proof of Peirce's Law [duplicate]

This was a question on my exam today that I couldn't figure out. Show $((P \supset Q) \supset P) \supset P$ with no premises using Fitch. The first attempt is I assumed $(P \supset Q) \supset P$. ...
5
votes
1answer
90 views

Is it possible to prove that we found the shortest proof?

Initial considerations: using natural deduction as a logical system, we're limited to propositional logic, and we have a fixed set of basic rules of inference. Suppose that we cannot use any theorems ...
0
votes
2answers
70 views

Showing validity of an argument when premises contradict each other (natural deduction)

I know that an argument is invalid when its premises are true while it's conclusions are false. But what if the premises are inconsistent? !(a=>b) , b | !a |- c ...
2
votes
3answers
78 views

Natural deduction proof for $(a\to(b\to c))\to((a\to b)\to(a\to c))$

I am trying to prove that $(a\to(b\to c))\to((a\to b)\to(a\to c))$ holds in natural deduction, in particular when I work backwards from a Fitch style proof I can only get so far: How can I prove ...
1
vote
0answers
55 views

Fitch system, or alternatives?

Is there a good resource for how to understand the rules of a Fitch proof system, or an alternative? I'm currently trying to get a sense or how things are proved in natural deduction, which differs in ...
1
vote
2answers
81 views

Does natural deduction require a non-empty set of premises?

Normally in a Hilbert system, writing a proof $\Delta \vdash \varphi_n$ with lines $\varphi_1, \varphi_2, ..., \varphi_n$ is done such that each $\varphi_k$ is either a proposition contained in $\...
1
vote
1answer
60 views

Hilbert systems and natural deduction systems in terms of “context”

I was reading the Wiki article on Hilbert systems and came across this passage: A characteristic feature of the many variants of Hilbert systems is that the context is not changed in any of their ...
3
votes
1answer
116 views

What is the utility, exactly, of the Deduction Theorem?

The Deduction Theorem states that for a set of assumptions $\Delta$ and two wffs $A$ and $B$, we have the metalogical relationship: $$\Delta \cup \{A\} \vdash B \implies \Delta \vdash A \to B$$ In ...
0
votes
1answer
53 views

(P → Q) v (Q → R), Fitch-style proof

I'm trying to construct a Fitch-style proof for $(P \to Q) \lor (Q \to R)$ using reductio ad absurdum and the introduction and elimination rules for conjunction, disjunction, and implication. I'm not ...
1
vote
1answer
51 views

Natural Deduction Problem formula

We define the size $Size(q)$ of a proposition $q$ as the number of variable occurrences in it, i.e. \begin{align} Size(x) &= 1 \\ Size(¬q) &= Size(q) \\ Size(q_1 \text{ op } q_2) &...
1
vote
1answer
137 views

Logical disjunction elimination rule

I know these two rules about disjunctive introduction (Vi (1), Vi (2)). In other words: Given ...
1
vote
1answer
275 views

Proving the distributive law with natural deduction

I have to prove the following logical equivalence, also known as one of the two distributive laws: $$ P \vee (Q \wedge R) \equiv (P \vee Q) \wedge (P \vee R) $$ I have solved the first part, $P \lor ...
5
votes
3answers
274 views

Predicate Logic, Proof of validity . How to remove negation infront of existential quantifier?

$\forall x~(P(x) \to (Q(x) \lor R(x))), \lnot \exists x~(P(x) \land R(x)) \vdash \forall x~(P(x) \to Q(x))$ I am stuck on how to get rid of the negation on "$\lnot \exists x~(P(x) \land R(x))$" in ...
3
votes
1answer
52 views

Predicate logic, proof of validity of sequent.

The goal is to prove that $\forall x (P(x) \land Q(x)) \vdash \forall x (P(x) \to Q(x))$ in natural deduction. Would like to find out if I did this natural deduction correctly and if not where did I ...
0
votes
0answers
42 views

Formal definitions in natural deduction

I am searching a formal definition of natural deduction rules and a formal definition of derivation in natural deduction. For example how to formalize hypothetical derivations? Hypothetical ...
0
votes
2answers
32 views

First-order logic mindset when checking if A fulfills B

Task I'm supposed to check if the following is correct: $\forall x(P(x) \lor Q(x)) \vDash \forall xP(x) \lor \forall xQ(x)$ Questions If I remember the definition correctly of $\vDash$ it means ...
4
votes
5answers
1k views

Why not ban nested quantifiers over the same variable?

People seem to think (1, 2, 3) that a wff can have nested quantifiers over the same variable, e.g., $\forall x(Px \wedge \exists x Qx)$. However, consider the following argument: $\forall x \exists ...