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

0
votes
1answer
20 views

Two aspects of randomness

Consider a random sequence of integers 1, 4, 3, 8, 2, 5, 3, 8 ... The only sufficient condition for the sequence to be random is its unpredictability ie. probability of any number coming next ...
0
votes
1answer
19 views

I'm trying to prove P→(Q∧R) from the following premises: (P→Q)∧R, (P∧R)→S, ¬S [on hold]

I made a truth table and found that the conclusion is valid. But, I need help constructing a formal proof.
1
vote
1answer
29 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
35 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
49 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
votes
1answer
61 views

Help with natural deduction system (Propositional logic) [closed]

In natural deduction, I'm trying to get to $(A \to B) \land (\lnot A \to C)$ from the following formula: $(A \land B) \lor (\lnot A \land C)$ and vice-versa, i.e. $(A \land B) \lor (¬ A \land C) \...
1
vote
2answers
128 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 ...
-3
votes
0answers
19 views

For all x (P(x) v Q(x)) and for all x((~P(x) and Q(x)) > R(x)) implies For all x (~R(x) implies P(x))

$$\forall x ~(P(x) \lor Q(x)) \land \forall x~((\lnot P(x) \land Q(x)) \to R(x)) ~\to~ \forall x (\lnot R(x) \to P(x))$$ How can I prove that statement by using natural deduction ? I am newbie and ...
2
votes
0answers
29 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
32 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
26 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
40 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
37 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
57 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
66 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
33 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
79 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
61 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
74 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
50 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
76 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
54 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
112 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
47 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
79 views

Logical disjunction elimination rule

I know these two rules about disjunctive introduction (Vi (1), Vi (2)). In other words: Given ...
1
vote
1answer
214 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
229 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
45 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
39 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
31 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 ...
2
votes
1answer
50 views

Equivalence in Natural deduction in First-order logic 2

I would want to check with you guys if I've done the following natural deduction correct. The reason being that I haven't gotten any answer sheet for this task. Task Solve the following with natural ...
0
votes
2answers
33 views

logical deduction question [duplicate]

For example: S ::= “Sales will go up.” E ::= “Expenses will go up.” Express the following: Both sales and expenses will fall. Why is it ¬ (S ∧ E) instead of ¬S ∧ ¬E ?
2
votes
3answers
63 views

Equivalence in natural deduction in First-order logic

Task $\vdash \exists x (P(x)\lor Q(x)) \iff \exists xP(x) \lor \exists xQ(x) $ My answer If we have $A \iff B$ then $A\vdash B$ and $B \vdash A$. So I started trying to see if I could prove $B$ ...
2
votes
1answer
54 views

Natural deduction in first-order logic

I've sat for more than an hour now and I don't understand how I'm supposed to solve the task below. $\{\forall x(P(x) \land Q(x)), \exists x\neg P(x)\} \vdash \exists x \neg Q(x) $ So I'm a bit ...
2
votes
1answer
81 views

Exercise 2 (p. 30) on W. Rautenberg - A concise introduction to Logic.

I'm can't solve Exercise 2 on page 30 on Rautenberg (Chapter 1.4 - A calculus of Natural Deduction), which reads: Augment the signature $\{\lnot, \land\}$ by $\lor$ and prove the completeness of the ...
0
votes
2answers
106 views

How to prove $\lnot(p\to q)\vdash p \land\lnot q$

This is the first time I post anything on the forum. I started with Tomassi's Logic and unfortunately I have been unable to solve some of its problems. One I get immediately stuck with is this one: $$...
1
vote
0answers
52 views

Fitch-style Deductive Proof

I am having trouble with the following question: Give natural deduction proofs of the following formulas (from no assumptions): $p \to p$. Here is what I have so far: $$\begin{array}{|l}\hline~~\...
2
votes
2answers
73 views

A real-world interpretation for $\{\neg(\phi\leftrightarrow\psi)\}\vdash((\neg\phi)\leftrightarrow\psi)$

One of the exercises in Chiswell's Mathematical Logic is to prove the following sequent $\{\neg(\phi\leftrightarrow\psi)\}\vdash((\neg\phi)\leftrightarrow\psi).$ I'm not interested in deriving ...
2
votes
1answer
72 views

Tautology question

I want to prove (φ→ρ) → ((ψ→ρ) → ((φ∨ψ)→ρ)) I made a proof but don`t know doing right may you check it whether doing right or wrong?
3
votes
2answers
57 views

Natural Deduction Proof that irreflexive, transitive relations on a Set S are not three-cycles

I am looking for a natural deduction proof for above question. I have formalized the argument in the following way: $$ \forall x \neg Rxx, \ \forall x\forall y \forall z (Rxy\land Ryz \rightarrow Rxz)...
2
votes
1answer
60 views

Natural deduction proof - problem with existential elimination

I have problems with the following proof: $$ \forall x \exists y (Rxy \land Py), \forall x \neg Rxx \vdash \neg \forall x \forall y (Px \implies (Py \implies x=y)) $$ The problem is with the ...
0
votes
1answer
72 views

How to show local soundness and completeness for NAND

I have been following Frank Pfenning's Notes on natural deduction, and I have a few questions on how to write rules with the local soundness and local completeness properties. Consider these rules ...
0
votes
2answers
60 views

Deducing formula from a given set of formulas

Having a set of formulas: $$ S = \big\{ p ⇒ (r \wedge p), \neg p \wedge s, s \vee (p ⇒ q)\big\} $$ I have to find a formula that can be deduced from this set of formulas. The answer we are looking for ...
2
votes
1answer
30 views

Natural proof steps for predicate

I am trying to prove the following predicate by using natural deduction rules but I do not see the way to do it: ∀ x(P(x) ∨ Q(x)) ⊢ ~∀x(~P(x) ∧ ~Q(x)) Is this predicate derivable? if yes please ...
2
votes
2answers
104 views

Proving propositional logic associativity with natural deduction

I'm pretty sure similar question was asked, so sorry that I'm posting this again, but just reading the answers on that question didn't seem to provide enough insight for me and I'd just like to double-...
-2
votes
1answer
111 views

Prove that double negation elimination is a derivated rule [closed]

If $B=\{\wedge i, \wedge e_1, \wedge e_2, \vee i_1, \vee i_2, \vee e, \to i, \to e, \neg i, \neg e\}$, how can I prove that $\neg\neg e$ is a derivated rule from $B$ and proof-by-contradiction?
2
votes
4answers
110 views

What's the intuition behind using Law of Excluded Middle in Natural Deduction?

I've recently started learning First-Order Logic and I have been doing some Natural Deduction exercises. I understand the principles behind most of the Inference Rules but when it comes to applying ...
0
votes
3answers
36 views

Construction of a derivation when proving equivalence of a logical formula.

Given $$A \wedge B \to C \equiv A \to B \to C$$ We want to show that $$\{ A \to B \to C\} \vdash A \wedge B \to C$$ by constructing a derivation using the natural deduction system $\mathcal{N}_{PL}$. ...