# Tag Info

## New answers tagged natural-deduction

0

As usual the key is to work backwards. To introduce the universal, assume an arbitrary variable, $a$, then derive $P(a)\to\lnot Q(a)$. To introduce that conditional, assume $P(a)$ then derive $\lnot Q(a)$. To introduce that negation, assume $Q(a)$, then derive a contradiction. To derive that contradiction under the assumptions of $\lnot\exists x~(P(x)\land Q(... 1$\lnot \exists x (P(x) \land Q(x))$--- premise$P(a)$--- assumed [a]$Q(a)$--- assumed [b]$\exists x (P(x) \land Q(x))\bot\lnot Q(a)P(a) \to \lnot Q(a)\forall x (P(x) \to \lnot Q(x))$1 Universal elimination when$∀$is not the main operator. You cannot apply UE when the quantifier is not the main operator. You have to derive$\forall x A(x)$in order to use it to "detach"$B$using ($\to$-E):$\forall x A(x) \to B$--- premise$\lnot \exists x (A(x) \to B)$--- assumed [a]$\lnot A(y)$--- assumed [b]$A(y)$--- assumed [c] ... 0 Natural Deduction Proof for Modus Tollens Using a simple form of natural deduction... 2 I have seen natural deduction proofs that are very complicated, or are written in a way such that I suspect that there is some motivation that I am surely missing. But I can't figure out how to get the intuition/motivation for natural deduction proofs in general. The following proof is based on a form of natural deduction. Simpler than most, it may help. It ... 1 I’d do this the following way similarly to what @Mauro has been hinting at in comments but I’m not sure if this is correct in the system for natural deduction you are using. I’ll use numbers to indicated the levels of „nested proofs”, this is the method of natural deduction I am used (so there are rules for introducing and eliminating different connectives ... 0 instructions state that I have to show it through the Laws of natural deduction. What really confuses me is how to derive ~A Prove$A\lor B\vdash (A\lor(B\land A))\lor(B\land\lnot A)$via an indirect proof containing a proof by cases. The derivation of$\lnot A$takes place inside the context of the indirect subproof, and is in fact done via the first ... 0 You have to show that the sentence A∨B$\Leftrightarrow$(A∨(B∧A))∨(B∧¬A) is a tautology, that is true for every possibile truth value of A and B, you can do it using a truth table. 0 The reiteration rule follows from a natural deductive proof system which uses an inference rule called "Addition". Specifically the addition rule says from$P$we can infer$P \lor Q $, for any statement$Q$. In some cases reiteration is trivial, for instance if the statement is a premise you can cite the same premise as many times as you want, ... -1 Hint: Assume to contrary that$\neg ((A\to B) \lor (B\to A))$is true. Using$P\to Q ~\equiv ~ \neg(P \land \neg Q)$, De Morgan's Law and removal of '$\neg\neg$', obtain the contradiction$A\land \neg A$. 1$\def\fitch#1#2{~~~~\begin{array}{|l}#1\\\hline#2\end{array}}A\to B$is not a tautology, so you will not be able to derive it with no assumptions. Rather your indirect proof requires first making the assumption of$\lnot((A\to B)\lor(B\to A))$, and then you must derive$A\to Bunder that. \fitch{}{\fitch{\lnot((A\to B)\lor(B\to A))}{\fitch{A}{~~\vdots\\... 0 Since X\to Y and \neg X\vee Y are equivalent, one has that \begin{align*} A\to((A\to B)\to B) & \Longleftrightarrow (\neg A)\vee(\neg(\neg A\vee B)\vee B)\\\\ & \Longleftrightarrow (\neg A)\vee((A\wedge\neg B)\vee B)\\\\ & \Longleftrightarrow (\neg A)\vee((A\vee B)\wedge(\neg B\vee B))\\\\ & \Longleftrightarrow (\neg A)\vee(A\vee B)\\\\ &... 2 Let us get you started with the derivation for \exists x~.P(x)~\lor~\exists x~.Q(x)\vdash \exists x~.(P(x)\lor Q(x)) using the Gentzen tree system.\dfrac{\exists x~.P(x)~\lor~\exists x~.Q(x)\\\qquad\qquad\vdots}{\exists x~.(P(x)\lor Q(x))}{?}$$Well, existential statements may be derived either by construction, or by reduction to absurdity. Which is ... 0 How to build a derivation of p\to q\vdash\lnot q\to\lnot p from the bottom up; in sequent form or using the Gentzen tree format. So the last step of the proof will be to introduce that conditional.$$\begin{split}p\to q, \lnot q&\vdash \lnot p\\\hline p\to q&\vdash \lnot q\to\lnot p&\quad&{\small (\to\textsf{intro})}\end{split}\qquad\lower{... 1 Hint: the proof has 3 instances of an elimination rule. Consider that the premise has as the principal operator a Vel, whereas on the right we have an existential quantifier. Try to work backward to see what you need: clearly the last rule will be an application of\exists$-introduction after a derivation of the formula$Pa \lor Qa$. If you're still stuck ... 0$\def\fitch#1#2{~~~~~\begin{array}{|l}#1\\\hline #2\end{array}}$It might be worth noting that any proof will necessarily involve something like excluded middle or double negation elimination - the statement is not valid in intuitionistic first-order logic. Here's Mauro ALLEGRANZA's LEM proof, reformatted. $$\fitch{~~1.~~Pa\to\exists y~Qy\hspace{21ex}\... 2$$\forall x (P(x) \lor Q(x)) , \forall y. \neg P(y) \vdash \forall x.Q(x)$$Start at the end. Keeping an eye on where you want to go will help you get there.$\dfrac{A}{\forall x~.A[x\backslash t]}{\forall\mathsf{intro}}$means that when given a predicate you may generalise to a universal by replacing all instances of the arbitrary free variable with a ... 0 So as for the first rule of natural deduction you can only use the elimination of the universal quantifier; can you go on from there? it is just like PL until (and not including) the last necessary rule. 1$p \to q \qquad$axiom$\neg q \qquad$auxilliary proposition$p\qquad$auxilliary proposition$q\qquad$elimination of$\to$(lines 1, 3)$\Bbb{F}\qquad$introducion of$\Bbb{F}$(lines 2, 4)$\neg p\qquad$introducion of$\neg$(lines 3, 5)$\neg q \to \neg p\qquad$introdution of$\to$(lines 2, 6) 1 assume p and$\neg q$Then q and$\neg q$by modus ponens contradiction therefore$\neg p\neg q\to\neg p$0$P\to Q\vdash\lnot(P\land\lnot Q)\$ I (mostly) understand the introduction and elimination rules for connectives, but I just don't know what to do here. I know I've got to turn the premise into the conclusion step by step using introduction and elimination of these logical connectives, but how? You seek to derive a negated statement.   Negation Introduction ...

Top 50 recent answers are included