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
2 votes
4 answers
434 views

Propositional Logic - Can you Derive $C \to A$ from $A$ alone, given the introduction rule?

Apparently, according to the Conditional Introduction rule, this is valid: Prove $C \to A$ Source: http://kpaprzycka.wdfiles.com/local--files/logic/W12R Page 5 So before this, the way I viewed ...
user2901512's user avatar
  • 2,070
6 votes
4 answers
3k views

natural deduction: introduction of universal quantifier and elimination of existential quantifier explained

Currently, I am dealing with the calculus of natural deduction by Gentzen. This calculus gives us rules to manipulate so-called sequents. Definition. If $\phi_1,\dots, \phi_n,\phi$ are formulas, then ...
ooooooo's user avatar
  • 223
13 votes
6 answers
912 views

Calculus of Natural Deduction That Works for Empty Structures

Currently, I am dealing with the calculus of natural deduction by Gentzen. This calculus gives us rules to manipulate so-called sequents. Definition. If $\Gamma$ is a set of formulas and $\phi$ a ...
ooooooo's user avatar
  • 223
5 votes
2 answers
3k views

Given ∃x.¬p(x), use the Fitch System to prove ¬∀x.p(x).

What I am thinking was I need two formulas, AX.p(X) => something AX.p(X) => ~ something I guess something maybe is the p(x) and the other is ~p(x) since we was given EX.~p(x)..But actually it can't ...
tang aqua's user avatar
  • 133
5 votes
2 answers
9k views

Proving 'Law of Excluded Middle' in Fitch system

I'm taking a course from Stanford in Logic. I'm stuck with an exercise where I'm doing some proof. The Fitch system I'm given only allows $ \land $ introduction and elimination $ \lor $ introduction ...
Tudor Timi's user avatar
4 votes
3 answers
5k views

How to prove that $P \rightarrow Q$ is equivalent with $\neg P \lor Q $?

In my book about Logic, which is called 'Language, Proof and Logic', by the way, there is explained that the conditional $ P \rightarrow Q $ is equivalent with $\neg P \lor Q$. There is another ...
Qqwy's user avatar
  • 348
2 votes
2 answers
713 views

How is the implication introduction used here?

I don't understand how the implication intruductions, the ones marked with the subscript $2 $ and $3 $ are used here. As I unerstand it, the implication introduction is used when we have a derivation ...
Alexander's user avatar
  • 2,237
8 votes
5 answers
11k views

Prove that $\vdash p \lor \lnot p$ is true using natural deduction

I'm trying to prove that $p \lor \lnot p$ is true using natural deduction. I want to do this without using any premises. As it's done in a second using a truth table and because it is so intuitive, I ...
Kasper's user avatar
  • 13.5k
5 votes
1 answer
180 views

Does an inference rule under natural deduction operate on sequents or formulas?

In natural deduction, is it correct that an inference rule operates on sequents which have only one formula on their right hand sides? Why does an inference rule seem to operate on formulas in Hurley'...
Tim's user avatar
  • 47.4k
5 votes
4 answers
4k views

Natural Deduction Tautology

I'm trying to prove the following tautologies: \begin{align} & ⊢ (A \to (B \to A)) \\ & ⊢ ((A \to B) \to A) \to A \end{align} For the first one, what I did was: $A$ assumption $B$ ...
user146767's user avatar
4 votes
2 answers
590 views

Prove the undecidability of a formula

I'm studying natural deduction for classical propositional logic, and I'm struggling with a point I cannot understand: when the book listed all the rules for natural deduction, it simply said that we ...
LuxGiammi's user avatar
  • 511
2 votes
3 answers
772 views

Restrictions on the use of universal generalization

I am currently reading a book on natural deduction, and it states that for universal generalization or $\forall$-introduction, defined as: $$\frac {\phi[t/x]} {\forall x \phi}$$ The following ...
esotechnica's user avatar
2 votes
1 answer
971 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 ...
Luen's user avatar
  • 97
