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.
121
questions
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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'...
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$ ...
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 ...
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 ...
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 ...
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 ...
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 ...
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) \...
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-...
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 ...
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 ...
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 ...
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 ...
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$ [...
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 ...
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 ...
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 ...
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 ...
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.
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 ...
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 ...
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.
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 ...
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 ...
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 ...
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. ...
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$ ...
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 ...
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)$...
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 ...
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\{\...
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 ...
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 ...
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 ...
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\...
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!...
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
...
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.....
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 ...
-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 ...
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 \...
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 ...