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
6
votes
2answers
98 views

$\vdash (\lnot \chi \to \lnot \theta) \to (\theta \to \chi) $

For $\theta, \chi$ $\mathcal{L}$-formulas in predicate logic, I'm trying to prove: $\vdash (\lnot \chi \to \lnot \theta) \to (\theta \to \chi) $. I've managed to prove $\vdash \lnot\lnot \theta \to \...
0
votes
2answers
53 views

Show that $A\vee B$ is logically equivalent to the sentence $(A\vee (B\wedge A))\vee(B\wedge\neg A)$?

Show that $A\vee B$ is logically equivalent to the sentence $(A\vee (B\wedge A))\vee(B\wedge\neg A)$ I need help with this problem. Can somebody explain this please? ...instructions state that I have ...
-2
votes
2answers
48 views

TFL question: ⊤ ⊢ (A → B) ∨ (B → A) [closed]

I am so unsure how to answer this question: ⊤ ⊢ (A → B) ∨ (B → A) Here is what I tried Can someone please help me? Thank you!
-1
votes
1answer
44 views

Natural deduction problem that has no premise [closed]

I have the following problem: ⊢A→((A→B)→B) I can't seem to be able to start! I am very confused and any tips in the right direction will help! Thanks a lot
0
votes
2answers
37 views

Give syntax proof of FOL Formla $\exists x.P(x) \lor \exists x.Q(x)$ $\vdash$ $\exists x.(P(x) \lor Q(x))$ [closed]

So the question is pretty much described in the title already. I have to show the following result. I have tried it but am failing to do so. Anyone who can please help me in understanding its proof. I ...
-1
votes
2answers
49 views

Give syntax proof of $\forall x (P(x) \lor Q(x))$ , $\forall y. \neg P(y)$ $\vdash$ $\forall x.Q(x)$

So the question is in the title already. I have to prove the following using first-order logic but I am failing to do so. Please someone help me understand how do I do it? $\forall x (P(x) \lor Q(x))$ ...
1
vote
3answers
57 views

Prove $(p \rightarrow q)$ $\vdash$ $( \lnot q \rightarrow \lnot p)$ using syntactic axioms and derivation rules.

I have to prove the following. I can prove the reverse but don't know how to go logically from premise to conclusion using syntactic axioms and derivation rules. Attached is the picture of rules I ...
1
vote
0answers
50 views

$v(\phi \vee \psi)=1 \iff \phi \vee \psi \in \Gamma^*$

I'm taking a lecture in Mathematical Logic for the first time, and the following is a step in the proof of the completeness theorem that I can't work out. Let $\Gamma^*$ be maximally consistent. For ...
1
vote
1answer
48 views

Formal proof for first-order logic question using natural deduction

I'm new to first-order logic and need a little bit of help with proving the following: ∀x∃yA(x,y) ⊢ ¬∃x∀y¬A(x,y) It seemed straightforward but I have been stuck at it for hours. This is what I have ...
0
votes
2answers
51 views

Natural Deduction proof using basic rules only

I need some assistance solving what seems to be a very intuitive problem, but becomes tough when only using strict natural deduction and not assuming De Morgan laws. Laws allowed: Implication, And, Or,...
2
votes
1answer
79 views

Is disjunction elimination a more general form of modus ponens?

It seems to me that disjunction introduction and disjunction elimination implies modus ponens. To be clear, I'm defining disjunction introduction as: $$p\vdash (p\lor q)$$ disjunction elimination as: $...
2
votes
1answer
75 views

Metalogical motivations for logical inference rules?

For example, does every (introduction/elimination) of natural deduction encode some kind of desideratum about the proof system of natural deduction? This was suggested in this question, asking for ...
0
votes
1answer
72 views

Course-of-values induction, according to Kleene IM (1952)

I'm having troubles with exercise *162a in "Introduction to Metamathematics", by S.C. Kleene, 1952. The ask is to prove: (1) $ \vdash A(0) \& \forall x [\forall y (y \leq x \Rightarrow A(...
1
vote
1answer
31 views

