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

677 questions
Filter by
Sorted by
Tagged with
62 views

### First order logic natural deduction problem

I am struggling with a particular case in the (inductive) proof of Theorem 2.8.3 (i) of Logic and Structure by Dirk Van Dalen ($c \neq x$ in the Theorem statement is a variable) The cases when we ...
22 views

### Can different variables refer to the same object without an identity rule stated explicitly?

For example, $\forall x(Qx\rightarrow \exists y(Py\wedge Rxy))$, if the Universe of discourse only contained one object, can this sentence be true?
35 views

### quantifier negation proof with natural deduction? [duplicate]

How can I derive ∃𝑥¬𝑃(𝑥)⊢¬∀𝑥𝑃(𝑥)? I know that I need to derive some sort of contradiction, but what do I assume?
49 views

### Stuck in logic exercise

"Consider a language with a single object constant a, a single unary function constant s, and two unary relation constants p and q. We start with the premises shown below. We know that p is true of s(...
58 views

### Predicate Logic: Exists-proof

I've entered my proof on this website and I don't understand why following proof isn't okay. As you can see, the proof checker tells me that I've used the rule for $\exists$ in a wrong way. Is this ...
78 views

### Natural deduction has me stuck

I have been trying to break down these two formula correctly using natural deduction, and now I am stuck and confused. Below there is my attempt to derive the propositional logic consequences. I need ...
58 views

53 views

### given $o(k), \neg o(n), \neg y(j), \forall x(y(x)\Rightarrow \neg o(x)), \exists x(y(x))$ prove $y(n)$ using Stanford university fitch system

Context: This is related to another question I've recently asked BUT it is a different formulation of the same problem. The orihinal problem is given here. Solving the puzzle is very easy, my goal is ...
125 views

### Herbrand Logic exercise on multidimensional induction

I am completing a self study guide from Stanfords "Teach yourself Logic" course, and I am stuck on a problem regarding multidimensional induction. "Starting with the axioms for e given in Section 12....
81 views

### Is the author implicitly doing a proof by contradiction?

In Lang, Serge. "Basic Mathematics" (p.42), appears this proof: From the existence of an inverse for non-zero rational numbers, we deduce: $$\text{If } ab=0, \text{then a=0 or b=0}$$ Proof. ...
58 views

### Given $\forall X\, p(X)$, use the Fitch System to prove $\lnot \exists X\, \lnot p(X)$

I've tried to solve this exercise based on a similar question that was asked some years ago, but I'm stuck in step 5. Any help? Thanks in advance. By the way I'm using Stanford's system. ...
55 views

103 views

### Given $∃y.∀x.p(x,y)$, use the Fitch system to prove $∀x.∃y.p(x,y)$

Given $\exists y. \forall x. p(x,y)$, use Fitch-style natural deduction system to prove $\forall x.\exists y.p(x,y)$. I know this question has been asked before, but based on that answer I'm not able ...
56 views

### Given $\exists x.\lnot p(x)$, use the Fitch System to prove $\lnot \forall x.p(x)$ [duplicate]

This is what I've come up with so far, but I'm stuck at step 11: \begin{align} &(1)\quad \exists x.\lnot p(x) & \text{Premise}\\ &(2)\quad \lnot p(x) & \text{Assumption}\\ & (3)\...
48 views

### Show that there is a rational number $b$ such that $ab = ba = 1$ using First Order Logic.

Working on Lang, Serge. "Basic Mathematics" (p. 39, ex. 4). Let $a = m/n$ be a rational number expressed as a quotient of integers $m, n$ with $m \neq 0$ and $n \neq 0$. Show that there is a ...
22 views

### Prove $T=T'$ using Natural Deduction.

Working on Lang, Serge. "Basic Mathematics" (p. 100, example). Let $S$ be the set of numbers x such that $1 \leq x \leq 2$. Let $T$ be the set of all numbers $5x$ with all x in $S$. We contend ...
42 views

### Help, have to prove the tautology (p ∨ ¬p) from nothing using fitch system. [closed]