1 vote
2 answers
377 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 ...
rentbuyer's user avatar
  • 312
1 vote
4 answers
344 views

Need Hints Prove "$((\neg \alpha \to \alpha) \to \alpha) $" Using Axiom 1,2,3 and MP and deduction theorem

$((\neg \alpha \to \alpha) \to \alpha) $ Hi, I am trying to prove this. Can someone gives me some hints to start the question... My friend told me I might need to use deduction theorem here, but I ...
kengkeng's user avatar
  • 129
0 votes
1 answer
2k views

prove $( \lnot \lnot p \Rightarrow p) \Rightarrow (((p \Rightarrow q ) \Rightarrow p ) \Rightarrow p )$ with intuitionistic natural deduction

I'm trying to prove this statement with intuitionistic natural deduction using inference rules like this example : this is the statement I'm trying to solve : $$( \lnot \lnot p \Rightarrow p) \...
ZEE's user avatar
  • 193
0 votes
2 answers
9k views

Prove if a = b, then f(a) = f(b) for any function f (with natural deduction)

I want to be able to prove that for all functions f, that $a = b \to f(a) = f(b)$. That this is true is obvious, but I'm not sure how to formally prove it using only the rules of inference in first-...
esotechnica's user avatar
53 votes
9 answers
10k views

"Modus moron" rule of inference?

This is an exercise I got from the book "First Order Mathematical Logic" by Angelo Margaris (1967). I have never heard of this rule before, the question is whether what Margaris calls the modus moron ...
user avatar
17 votes
2 answers
6k views

Difference between Logical Axioms and Rules of Inference

What's the difference between Logical Axioms and Rules of Inference? In my understanding, both are ordered pairs of formulas which are used to reach a conclusion through syllogisms. My questions Can ...
Incognito's user avatar
  • 1,195
8 votes
3 answers
38k views

Proving De Morgan's Law with Natural Deduction

Here is my attempt, but I'm really not sure if I've done it right; as I'm just about getting the hang of Natural Deduction technique. Have I done it correctly? If not, where did I make errors and ...
Haxify's user avatar
  • 435
7 votes
4 answers
836 views

Show that $(p \to q) \lor (q \to p)$ is a tautology

I tried to prove that $(p \to q) \lor (q \to p)$ is a tautology. I used $p$ and $¬q$ as conditions. (Premises 1 and 5) I managed to get to a solution, but I'm not sure if it's right. Can you please ...
AYELET's user avatar
  • 71
6 votes
2 answers
182 views

Are the two Or-Elims equivalent?

