Questions tagged [natural-deduction]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
0 votes
0 answers
27 views

Why is it simpler to express the cut-elimination rule in general deductive systems than strictly formal systems?

This article says: Depending on the strength of the metalanguage used to define the judgments and steps, simply having a deductive system does not in itself necessarily yield an effective procedure ...
Julius Hamilton's user avatar
0 votes
0 answers
29 views

Prove with natural deduction

Prove P ∨ Q, Q ∨ R, P → ¬R |- Q with natural deduction. P ∨ Q, premiss Q ∨ R, premiss P → ¬R, premiss ... ... Conclusion, Q I dont know how to properly solve this question? I know somewhat how to ...
phuck's user avatar
  • 1
0 votes
2 answers
117 views

Elemination of duplicate premise

Suppose that I have proof tree starting with some statement |- B in a sequent calculus, leading to two premises/leafs |- A. Is it always possible to transform such a proof tree into another proof tree,...
aiquita's user avatar
  • 11
1 vote
1 answer
81 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 ...
Jesús Díaz Castro's user avatar
-1 votes
4 answers
619 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 ...
Smiley's user avatar
  • 9
1 vote
1 answer
170 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 ...
Smiley's user avatar
  • 9
2 votes
1 answer
950 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 ...
Newbie123's user avatar
  • 125
2 votes
1 answer
196 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,...
iMrFelix's user avatar
  • 121
1 vote
1 answer
541 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 ...
Jay Jay's user avatar
  • 69
1 vote
0 answers
34 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 ...
Arth Patel's user avatar
1 vote
1 answer
82 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... ...
Stephane Rolland's user avatar
4 votes
2 answers
356 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 ...
Robert's user avatar
  • 143
5 votes
2 answers
603 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 ...
user1868607's user avatar
  • 2,194