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
3
votes
1answer
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 ...
0
votes
1answer
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?
0
votes
1answer
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?
-1
votes
1answer
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(...
3
votes
1answer
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 ...
1
vote
2answers
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 ...
2
votes
1answer
58 views

Prove if $B$ has a smallest element, then this element is unique.

Working on the book: Daniel J. Velleman. "HOW TO PROVE IT: A Structured Approach, Second Edition" (p. 206) Theorem 4.4.6. Suppose $R$ is a partial order on a set $A$, and $B \subseteq A$. If $...
-3
votes
1answer
38 views

How to prove by natural deduction? [closed]

Hi I am new to Mathematical Logic and recently I self-tutored on natural deduction. I have learned natural deduction rules like: Rule for $\wedge$-formula. Rule for $\rightarrow$-formula. Rule for ...
1
vote
2answers
85 views

Help to find a proof in natural deduction

I have a question about the methodology of natural deduction, more specifically finding a proof in natural deduction. The assignment says: Find a proof for the formula $(P \rightarrow \neg P) \...
1
vote
1answer
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 ...
0
votes
1answer
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....
2
votes
0answers
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. ...
1
vote
1answer
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. ...
-2
votes
0answers
55 views

Prove that if the square of a positive integer is divisible by 3, then so is the integer.

$\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}} \def\Ae#1{\qquad\mathbf{\forall E} \: #1 \\} \def\Ai#1{\qquad\mathbf{\forall I} \: #1 \\} \def\Ee#1{\qquad\mathbf{\exists E} \: #1 \\} \...
1
vote
1answer
46 views

Given ∀x.(p(x) ⇒ q(x)), use the Fitch System to prove ∀x.p(x) ⇒ ∀x.q(x)

I'm having trouble solving this exercise: Given ∀x.(p(x) ⇒ q(x)), use the Fitch System to prove ∀x.p(x) ⇒ ∀x.q(x) My idea was to use Universal Introduction on steps 4 and 5, and once I get AX:p(X) ...
1
vote
2answers
66 views

Construct a proof for the argument: P ∨ Q, ¬Q ∴ P

Could you please help me to complete my proof using (only) : ∧I, ⊃I, ∨I, ≡I, ∧E, ⊃E, ∨E, ≡E, ¬I and ¬E. P ∨ Q, ¬Q ∴ P I tried this proof, on http://proofs.openlogicproject.org/ : but it seems that ...
3
votes
0answers
64 views

Show every positive integer can be written in one of the forms $3k$, $3k+1$, $3k+2$ for some integer $k$.

$ \def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}} \def\Ae#1{\qquad\mathbf{\forall E} \: #1 \\} \def\Ai#1{\qquad\mathbf{\forall I} \: #1 \\} \def\Ee#1{\qquad\mathbf{\exists E} \: #1 \\} \...
2
votes
1answer
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 ...
0
votes
1answer
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)\...
1
vote
1answer
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 ...
1
vote
0answers
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 ...
-2
votes
1answer
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....
1
vote
1answer
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 ...
0
votes
2answers
74 views

Prove there is a unique set $A$ such that for every set $B$, $A \cup B=B$ using Natural Deduction.

I added $\forall Y(\emptyset \cup Y = Y)$ as a premise; the exercise does not provide it. $ \def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}} \def\Ae#1{\qquad\mathbf{\forall E} \: #1 \\} \...
0
votes
2answers
50 views

Natural Deduction, Finish the Proof

$$(((p\land q)\lor r)\land ((p\land q)\lor s)) \to ((p\land q)\lor (r\land s))$$ I don't know how to finish this proof by natural deduction using tree. First I used $(\to I)$ I got $((p\land q)\lor(r\...
2
votes
1answer
34 views

Prove $\exists x(P(x) \land \forall y(P(y) \to y=x)) \vdash \exists x \forall y(P(y) \leftrightarrow y=x)$.

This is the skeleton for this proof using Fitch-style natural deduction system. $ \def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}} \def\Ae#1{\qquad\mathbf{\forall E} \: #1 \\} \def\Ai#1{\...
2
votes
1answer
75 views

Proof: the element $0 \in \mathbb{Z}$ is unique.