We have: $\varphi \lor \psi, \neg \varphi \vdash \psi$ $\varphi \lor \psi, \varphi \to \chi, \psi \to \chi \vdash \chi$ Using $2$ and explosion (ex falso), one can prove $1$: $\varphi \lor \psi$ [...
Kenny Lau's user avatar
  • 25k
5 votes
2 answers
627 views

Countable set of truth assignments satisfying set of well formed formulas

I am trying to answer the following question posed in my logic class: (throughout we work in propositional logic) is there a set $S$ of well-formed-formulas (wffs) satisfied by countable set $V$ of ...
youngbuck25's user avatar
5 votes
5 answers
2k views

Why not ban nested quantifiers over the same variable?

People seem to think (1, 2, 3) that a wff can have nested quantifiers over the same variable, e.g., $\forall x(Px \wedge \exists x Qx)$. However, consider the following argument: $\forall x \exists ...
Joshua Meyers's user avatar
4 votes
1 answer
441 views

Converse of Deduction Theorem

I have a basic question about natural deduction and deduction theorem. I learn from my textbook that the deduction theorem $$\textit{If }\ \Gamma,A\vdash B,\ \textit{ then }\ \Gamma\vdash A\rightarrow ...
Kelly's user avatar
  • 581
3 votes
2 answers
191 views

Peano/Presburger axioms - "find" numbers lower or equal than another number

[EDIT/CONCLUSION] It turns out it was actually working.. I was just like too stupid to let the prover run for more time and assumed it would take a lot / not be able to prove with what I've provided ...
PhantomR's user avatar
  • 342
3 votes
2 answers
436 views

How to prove this sequent using natural deduction?

How do I prove $$S\rightarrow \exists xP(x) \vdash \exists x(S\rightarrow P(x))$$ using natural deduction? Just an alignment of which axioms or rules that one could use would be much appreciated.
ryekos's user avatar
  • 35
3 votes
3 answers
1k views

The problem of Free Variables in natural deduction rules ($\forall$, $\exists$, =).

I am in need of some clarification relating to the rules mentioned. I am doing two different courses on Logic (Philosophy / Computer Science departments) and unforunately they use slightly different ...
Szmagpie's user avatar
  • 2,449
3 votes
2 answers
5k views

Modus Tollens Proof

I came across the following proof in the book Logic, by Paul Tomassi: (P & Q) → ~R : R → (P → ~Q) According to the author, the proof should be a simple application of modus tollens. The following is ...
User4407's user avatar
  • 455
3 votes
4 answers
718 views

Prove using Natural Deduction in predicate logic $(\forall x\ P(x))\to Q ⊢ \exists x (P(x)\to Q)$

I couldn't find a proper answer. I am pretty sure the universal quantifier elimination rule can't be applied directly and I tried proving by contradiction, but couldn't complete it.
varkey's user avatar
  • 33
3 votes
1 answer
536 views

Does sequent calculus have axiom?

Are axioms inference rules without assumptions, or not inference rules at all? I heard that sequent calculus doesn't have axioms, is that true? p69 in §6. Summary and Example in IV. A Sequent ...
Tim's user avatar
  • 47.4k
2 votes
2 answers
1k views

Trying to prove $p,p \to (r \to q) \vdash (\neg q \to \neg r)$ by using natural deduction.

Inference rules allowed are: $\lor$, $\wedge$, $\rightarrow$, $\neg$ introductions and eliminations. In question, it says I am allowed to make use of a lemma or equivalence as long as I provide a ...
Bonellia's user avatar
  • 123
2 votes
2 answers
2k views

Natural deduction proof / Formal proof : Complicated conclusion with no premise

Find a formal proof for the following: $\vdash [(\neg p \land r)\rightarrow (q \lor s )]\longrightarrow[(r\rightarrow p)\lor(\neg s \rightarrow q)]$ As you can see. No premise to use. We have to use ...
ex.nihil's user avatar
  • 934
2 votes
2 answers
950 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. ...
MWB's user avatar
  • 565
2 votes
1 answer
160 views

Logic justification for the use of "Let $y = ...$" in Existential proof. [duplicate]

Working on the book: Daniel J. Velleman. "HOW TO PROVE IT: A Structured Approach, Second Edition" (p. 127) Theorem. For every real number x, if $x > 0$ then there is a real number $y$ ...
F. Zer's user avatar
  • 2,323
2 votes
1 answer
311 views

Do inference rules mean the same in a Hilbert system and in a natural deductive system?

Is it correct that Enderton's A Mathematical Introduction to Logic uses a Hilbert style system for first order logic? On p110 in SECTION 2.4 A Deductive Calculus in Chapter 2: First-Order Logic Our ...
Tim's user avatar
  • 47.4k
2 votes
2 answers
1k views

Natural deduction, Proof $\vdash$ $P\Rightarrow(Q\Rightarrow P)$

So I have a question regarding natural deduction, are we allowed to "copy" our previous assumption inside a new assumption. I will use an example to illustrate. $\vdash$ $P\Rightarrow(Q\Rightarrow P)$...
some1fromhell's user avatar
1 vote
1 answer
177 views

Using natural deduction to prove that $p \implies q \vdash \lnot p \lor q$

Using only rules of natural deduction, I am trying to prove that $$p \implies q \vdash \lnot p \lor q$$ but am having a lot of difficulty. I was able to prove the other direction. Could anyone show ...
Thomas Formal's user avatar
1 vote
1 answer
1k views

Rule T in First-Order Logic

In Enderton's A Mathematical Introduction to Logic (second edition, page 118), we are given the so-called Rule T (Lemma $24C$) : If $\Gamma\vdash\alpha_1,\ldots,\Gamma\vdash\alpha_n$ and $\left\{\...
Demosthene's user avatar
  • 5,420
1 vote
4 answers
8k views

Prove :(P → Q) ∨ (Q → P) using natural deduction

Allowed inference rules: ∨-I, ∨-E, ∧-I, ∧-E, →-I, →-E, ¬-I, ¬-E I tried to prove a contradiction by assuming $¬ ((P → Q) ∨ (Q → P))$ but got stuck, or am I doing it in the wrong way? Edit: My proof ...
ccy1997's user avatar
  • 13
1 vote
1 answer
674 views

Is this a proof of how law of the excluded middle implies double negation elimination?

Here is a proof for double negation elimination. I wanna know if it's a proof of how law of excluded middle implies double negation elimination, since there's usage of rule of explosion (ex falso ...
Pooria's user avatar
  • 477
1 vote
1 answer
88 views

Prove $\vdash \neg(\square F\land p)$ in $KD$

How to prove that $\vdash \neg(\square F\land p)$ in $KD$? The allowed rules are natural deduction rules and the axiom $\square p\to\diamond p$ where $\diamond p=\neg\square\neg p$. I actually don't ...
user557's user avatar
  • 11.9k
1 vote
1 answer
96 views

$\vdash\phi \land \diamond\psi \to \diamond(\psi\land\diamond\phi)$ in KB

I've been trying to prove $\vdash\phi \land \diamond\psi \to \diamond(\psi\land\diamond \phi)$ in natural deduction where it's allowed to use $\phi\to \square \diamond \phi$ and/or $\diamond\square\...
user557's user avatar
  • 11.9k
0 votes
2 answers
158 views

Natural deduction proof of $p \lor (p\implies q)$ with propositional calculus [closed]

I'm having a bit of trouble proving this with the propositional calculus rules. $$p \lor (p\implies q)$$ Would someone mind helping me and showing which rules they've used with an explanation! Thanks!...
Petra J's user avatar
  • 11
0 votes
1 answer
162 views

Natural Deduction - How to define literals?

I'm currently working on the following question: "At least one of Plato and Democritus believed in the theory of forms. Plato believed in the theory of forms only if he was not an atomist, and ...
Scyther's user avatar
  • 11
0 votes
1 answer
342 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.....
lucasbbs's user avatar
0 votes
2 answers
139 views

Proving $\forall x (A\to B) \to(A \to \forall x B):x\notin \mbox{free}(A)$ in a Hilbert system where it is not an axiom

I have no idea whether this question is way too specific or whether something similar has already been asked (we still need to work out a way to search for formulas I guess). Anyways here I go: I ...
masterxilo's user avatar
-1 votes
2 answers
90 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 ...
Francisco's user avatar
  • 121
36 votes
9 answers
3k views

**Ended Competition:** What is the shortest proof of $\exists x \forall y (D(x) \to D(y)) $?

The competition has ended 6 june 2014 22:00 GMT The winner is Bryan Well done ! When I was rereading the proof of the drinkers paradox (see Proof of Drinker paradox I realised that $\exists x \...
Willemien's user avatar
  • 6,562
10 votes
1 answer
1k views

Relationship between sequent calculus and Hilbert systems, natural deduction, etc

I am trying to learn the basics of logic and I'm confused on how these proof systems work together. The big ones I see are Hilbert style, and then Gentzen style which includes natural deduction, and ...
Brandon L's user avatar
  • 123