Can an assumption be discharged without it being part of the tree?

Given the following formula, use natural deduction to prove that it holds. The answer given by the professor was the following below: I would like to understand how we can discharge the assumption ...
0
votes
2answers
54 views

How to state precisely this requirement relative to the application of natural deduction rules?

Contrary to replacement rules, in natural deduction, rules of infrence need to be applied " to an entire line" . For example, I cannot use Modus Ponens in the following way Premise (1) : ...
0
votes
1answer
99 views

Prove $(∀x(P(x) ∨ Q(x))) → ((∃x(¬P(x))) → (∃x(Q(x))))$ using natural deduction

Hi guys I'm trying to learn natural deduction in predicate logic and I'm struggling with this proof. $(∀x(P(x) ∨ Q(x))) → ((∃x(¬P(x))) → (∃x(Q(x))))$ I'm trying to follow my textbook but don't have ...
2
votes
0answers
28 views

Why is an assumption not discharged for the first implication introduction in natural deduction? [duplicate]

Why is it that an assumption need not be discharged for the first implication introduction in natural deduction? For example, $$\dfrac{\dfrac{[p]^1}{q\to p}{{\to}\mathrm I}}{p\to(q\to p)}{{\to}\mathrm ...
0
votes
2answers
70 views

Natural Deduction Proof: {A v B, ¬A v C} ⊢ B v C

Prove using natural deduction: $(A \lor B), (\lnot A \lor C) ⊢ (B \lor C)$. My work so far: ...
3
votes
1answer
46 views

Deduction rules involving set $\Gamma$ of premises versus elementary textbook natural deduction rules. How do they differ exactly?

In elementary textbooks, natural deduction rules are presented in the following way, say, for $\&$-Intro from $\phi$ and $\psi$, infer $\phi\&\psi$ or $(n).....\phi$ $(m)....\psi$ $\therefore$ ...
0
votes
1answer
48 views

How to prove $p\land q\to \neg r \vdash r \to p \to \neg q$ using natural deduction? [closed]

I'm having a lot of trouble proving the sequent below with Natural Deduction rules. I'm new to this and find it difficult to come up with proof strategies. The first thing I do is to assume $r$ but ...
0
votes
1answer
19 views

natrual deduction is this model wrong answer?

This model entails premise but not the conclusion But in my opinion if we use the b also in conclusion we have a proof that this premise entails conclusion or?
0
votes
1answer
74 views

Natural deduction for predicate logic

I'm trying to solve this problem: ((∀xFx)→¬(∀xPx))∧(¬(∀xPx)→(∀xFx))→∃x((Fx→¬Px)∧(¬Px→Fx)) I tried double negating the ∃x((Fx→¬Px)∧(¬Px→Fx)), but then I'm getting stuck on what to do next. How would ...
2
votes
2answers
67 views

Universal Generalisation ($\forall$ - I)

With this deduction rule, in the premise of the rule: the term to be substituted for a variable must be arbitrary (refer to an arbitrary d $\in$ D). What constitutes arbitrary and not arbitrary? $ P(...
2
votes
3answers
100 views

Proving Sequent using Natural Deduction

RTP: $P \to Q, R \to \neg Q, (S\to \neg P)\to R \vdash (\neg T ∨ P)\to(T \to S)$ using primitive rules of natural deduction. I've attempted this question multiple times but keep getting stuck on ...
2
votes
2answers
52 views

Confusion over semantics behind ∃-elimination

$\exists-$ states that: if $\Sigma, A(u) \vdash B$ where u occurs nowhere else, then $\Sigma, \exists x A(x) \vdash B$. Why does this translate to $\exists$ and not $\forall$? Intuitively, $A(u)$ ...
2
votes
2answers
165 views

What are the pros and cons of natural deduction relative to Hilbert-style systems?

What are the pros and cons of natural deduction relative to Hilbert-style systems? From Wikipedia, I get the impression that natural deduction proofs tend to be shorter and closer to how humans do it. ...
0
votes
2answers
78 views

Prove $(\forall x\ Q(x))\to P ⊢ \exists x (Q(x)\to P)$ using Natural Deduction [duplicate]

I have stumbled upon this predicate logic sequent which I have trouble proving using natural deduction: $(\forall x\ Q(x))\to P ⊢ \exists x (Q(x)\to P)$ I started with ∀xQ(x) → P as the premise. I ...
2
votes
1answer
80 views

Negation rules in natural deduction

There are various treatments of using negation in natural deduction for classical logic. Let me quote bits of it: $$\frac{}{\top}\top I$$ $$\frac{\bot}{A}\bot E\quad ex\ falso\ quodlibet$$ $$\frac{A\...
0
votes
2answers
80 views

How to proof “(𝑃∧𝑄)→¬(¬𝑃∨¬𝑄)” is a tautology [duplicate]

That is part of my homework and I really have no idea about that. Really need some help. There is the question: In our proof system for Sentential, if there is a proof of ℬ from 𝒜 then 𝒜→ℬ is a ...
1
vote
2answers
64 views

Show $\vdash (\phi \to \psi) \land (\lnot \phi \to \psi) \to \psi$.

Note: $\lnot \phi$ is an abbreviation of $\phi \to \bot$. Using Dirk van Dalen. "Logic and Structure (Universitext)" as reference book. Derivation: $ \def\be{\mathsf{\tiny{\leftrightarrow} ...
4
votes
1answer
110 views

How do I prove the equivalence of $\exists x. P(x)$ and $\lnot \forall x. \lnot P(x)$ in natural deduction?

I've been trying it in Joachim Breitner's fun little Incredible Proof Machine applet (https://incredible.pm/), mostly just because it's easy to visualize that way, but I don't think that's essential. ...
3
votes
2answers
137 views

First-order de Morgan's laws for $\nvdash$

This is a continuation of my previous question about $\nvdash$. Assuming that $x$ does not occur free in $\Gamma$, it seems to me that the following two statements in (1) and (2) should hold. These ...
0
votes
1answer
58 views

How to prove ¬(P ∧ ¬Q), ¬P → Q ∴ Q using Fitch-style natural deduction system?

Once again, for the argument ¬(P ∧ ¬Q), ¬P → Q ∴ Q, I am trying to prove it using fitch style natural deduction system. However, I run into a problem with ∧Elim for ¬(P ∧ ¬Q). I can't get anything out ...
2
votes
3answers
73 views

How to find my way in this proof (fitch natural deduction proof) P → ¬Q, ¬Q → P ∴ ¬(Q ↔︎ P)

Hello all, I am very stuck in this proof. I'm still pretty much new to logic but I'm trying to get better at proofs with doing a bunch of practice proofs and this is one of them. It seems like I just ...
0
votes
1answer
37 views

Natural Deduction: Can you derive ¬(P v Q) from ¬P v ¬Q? [closed]

Can one derive ¬(P v Q) from ¬P v ¬Q in natural deduction? Upon inspection these rules look the same, how would one derive this in an application such as https://proofs.openlogicproject.org/?
0
votes
3answers
176 views

Natural Deduction: Prove $⊢ (A → B) ∨ (B → C)$

Target: Prove $⊢ (A → B) ∨ (B → C)$ without using LEM. I may be way off here, but is it valid to solve the above with the following or-elimination pattern: Answer: No, it is not possible to prove ...
1
vote
2answers
70 views

Natural deduction - finishing the proof

Give a natural deduction proof of ($\neg A \lor B) \Leftrightarrow C$ from hypotheses $\neg A \to C$ and $B \Leftrightarrow C$ My attempt so far: $\neg A \to C$ $B \Leftrightarrow C$ C $\neg A$ (1,3,...
1
vote
1answer
46 views

RTP: ⊢ $(A \to (A \to B)) \to (A \to B)$ using only primitive rules of natural deduction

Context: Uni introductory predicate logic course question I need to prove $(A \to (A \to B)) \to (A \to B)$ using only the primitive rules of natural deduction. I know that since I have no premises, ...
3
votes
0answers
45 views

''Relax Type'' in Computational Logical Framework

I am reading a nlab article about Matt Oliveri's computational logical framework. It introduces new type constructors such as $\textsf{Relax}$. I tried to read the author's justification for the ...
1
vote
2answers
63 views

Natural deduction proof dilemma

Give a natural deduction proof of $A \land (B \rightarrow \neg C)$ from hypotheses $A \land D$ and $A \rightarrow \neg C$. My attempt so far: $A \land D$ $A \rightarrow \neg C$ A (1, $\land e$) $\...
1
vote
1answer
73 views

Natural Deduction Proof for $p\land q \rightarrow r \vdash (p \rightarrow r) \lor (q \rightarrow r)$

Can anyone give me some hints on how to prove $p\land q \rightarrow r \vdash (p \rightarrow r) \lor (q \rightarrow r)$ with natural deduction? I have spend hours trying to prove it to no avail. I know ...
0
votes
3answers
66 views

Natural Deduction proof - Is it correct?

Let me know if this proof is correct. This is in french. Translation French --> English prémisse = premise supposition = assumption I now know that this is 100% incorrect. Does anyone know how to ...
0
votes
5answers
172 views

How do I solve prove this natural deduction problem?

Premises: $\neg(A \to B)\ ,\ \neg B \to C$ . Conclusion: $C$ My intuition is that I should do a sub-derivation where I prove $\neg C$ is an absurdity. However, I soon run into issues. If I could ...
1
vote
1answer
92 views

Natural deduction proof (Fitch) - Alternative using disjunction exclusion

I have to build a fitch proof for the negation introduction rule with some constraints: I cannot use ¬¬E, ¬I, RAA (Reductio ad absurdum) and ¬¬I. There is also another constraint saying that I have ...
0
votes
3answers
73 views

Natural deduction proof $(p→¬p ) ⊢ (p→r)$

I'm just learning natural deduction and I'm struggling how to prove $(p→¬p ) ⊢ (p→r)$ properly. Especially I'm wondering what to get $r$ to the implication. Premise: $(p→¬p)$ Assume: $p$ Eliminate $→$ ...
1
vote
2answers
125 views

Predicate Logic and Inference

Assume that given three predicates are presented below: $H(x)$: $x$ is a horse $A(x)$: $x$ is an animal $T(x,y)$: $x$ is a tail of $y$ Then, translate the following inference into an inference using ...
3
votes
2answers
66 views

Prove $(s \to p) \to (s \to q)$ using propositional logic [duplicate]

I need to demonstrate $(s \to p) \lor (t \to q) \vdash (s \to q) \lor (t \to p)$ I know that, if I can do something like the following, I can succesfully demonstrate the validity of this logical ...
-1
votes
2answers
76 views

Swapping implications - I have no idea where to begin with this [closed]

$(s \to p) \lor (t \to q) \vdash (s \to q) \lor (t \to p)$ This has been giving me a terrible headache. I have no idea how to go about proving this. I'm not asking for a complete solution, I just need ...
4
votes
1answer
109 views

Predicate Logic - Natural deduction

Does the set of inference rules of Gentzen’s Natural Deduction have redundancy in the sense that without some rule of the system it can still be complete? My thoughts: I came across this question and ...
2
votes
1answer
134 views

Natural Deduction Proof with Quantifiers Proof Validation

Only using natural deduction prove: $$\frac{\forall x P(x) \\ \forall x \lnot Q(x) \lor \forall yQ(y) \\ \exists x [P(x) \rightarrow \lnot Q(x)]}{\therefore \forall x \lnot Q}$$ My solution: $1. \...

1
2 3 4 5
16