If I symbolize the argument in First-Order logic, I think this would be the argument (the conclusion is an expansion of $\exists!$ definition): $\exists z \forall x(x+z=x) \vdash \exists y(\forall x(...
-1
votes
1answer
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 ...
2
votes
5answers
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 ...
0
votes
0answers
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 ...
0
votes
1answer
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 ...
-3
votes
1answer
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(...
0
votes
0answers
51 views

Prove that given any two consecutive integers, one is even and the other is odd.

Symbolization key: $E(x)$: x is even. $O(x)$: x is odd $ \def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}} \def\Ae#1{\qquad\mathbf{\forall E} \: #1 \\} \def\Ai#1{\qquad\mathbf{\forall I} ...
2
votes
1answer
95 views

Proving $\forall x(x \text{ is odd} \to x^2 \text{ is odd)}$ using First Order Logic.

Symbolization key: We define: $O(x)$: $x$ is odd. Proof: $ \def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}} \def\Ae#1{\qquad\mathbf{\forall E} \: #1 \\} \def\Ai#1{\qquad\mathbf{\forall ...
2
votes
0answers
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', ...
1
vote
1answer
52 views

Prove $\forall xA(x) \to B \therefore \exists x(A(x) \to B)$.

Working on P.D. Magnus. "forallX: an Introduction to Formal Logic" (p. 297, exercise C. 1): $ \def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}} \def\Ae#1{\qquad\mathbf{\forall E} \: #1 \\}...
3
votes
1answer
28 views

Showing $(L \leftrightarrow ((N \to N) \to L)) \lor H$ is not contingent.

Working P.D. Magnus. forallX: an Introduction to Formal Logic (p. 182, exercise B. 4). To solve it, I tried that sentence is a theorem: $ \def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}} ...
2
votes
1answer
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, ...
1
vote
3answers
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.
2
votes
1answer
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 ...
1
vote
1answer
95 views

Prove $\exists x (\exists yA(y) \to A(x))$ is a theorem.

Working on P.D. Magnus. forallX: an Introduction to Formal Logic (pp. 297, exercise C. 5): $ \def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}} \def\Ae#1{\qquad\mathbf{\forall E} \: #1 \\} ...
1
vote
2answers
83 views

Prove $\exists x (A(x) \to \forall y(A(y))$ is a theorem.

Working on P.D. Magnus. forallX: an Introduction to Formal Logic (pp. 297, exercise C. 4): $ \def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}} \fitch{}{ \fitch{\neg \exists x (A(x) \to \...
4
votes
2answers
69 views

Prove $\forall x(A \vee B(x)) \therefore A \vee \forall xB(x)$.

Working on P.D. Magnus. forallX: an Introduction to Formal Logic (pp. 297, exercise C. 3): $ \def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}} \fitch{\forall x(A \vee B(x))}{ \fitch{\...
2
votes
1answer
41 views

Show $\neg (W \to W), (W \leftrightarrow W) \wedge W, E \vee (W \to \neg (E \wedge W))$ are jointly inconsistent.

Working on P.D. Magnus. forallX: an Introduction to Formal Logic (pp. 182, exercise B. 9): $ \def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}} \fitch{\neg (W \to W)\\(W \leftrightarrow W) ...
0
votes
1answer
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 ...
-1
votes
1answer
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 ...
1
vote
3answers
113 views

Proving $A \to \exists x B(x) \therefore \exists x(A \to B(x))$

Working on P.D. Magnus. forallX: an Introduction to Formal Logic (pp. 297, exercise C. 2), appears the following exercise: $ \def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}} \fitch{A \to ...
0
votes
1answer
34 views

Proving $\forall x \forall y(R(x,y) \to R(y,x)) \therefore \forall x \forall y\forall z[(R(x,y) \wedge R(x,z)) \to \exists u(R(y,u) \wedge R(z,u))]$

Working on Working on P.D. Magnus. forallX: an Introduction to Formal Logic (pp. 297, exercise B. 4), appears this exercise: $ \def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}} \fitch{\...
0
votes
3answers
44 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.
0
votes
0answers
38 views

Exercise 2.4.5 in Chiswell and Hodges

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

1
2 3 4 5
14