I'm new using fitch so this is all i have and don't know how to get it done. (https://i.paste.pics/d0746642a4513e1ca1799b3e92e2ace2.png) Here's the link of the exercise: http://intrologic.stanford....
59 views

### Urgent Help Given p ⇒ q, use the Fitch System to prove ¬q ⇒ ¬p. [closed]

I think I'm close but I don't know what to do next. Help, please. All I've done is this: 1.p=>q Premise 2.~q assumption 3.p assumption 4.q implication elimination 1,3 5.q&~q and ...
74 views

34 views

38 views

### Use induction and elimination rules of propositional logic to prove [duplicate]

I was asked to prove p -> q |- ¬p or q by nature induction $p \rightarrow q$ premise p assume q $\rightarrow e,1$ $¬ p \rightarrow ¬ q$ ¬p ...
125 views

### Determine if Modus Ponens argument is valid

I am trying to determine whether the following argument is valid: P ⇒ ((∼Q) ∧ R) Q ⇒ (P ∨ R) therefore P ⇒ R I have constructed truth tables for each statement. However, I am confused on how to ...
39 views

### What are those implicit “rules” by which we deduce theorems from axioms in mathematics?

In purely formal mathematics - meaning using inference rules to derive new theorems from axioms (like in Hilbert calculus) - there is explicitly told how to deduce new theorems. However in most of ...
80 views

### Proving $\forall x\forall y(P(x) \to Q(y)) \vdash \exists x(P(x) \to \forall y \, Q(y))$ using natural deduction.

I am getting an error presumably in the last line (application of $\mathbf{E I}$ rule, i.e. introduction of the existential quantifier) using proof checker BoxProver. The proof seems correct, but ...
52 views

### How do i use natural deduction to prove ∀x ∀y ∀z (P(x, y) ∧ P(y, z) → P(x, z)), ∀x ¬P(x, x) ⊢ ∀x ∀y (P(x, y) → ¬P(x, y)) in fitch-style? [closed]

I've been doing a lot of exercises in predicate logic, but i'm unable to solve it for as I can hardly wrap my head around how to begin: ∀x ∀y ∀z (P(x, y) ∧ P(y, z) → P(x, z)), ∀x ¬P(x, x) ⊢ Ex Ey (P(...
51 views

47 views

### Constructing Natural Deduction Sequences?

My question is at the very end of this preamble, which I think will aid in the understanding of the question and I therefore included. Start with a 'set' $P$, of atomic proposition 'characters', ...
52 views

41 views

### Justify indirect proof rule with law of excluded middle

In P.D. Magnus. forallX: an Introduction to Formal Logic (p. 174, exercise D), appears this exercise: D. Show that if you had LEM as a basic rule, you could justify IP as a derived rule. That is, ...
65 views

### Language, Proof and Logic $14.12$ Solution $\left(\text{I need help}\tiny\overset{\cdot~\cdot}{\frown}\right)$

I can only use Taut Con in this assignment but I dont know how to change line $15$ to line $16$ using it. Would appreciate any help! I thought I could used $\lor~$Elim but I can't seem to do it.
32 views

### Question about Fitch style natural deduction

So I have a proof in which i have derived both ~P and (P v Q). My current objective is to extract the Q as I need it for another part of the proof. It seems obvious to me that if I have ~P true and (P ...
95 views

69 views

44 views

### How to formalize these proofs and conclusion?

I have these sentences and I have obtained these atoms and solution: 1.- When there is public spending, if the citizens are not satisfied, the banks do not give credits 2.- For there to be public ...
44 views

### Is this proof solvable? Doubt about natural deduction

I am learning logic and I found a difficult exercise. I have been exercising for three days and I start to get overwhelmed. I would like some help, to learn from my mistake... I think not to plan ...
113 views

### Deriving a implies b from (not a) or b (formally: $\neg a \vee b\vdash a\rightarrow b$)
I've struggled a long time proving $\neg a \vee b\vdash a\rightarrow b$ via natural deduction, so I thought I can just show (and explain) how it's done after I finally figured it out.
I am working through Chiswell and Hodges and came across this exercise (2.4.5): Show that {$\phi$} $\vdash$ $\psi$ iff $\vdash$ $( \phi \rightarrow \psi )$. For the first part, my line of ...