Questions tagged [natural-deduction]
The natural-deduction tag has no usage guidance.
10
questions
1
vote
1answer
30 views
Formal Logic - Natural deduction: Problem with assumptions about exists-negation
I'm stuck on how to progress with this proof, despite I have tried, I cannot see the next move.
Given this proof without predicate:
So far what I've accomplished:
My idea is, as I can't see any ...
0
votes
3answers
211 views
Prove (p → ¬q) is equivalent to ¬(p ∧ q)
I need to prove the above sequent using natural deduction. I did the first half already i.e. I proved $(p\rightarrow\neg q)\rightarrow \neg (p \wedge q)$, but I'm stuck on where to start for the ...
1
vote
1answer
75 views
Proving the validity of a sequent using Modus Tollens
Problem: Prove $p \rightarrow (q \vee r), \neg q, \neg r \vdash \neg p$ using Modus Tollens.
I need to prove the validity of the above sequent by using natural deduction. Initially, I didn't read the ...
2
votes
1answer
203 views
Natural deduction: understanding bottom elimination (¬e)
I am new to natural deduction and upon reading about various methods online, I came across the rule of bottom-elimination in the following example.
I do not understand the step in line 10.
Upon ...
2
votes
1answer
109 views
Natural deduction proof: distributivity of existential quantification
In a current exam-prep exercise, we were tasked to prove the following formula using natural deduction of first-order logic:
$(\exists x. P \lor Q) \rightarrow P \lor (\exists x.Q)$ for arbitrary $P,...
1
vote
1answer
154 views
Algorithm for automatic construction of natural deduction proofs
I was wondering if there exists any algorithm for automatic construction of nautral deduction proofs. I'm interested in propositional logic and first order logic.
If there is no algoritm, can you ...
0
votes
0answers
23 views
Natural deduction proof without any predicate
I am gaving trouble proving a natural deduction proof when there is no predicate given. Only conclusion is given. I understand the rules of elimnations, inclusions, IPs and others but I having trouble ...
1
vote
1answer
68 views
Some explanations needed about Negation in Gentzen's Natural Deduction rules
I'm beginning to have an understanding thanks to some videos relating to "Proposition as Types". But, I don't come from a theoretical CS background, so maybe I'm blocked probably a bit by notation...
...
4
votes
2answers
255 views
Predicate Logic - Natural Deduction; Assumptions about exists-elimination
I am stuck on how to progress with this proof; i cannot see my next move.
The task is to show $S \to \exists x Q(x) \vdash \exists x (S \to Q(x))$ using natural deduction for predicate logic.
My ...
5
votes
2answers
397 views
Explanation of implication-introduction rule
I read in Proofs and Types by Girard et alii. the following excerpt that talks about the calculus of natural deduction:
Now a sentence at a leaf (of the deduction tree) can be dead, when it
no ...
