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.
891
questions
0
votes
0
answers
42
views
Proof in Natural Deduction, Sequent Calculus or Hilbert System
Is there any smart way to check if certain statements are not provable in any of these proof systems?
Like for example the following task:
Prove or disprove the following statements:
$\vDash \exists ...
- 69
1
vote
0
answers
45
views
Soundness and completeness of Fitch-style for first order logic
I am looking for literature in which a detailled proof of the soundness and completeness of Fitch-style proofs for first order logic is given. In his 1952 book "Symbolic Logic, An Introduction&...
- 171
0
votes
1
answer
41
views
Can the Natural Deduction rule "$\exists$-Introduction" be derived from other rules? [closed]
Can the Natural Deduction rule (for First-Order Logic) "$\exists$-Introduction" be derived from other Natural Deduction rules? The rule states that if $(P_1, P_2, \dots, P_n)$ is a proof, ...
- 11k
1
vote
1
answer
73
views
How/where is this technique generalised and proven for other (standard, first order) logical operations (if possible)? A method of natural deduction.
Logic is something I am entirely self-taught in. Due to my resulting ignorance, it is difficult for me to search for the right things. Therefore, please excuse me if this has been asked before.
The ...
- 41.9k
2
votes
0
answers
85
views
Can this rule of inference do replace axiom of extensionality?
If I replace the below axiom in ZFC (or NBG) by the below inference rule, there are any consequence in what can be demonstrated?
Axiom: If two sets (or classes) have the same elements then their are ...
0
votes
1
answer
89
views
How to derive $ \forall x \exists y \forall z \exists w \;\; (Q(x, y) \lor \lnot Q(w, z))$?
I have to give a natural deduction proof of the statement:
$$ \emptyset \;\; \vdash \;\; \forall x \exists y \forall z \exists w \;\; (Q(x, y) \lor \lnot Q(w, z)) $$
This is a valid formula as per ...
- 1,988
0
votes
1
answer
52
views
How to prove ¬p ∧ ¬q ⊢ ¬(p ∨ q) by natural deduction?
Here's my attempt, but I think it's incorrect because I don't discharge assumption 1:
¬p ∧ ¬q $\qquad$ premise
¬p $\qquad$ by (∧E)
¬q $\qquad$ by (∧E)
p $\qquad$ assumption¹
p ∨ q $\qquad$ ...
- 207
0
votes
1
answer
53
views
How to prove $\neg q \rightarrow \neg p \vdash p \rightarrow q$ and $\neg (p \lor q) \vdash \neg p \land \neg q$ by natural deduction?
For the first proof, I actually finished but I'm not sure if it is correct.
Proof for $\neg q \rightarrow \neg p \vdash p \rightarrow q$:
$\neg q \rightarrow \neg p$, $[p]^1$, $[\neg q]^2$
$\neg p$ by ...
- 207
0
votes
0
answers
47
views
What does it mean to discard a hypotesis in a natural deduction?
My textbook says that in the deductive system of natural deduction every hypotesis must be discarded by a rule of inference and after being discarded, it cannot be used again in the deduction... But ...
- 207
1
vote
1
answer
107
views
Trying to understand "Deriving natural deduction rules from truth tables" and having trouble with false hypothetical judgments
For rows of the truth table where the connective is false the connective is placed as a judgement. This doesn't make sense to me. Having the false proposition be in the hypothetical position makes ...
0
votes
1
answer
56
views
Prove that contrapositive rule is equivalent to the rule of double negation
Many deduction systems I see at various places (for example here includes the following two axioms
$$
a \Rightarrow (b \Rightarrow a),\\
[a \Rightarrow (b \Rightarrow c)]\Rightarrow [(a\Rightarrow b) \...
- 6,891
2
votes
1
answer
61
views
Proof of distributivity of $\land$ over $\lor$ using disjE in natural deduction
I'm learning about natural deduction from https://www.inf.ed.ac.uk/teaching/courses/ar//slides02.pdf
I'm trying to understand its proof of
$$
P \land (Q \lor R) \vDash (P \land Q) \lor (P \wedge R)
$$
...
1
vote
1
answer
69
views
How do we know inference rules are correct?
I know axioms are statements which are assumed to be true (meaning that axioms are not proved).
Theorems are statements which can be proved or has been proved. In the proofs of theorems we can use ...
- 19
2
votes
1
answer
69
views
On the Logic of Logics
I am teaching myself logic (from various sources), and I was viewing this video: https://youtu.be/IOiZatlZtGU. I had a few questions about 'proving' statements about logic in logic.
At 16:50 (https://...
- 143
0
votes
0
answers
33
views
Getting from deduction a syntactically different conclusion
I’m trying to prove the conclusion, C, from the hypotheses, f1-f6, but I am getting stuck at a wall. After deriving f16, I’m having trouble seeing the next step.
If I resolve f16 and f12 on eat(John,p)...
0
votes
0
answers
48
views
Trying to get my head around the "For exists" rule in predicate logic.
PREDICATE LOGIC EXAMPLEI cant embed images but I've tried to link it if you can see it but if not then ill type part of the proof here:
p(x) ^ r(x,y)
r(x,y)
Ǝy.r(x,y)
so from line 1 to 2, we used ...
- 1
-1
votes
1
answer
102
views
Solve Logic puzzle using predicate logic and natural deduction [closed]
I am trying to solve this question using predicate logic and natural deduction but could only do so using propositional logic.
The cops have three suspects for the murder of Dave: Adam, Ben, and ...
0
votes
0
answers
17
views
Does proving that $\pi$ is a parsing tree suffice to say that $\phi$, its associated formula is a formula?
Let $\phi$ be an expression of $LP(\sigma)$, $\pi$ its "parsing" (planar?) tree.
If we show that $\pi$, indeed, is a proper parsing tree, that is verify that all of the defining properties ...
1
vote
1
answer
64
views
Reductio ad absurdum when there are no premises and just a supposition $S$
I was reading An Introduction to Formal Logic by Peter Smith - https://www.logicmatters.net/resources/pdfs/IFL2_LM.pdf , and on page 36 he explains Reductio ad absurdum as:
If $A_1, A_2, \dots, A_n$ (...
- 594
-2
votes
1
answer
51
views
Show that the argument (p∧q)∨(¬p∧¬q)⊢p⊃q is valid with natural deduction
Here is what I have done :
...
- 11
1
vote
2
answers
47
views
Is this predicate logic derivation valid?
Could someone please be so kind as to check the validity of my predicate derivation? I am trying to prove that the set $\{(\forall x)\lnot(\exists y)Gxy,(\forall z)[Hz\implies(\exists z) Gzy],(\exists ...
- 709
3
votes
3
answers
149
views
Why does natural deduction get its name?
For example, I want to prove $\psi$ from the assumption $\{\varphi,\varphi\to\psi\}$ , the "most natural" proof would be:
$\varphi$
$\varphi\to\psi$
$\psi$(MP)
But using natural deduction, I ...
- 135
0
votes
0
answers
28
views
what does it mean to say natural deduction is paradoxical?
In the very beginning of Chapter 2 Natural Deduction, page 8, in Jean-Yves Girard's book Proofs and Types (translated by Paul Taylor and Yves Lafont, published in 1989), the author writes:
Natural ...
- 109
-2
votes
2
answers
138
views
How to prove this using natural deduction?
could I get some help on how to solve this problem? I have been doing this course where we were asked to solve this problem and I'm stuck on how to even get started.
¬((A ∨ B)→(A ∨ C)) ⊢ (A ∨ B) ∧ ¬(B→...
- 63
1
vote
1
answer
537
views
How to make a formal proof with A → (B ∨ C) ⊢ (A → B) ∨ (A → C)
Here is what I've got so far
I feel like I need an indirect proof for this and so I need to prove a contradiction with one of line 4 or 5. I'm not sure how to approach it. Any hints that can help me ...
- 29
0
votes
0
answers
71
views
Fitch deduction question, ((A ∧ B) → C ⊢ A → (B → C))
I have been at this for 6 hours. I can't figure it out and I don't know what else to do. Please help. My problem is I don't know how to do this without assuming A&B. Here's the furthest I got:
(A ∧...
- 25
0
votes
0
answers
86
views
Is there a proof of natural deduction's negation introduction from a Hilbert-style axiom system?
Working through a book An introduction to proof theory - normalization, cut-elimination and consistency proofs, I started comparing natural deduction and Hilbert-style systems. I had some basic ...
- 33
0
votes
0
answers
37
views
Do we need introduction and elimination rules?
Can't we do logic/maths without introducing/eliminating additional operators (⊸, ⊗, ⊕, )? Isn't it enough to have mutually irreducible computation/conversion rules?
⊸ introduction & elimination:
$$...
- 9
0
votes
1
answer
183
views
Tricky proof of ∃x∃yfxy → ∃y∃xfxy using natural deduction - help appreciated!
I am trying to figure out how ∃x∃yf xy -> ∃y∃xf xy is supposed to work, using natural deduction.
I know how to use the exist elimination rule, but I usually end up somewhere where I don't know how ...
- 25
1
vote
1
answer
95
views
Natural deduction moving quantifiers
I have difficulties proving with natural deduction the following:
$$Ga\rightarrow\exists xFx \vdash \exists x(Ga\rightarrow Fx)$$
Thanks for the help!
- 335
1
vote
2
answers
94
views
How to prove (¬¬x→¬¬y) ⊢ (x→y)? [closed]
How to prove (¬¬X→¬¬Y) ⊢ (X→Y) ?
What I've done:
[~X] ¬¬X→¬¬Y implication exclusion
[Y] ¬Y AND introduction
...
- 237
1
vote
1
answer
110
views
First-order logic: where's the the flaw in this argument?
There must be a flaw in the following argument, but I don't see it at the moment. Who can point it out?
In first-order logic, suppose that a structure $\mathfrak{U}$ is a model of the formula ($x = 3$...
- 121
1
vote
1
answer
76
views
What strategies could be used to prove the validity of this argument in order to not violate restrictions on universal generalization (Hurley)
I'm considering a particular argument while working through Hurley's Concise Introduction:
...
- 11
0
votes
0
answers
47
views
can I falsify a traditional inference with modern natural deduction like system?
I can represent a traditional syllogism with the language of first-order predicate logic.
and If the syllogism is valid, then I can prove it with natural deduction system or tableaux.
If the syllogism ...
- 89
0
votes
3
answers
106
views
How to prove $A \to (B \lor C)$ therefore $(A \to B) \lor (A \to C)$? [closed]
In doing this proof I found a solution, but I believe it to be incorrect because within the proof it uses
assume A
.
.
. . . assume C
. . . A -> C
Is it valid to conclude A -> C in the same ...
4
votes
1
answer
128
views
Natural Deduction: An unusual presentation?
1. Context
On page 241 of their paper Natural deduction and coherence for weakly distributive categories Blute et al give the right- and left-introduction rules of multiplicative conjunction for (...
- 2,630
0
votes
0
answers
45
views
Predicate Logic: Deduction for Quantifiers
So, I was bothered by the question of natural deduction wherein we have to prove ∀h(Fh ⇒ Fk) from premise ∃g Fg ⇒ Fk given that k is a constant which isn't used before
To get the conclusion in ∀(_) ...
0
votes
1
answer
41
views
Natural Deduction: Universal Quantifiers in Predicate
How do we prove the conclusion: ∀x(Ax ∨ ⇁Ax)
This is also called LEM, i.e. the Law of Excluded Middle.
I'm confused while proving this because for ∀x, deduction assuming some constant is required.
So, ...
- 97
0
votes
1
answer
58
views
Propositional Logic: Natural Deduction using Elimination and Introduction rules
So, we have to prove ⇁Y as conclusion from premises:
A. (X ∨ Y) ⇒ (X ∧ Y)
B. ⇁X
What I’ve tried so far is basically:
⇁X [Premise]
⇁X ∨ (X ∧ Y) [∨In, 1]
(X ∨ Y) ⇒ (X ∧ Y) [Premise]
.
.
.
n. X ...
user1056624
1
vote
2
answers
125
views
Proving $\exists x\lnot R(x), \forall x(P(x)\to Q(x)), \forall x(\lnot Q(x) \lor R(x)) \vdash \exists x\lnot P(x)$
This is the proof we have to prove:
$$\exists x\lnot R(x), \forall x(P(x)\to Q(x)), \forall x(\lnot Q(x) \lor R(x)) \vdash \exists x\lnot P(x)$$
My proof:
$∀x(P(x)→Q(x))$ From data
$∃x¬R(x)$ From ...
3
votes
2
answers
131
views
A natural deduction proof of $\neg (A \leftrightarrow \neg A ) $.
I want to prove $\neg (A \leftrightarrow \neg A ) $ in natural deduction: I tried first
But I can't figure how to discharge the hypothesis $A$ and $\neg A$. I then tried
Here I just need to ...
- 4,741
0
votes
0
answers
59
views
A natural deduction proof of $\neg (A \wedge B) \rightarrow (A \rightarrow \neg B)$ without RAA
I am doing (for fun) the exercices of this lean tutorial.
For the third exercice of section 3.6. Exercises:
"Give a natural deduction proof of $\neg (A \wedge B) \rightarrow (A \rightarrow \neg ...
- 4,741
0
votes
1
answer
36
views
Given the following rule for implication-introduction, is this the same rule that discharges assumptions? [duplicate]
The following is an example that my teacher came up with during one of our earlier lectures on natural deduction.
"Given the rules of inference that we have introduced so far, reflect on whether ...
- 55
0
votes
0
answers
85
views
Tips on initial assumptions for proofs using natural deduction - with a specific example.
Here is a question that's been bugging me:
"Derive the following, using the rules of natural deduction:
$$
\vdash \neg(P_{1} \rightarrow P_{2}) \rightarrow P_{1} \vee P_{2}
$$
That is, give a ...
- 55
0
votes
1
answer
103
views
How to prove that $P_b \leftrightarrow (P_a \land P_b), P_a \leftrightarrow \neg P_b \vdash P_a$ with natural deduction
I need to build a proof for $P_b \leftrightarrow (P_a \land P_b), P_a \leftrightarrow \neg P_b \vdash P_a$ with natural deduction... I have built the following proof, however I am stuck in the middle ...
- 17
0
votes
1
answer
72
views
How to build a proof for $\vdash \exists y \forall x P(x,y) \rightarrow \forall x \exists y P(x,y)$ using the software Fitch
I want to build a proof for $\vdash \exists y \forall P(x,y) \rightarrow \forall x \exists y P(x,y)$ using the software Fitch...
I have the above proof and I want to test it to be sure I have done ...
- 17
0
votes
1
answer
233
views
How to prove that $\vdash \exists y \forall x P(x,y) \rightarrow \forall x \exists y P(x,y)$ with natural deduction in tree style
I have built the following proof for $\vdash \exists y \forall x P(x,y) \rightarrow \forall x \exists y P(x,y)$ with natural deduction in tree style.
However, I am stuck in the middle of the problem.....
- 17
-2
votes
1
answer
91
views
¬A → B , ¬B ⊢ A [closed]
not A > B :PR
not B :PR
PR = Premises
This is the strategy of the Conditional Introduction. On line 3 I'm assuming the antecedent of my goal sentence.
(You don’t have to use this vv but it’s what ...
- 19
0
votes
1
answer
118
views
Derivation (¬¬A → A) → (¬¬B → B) → ¬¬(A ∧ B) → A ∧ B.
I am struggling trying to make a derivation of this principle of indirect proof.
Starting with the needed assumptions:
u: ¬¬A → A v:¬¬B → B w: ¬¬(A ∧ B)
I thought that in order to prove A ∧ B I ...
- 45
0
votes
1
answer
73
views
Natural Deduction with Identity
I am confused on how to deal with identities in natural deduction proofs with predicate logic.
More specifically, how would one go about solving this?
...
user1044951