#LyX 1.3 created this file. For more info see http://www.lyx.org/ \lyxformat 221 \textclass article \begin_preamble \usepackage{color} \usepackage{html} \usepackage{fitch} \usepackage{ae} \pagecolor{white} \end_preamble \language english \inputencoding auto \fontscheme default \graphics default \paperfontsize default \spacing single \papersize Default \paperpackage a4 \use_geometry 0 \use_amsmath 0 \use_natbib 0 \use_numerical_citations 0 \paperorientation portrait \secnumdepth 3 \tocdepth 3 \paragraph_separation indent \defskip medskip \quotes_language english \quotes_times 2 \papercolumns 1 \papersides 1 \paperpagestyle default \layout Title Introduction to natural deduction \layout Author Daniel Clemente Laboreo \layout Date August 2004 (reviewed at May 2005) \layout Standard \begin_inset LatexCommand \tableofcontents{} \end_inset \layout Section Before starting... \layout Standard This tutorial is available in several languages: \begin_inset ERT status Collapsed \layout Standard \backslash htmladdnormallinkfoot{Spanish}{http://www.danielclemente.com/logica/dn.html} \backslash htmladdnormallink{(and PDF)}{http://www.danielclemente.com/logica/dn.pdf}, \backslash htmladdnormallinkfoot{Esperanto}{http://www.danielclemente.com/logica/dn.eo.html} \backslash htmladdnormallink{(and PDF)}{http://www.danielclemente.com/logica/dn.eo.pdf}, \backslash htmladdnormallinkfoot{Catalan}{http://www.danielclemente.com/logica/dn.ca.html} \backslash htmladdnormallink{(and PDF)}{http://www.danielclemente.com/logica/dn.ca.pdf}, and \backslash htmladdnormallinkfoot{English}{http://www.danielclemente.com/logica/dn.en.html} \backslash htmladdnormallink{(and PDF)}{http://www.danielclemente.com/logica/dn.en.pdf}. \layout Standard \layout Standard \end_inset \layout Standard Formulas look much nicer in the PDF, but if it's not possible to use it, then look at the HTML pages. \layout Subsection Who am I \layout Standard My name is Daniel Clemente Laboreo, I'm 19 years old (in 2004), I live in Gavà (Barcelona, Spain), and I study Computer Science in the \emph on FIB \emph default ( \emph on UPC \emph default , Public University of Catalonia). There, in the subject called \emph on ILO \emph default ( \emph on Introduction to logic \emph default ), is where I was taught this topic. \layout Subsection Why do I write this \layout Standard Some reasons: \layout Itemize There's a big gap in the search \begin_inset Quotes eld \end_inset \emph on natural deduction \emph default \begin_inset Quotes erd \end_inset at Google. I myself needed to study it before the exam, but couldn't find anything useful which helped me. There actually existed some tutorials, but no one was good enough (in my opinion): some were too confusing, others had special characters which didn't display correctly, and others didn't explain everything (as if everyone knew all the logic concepts). So I decided to create this tutorial which I hope it will help someone. \layout Itemize It's a topic I like, and can do without much problems. \layout Itemize It makes you think. Maybe it hasn't got a lot of practical uses, but one really has to try hard and spend some time in order to solve some simple problems. \layout Itemize Well, I confess that I wrote this to learn text processing with \begin_inset ERT status Collapsed \layout Standard \backslash LaTeX \end_inset . You need some dedication to learn it, but the results make the work be worth it. \layout Subsection Whom is it addressed to \layout Standard Principally, to anyone who likes logic, computer science, or mathematics. Anyone who wants to prepare the university logic subjects will also gain some useful concepts. \layout Standard This doesn't pretend to be a complete course for natural deduction, but it will continue being an introduction. When I learn more, I will correct it if necessary, but I won't add more sections (I would write them on external documents). \layout Subsection License \layout Standard All the document is \begin_inset ERT status Collapsed \layout Standard \backslash htmladdnormallinkfoot{FDL}{http://www.gnu.org/licenses/fdl.html} \end_inset (like the GPL from free software, but for documents). The source code is made with LyX ( \begin_inset ERT status Collapsed \layout Standard \backslash htmladdnormallinkfoot{dn.en.lyx}{http://www.danielclemente.com/logica/dn.en.lyx} \end_inset ), and uses the macros \begin_inset ERT status Collapsed \layout Standard \backslash htmladdnormallink{fitch.sty}{http://www.danielclemente.com/logica/fitch.sty} \end_inset by Johan W. Klüwer. I have used the program \begin_inset ERT status Collapsed \layout Standard \backslash htmladdnormallink{latex2html}{http://www.danielclemente.com/linux/l2h.html} \end_inset (slightly patched) to create the web pages. \layout Standard You have the right, among others, to modify it or to translate it to other languages which you know well, and also to redistribute it, sell it, and more. \layout Section Basic concepts \layout Standard In logic one has to be perfectly clear of the meaning of each word. I will just remember what are and how to read the strange symbols used in this document. \layout Subsection Formalization \layout Standard \emph on To formalize \emph default means writing an expression in a standard form which anyone can understand. \layout Standard When working with logical algorithms, you can be thinking all the time in phrases like \begin_inset Quotes eld \end_inset \emph on If I have a LCD screen but it has too many dead pixels, then I need another monitor \emph default \begin_inset Quotes erd \end_inset . You can, but they are too long. It's better to represent each action with a letter, and write the phrase using such letters along with simple words like \emph on and \emph default , \emph on or \emph default , \emph on not \emph default , or \emph on then \emph default . \layout Standard For example, we have this vocabulary: \layout Standard \begin_inset Formula $L$ \end_inset : \emph on have a LCD (Liquid Crystal Display) monitor \layout Standard \begin_inset Formula $P$ \end_inset : \emph on have all pixels working perfectly, with not too many fused ones \layout Standard \begin_inset Formula $M$ \end_inset : \emph on need a new monitor \layout Standard The phrase \begin_inset Quotes eld \end_inset \emph on If I have a LCD screen but it has too many dead pixels, then I need another monitor \emph default \begin_inset Quotes erd \end_inset is better expressed by \begin_inset Quotes eld \end_inset \emph on if \begin_inset Formula $L$ \end_inset and not \begin_inset Formula $P$ \end_inset , then \begin_inset Formula $M$ \end_inset \emph default \begin_inset Quotes erd \end_inset . \layout Standard At natural deduction we will only use the version with letters, following these conditions: \layout Itemize The letters (named \emph on propositional letters \emph default ) are uppercase. \layout Itemize Normally \begin_inset Formula $P$ \end_inset , \begin_inset Formula $Q$ \end_inset , \begin_inset Formula $R$ \end_inset , \begin_inset Formula $S$ \end_inset , ... are used, but anyone else is allowed. \layout Itemize We use some special symbols for the operators \emph on and \emph default , \emph on or \emph default , \emph on not \emph default and \emph on implication \emph default . \layout Subsection Used symbols \layout Standard To express the relation between one action and another, there exist some international icons. The basic operators you must know are \begin_inset Formula $\vee$ \end_inset , \begin_inset Formula $\wedge$ \end_inset , \begin_inset Formula $\neg$ \end_inset , \begin_inset Formula $\Rightarrow$ \end_inset . The others are more complex, but here I put all of them as a reference, to be able to find them if you were searching any of them. \layout Standard \begin_inset Tabular \begin_inset Text \layout Standard \series bold Symbol \end_inset \begin_inset Text \layout Standard \series bold It's read... \end_inset \begin_inset Text \layout Standard \series bold Description \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\vee$ \end_inset \end_inset \begin_inset Text \layout Standard \emph on or \end_inset \begin_inset Text \layout Standard \begin_inset Formula $A\vee B$ \end_inset is true whenever one of the two, or both, are true. \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\wedge$ \end_inset \end_inset \begin_inset Text \layout Standard \emph on and \end_inset \begin_inset Text \layout Standard To make \begin_inset Formula $A\wedge B$ \end_inset true, both \begin_inset Formula $A$ \end_inset and \begin_inset Formula $B$ \end_inset have to be true. \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\neg$ \end_inset \end_inset \begin_inset Text \layout Standard \emph on not \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\neg A$ \end_inset only is true when \begin_inset Formula $A$ \end_inset is false. \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\Rightarrow$ \end_inset \end_inset \begin_inset Text \layout Standard \emph on implies \end_inset \begin_inset Text \layout Standard Shows consequence. The expression \begin_inset Formula $A\Rightarrow B$ \end_inset says that when \begin_inset Formula $A$ \end_inset holds, so does \begin_inset Formula $B$ \end_inset . In addition, \begin_inset Formula $A\Rightarrow B$ \end_inset is considered true except for the case \begin_inset Formula $A$ \end_inset true and \begin_inset Formula $B$ \end_inset false. To understand that, think of an \begin_inset Formula $A$ \end_inset which implies \begin_inset Formula $B$ \end_inset and ask yourself: \emph on is it possible that \begin_inset Formula $A$ \end_inset is true but not \begin_inset Formula $B$ \end_inset ? \emph default Anyway, don't worry about that, it's not important right now. \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\Longleftrightarrow$ \end_inset \end_inset \begin_inset Text \layout Standard \emph on if and only if \end_inset \begin_inset Text \layout Standard \begin_inset Formula $A\Longleftrightarrow B$ \end_inset is the same as \begin_inset Formula $(A\Rightarrow B)\wedge(B\Rightarrow A)$ \end_inset . It means that from \begin_inset Formula $A$ \end_inset we can deduce \begin_inset Formula $B$ \end_inset and viceversa, so they are equivalent. \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\square$ \end_inset \end_inset \begin_inset Text \layout Standard \emph on false \end_inset \begin_inset Text \layout Standard The empty square represents \emph on false \emph default (the binary \emph on 0 \emph default ). Technically, it represents \begin_inset Formula $\{\}$ \end_inset . \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\blacksquare$ \end_inset \end_inset \begin_inset Text \layout Standard \emph on true \end_inset \begin_inset Text \layout Standard The filled square represents \emph on true \emph default (the binary \emph on 1 \emph default ). Technically, it represents \begin_inset Formula $\{<>\}$ \end_inset . \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\exists$ \end_inset \end_inset \begin_inset Text \layout Standard \emph on exists... \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\exists xPx$ \end_inset can be read \emph on there exists an \begin_inset Formula $x$ \end_inset such that \begin_inset Formula $P$ \end_inset of \begin_inset Formula $x$ \end_inset \emph default . If in our domain, we can find an element (or more) which makes true the property \begin_inset Formula $P$ \end_inset applied to that element, then the formula is true. \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\forall$ \end_inset \end_inset \begin_inset Text \layout Standard \emph on for all... \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\forall xPx$ \end_inset can be read \emph on for all \begin_inset Formula $x$ \end_inset , \begin_inset Formula $P$ \end_inset of \begin_inset Formula $x$ \end_inset \emph default . If all elements we are working with make the property \begin_inset Formula $P$ \end_inset become true, then the formula is true. \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\vdash$ \end_inset \end_inset \begin_inset Text \layout Standard \emph on then \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\vdash$ \end_inset is the symbol of the \emph on sequent \emph default , which is the way of saying \begin_inset Quotes eld \end_inset \emph on when all this from the left happens, then it also happens all this from the right \emph default \begin_inset Quotes erd \end_inset . There exist valid sequents, like \begin_inset Formula $P\wedge Q\vdash P$ \end_inset or like \begin_inset Formula $P\Rightarrow Q,\ Q\Rightarrow R,\ P\vdash P\wedge R$ \end_inset . But there are also invalid ones, like \begin_inset Formula $P\Rightarrow Q,\ \neg P\vdash\neg Q$ \end_inset . The objective of natural deduction is to prove that a sequent is valid. \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\vDash$ \end_inset \end_inset \begin_inset Text \layout Standard \emph on valid \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\phi\vDash\varphi$ \end_inset means that \begin_inset Formula $\varphi$ \end_inset is logical consequence of \begin_inset Formula $\phi$ \end_inset , but when one writes \begin_inset Formula $A\vDash B$ \end_inset , what we mean is that the sequent \begin_inset Formula $A\vdash B$ \end_inset is valid, that is, we could somehow prove it, and now is considered true for any interpretation of the predicate symbols. \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\nvDash$ \end_inset \end_inset \begin_inset Text \layout Standard \emph on invalid \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\phi\nvDash\varphi$ \end_inset means that \begin_inset Formula $\varphi$ \end_inset is not logical consequence of \begin_inset Formula $\phi$ \end_inset . If you can find a series of values ( \emph on model \emph default ) which make \begin_inset Formula $\phi$ \end_inset true but \begin_inset Formula $\varphi$ \end_inset false, then invalidity is proven. \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\Vdash$ \end_inset \end_inset \begin_inset Text \layout Standard \emph on satisfiable \end_inset \begin_inset Text \layout Standard A set of formulas is satisfiable if there exists a series of values ( \emph on model \emph default ) which can make all of them true at the same time. \end_inset \begin_inset Text \layout Standard \begin_inset Formula $\nVdash$ \end_inset \end_inset \begin_inset Text \layout Standard \emph on unsatisfiable \end_inset \begin_inset Text \layout Standard A set of formulas is unsatisfiable if there isn't any combination of variables ( \emph on model \emph default ) which can make all of them become true at the same time. \end_inset \end_inset \layout Subsection Precedence of operators \layout Standard When you see an expression, you must be able to recognise what is it. For instance, \begin_inset Formula $A\vee B\Rightarrow C$ \end_inset is an implication (not a disjunction!), because \begin_inset Formula $\Rightarrow$ \end_inset is evaluated last (it has lower priority than \begin_inset Formula $\vee$ \end_inset ). \layout Standard Here there are the operators, inversely sorted by priority: \layout Itemize \begin_inset Formula $\Longleftrightarrow$ \end_inset \layout Itemize \begin_inset Formula $\Rightarrow$ \end_inset \layout Itemize \begin_inset Formula $\vee$ \end_inset and \begin_inset Formula $\wedge$ \end_inset (they have the same priority) \layout Itemize \begin_inset Formula $\neg$ \end_inset \layout Standard This means that \begin_inset Formula $\neg$ \end_inset is the one that most \begin_inset Quotes eld \end_inset \emph on sticks \emph default \begin_inset Quotes erd \end_inset to the symbol it has next. See this example about when and where are needed the parenthesis: \layout Standard \begin_inset Formula $P\vee\neg Q\Rightarrow R\wedge P\Longleftrightarrow\neg(R\vee S)\wedge A\Rightarrow B$ \end_inset is the same as \begin_inset Formula $(\ (P\vee(\neg Q))\ \Rightarrow\ (R\wedge P)\ )\Longleftrightarrow(\ ((\neg(R\vee S))\wedge A)\Rightarrow B\ )$ \end_inset \layout Standard But don't panic, I won't use again expressions that long. \layout Section Natural deduction \layout Standard Now I must explain what it is, how can it be done, and whether it has any practical use. \layout Subsection What it is for \layout Standard Natural deduction is used to try to prove that some reasoning is correct ( \begin_inset Quotes eld \end_inset \emph on to check the validity of a sequent \emph default \begin_inset Quotes erd \end_inset , says theory). Example: \layout Standard I tell you: \begin_inset Quotes eld \end_inset \emph on In summer it's warm, and now we're in summer, so now it's warm \emph default \begin_inset Quotes erd \end_inset . You start doing calculations, and finally reply: \begin_inset Quotes eld \end_inset \emph on OK, I can prove that the reasoning you just made is correct \emph default \begin_inset Quotes erd \end_inset . That is the use of natural deduction. \layout Standard But it's not always so easy: \begin_inset Quotes eld \end_inset \emph on if you fail a subject, you must repeat it. And if you don't study it, you fail it. Now suppose that you aren't repeating it. Then, or you study it, or you are failing it, or both of them \emph default \begin_inset Quotes erd \end_inset . This reasoning is valid and can be proven with natural deduction. \layout Standard Remark that you don't have to believe nor understand what you are told. For example, I say that: \begin_inset Quotes eld \end_inset \emph on Thyristors are tiny and funny; a pea is not tiny, so it isn't a thyristor \emph default \begin_inset Quotes erd \end_inset . Even if you don't know what am I talking about, or think that it is stupid (which it really is), you must be completely sure that the reasoning was correct. \layout Standard So, given a supposition \begin_inset Quotes eld \end_inset \emph on if all this happens, then all that also happens \emph default \begin_inset Quotes erd \end_inset , natural deduction allows us to say \begin_inset Quotes eld \end_inset \emph on yes, that's right \emph default \begin_inset Quotes erd \end_inset . In logical language: if you are given a sequent \begin_inset Formula $A\vdash B$ \end_inset , you can conclude at the end that it is \begin_inset Formula $\vDash$ \end_inset ( \emph on valid \emph default ). Then we write \begin_inset Formula $A\vDash B$ \end_inset ( \begin_inset Formula $A$ \end_inset has as consequence \begin_inset Formula $B$ \end_inset ). \layout Subsection What it is not for \layout Standard It isn't suitable for proving \emph on invalidity \emph default of some supposition. I might say \begin_inset Quotes eld \end_inset \emph on at daytime, it isn't night; and now it's daytime, so now it's also night \emph default \begin_inset Quotes erd \end_inset and you may pass some time trying the rules of natural deduction, but obtaining nothing useful. After some time, you will intuitively discover that the reasoning might not be valid, and it's then when another methods -not natural deduction- should be tried in order to prove invalidity. They are explained later. \layout Standard So, natural deduction only serves for proving validity, but not invalidity. What a pity, isn't it? \layout Standard Neither does it serve to provide a good answer to the question \begin_inset Quotes eld \end_inset \emph on What would happen if...? \emph default \begin_inset Quotes erd \end_inset . When we are to prove the validity of \begin_inset Formula $A\vdash B$ \end_inset , we must think of things that would happen if \begin_inset Formula $A$ \end_inset happened, and if we discover that one of these things is \begin_inset Formula $B$ \end_inset , then we have finished. But we will never be able to give a complete and finite list of all those things. \layout Subsection Functioning \layout Standard We are asked to prove the validity of \begin_inset Formula $\Gamma\vdash S$ \end_inset , where \begin_inset Formula $\Gamma$ \end_inset (that's \emph on gamma \emph default ) is a group of formulas separated by commas, and \begin_inset Formula $S$ \end_inset is a single formula. \layout Standard We start assuming that all formulas in \begin_inset Formula $\Gamma$ \end_inset are true, and, by continuous application of 9 concrete rules, we can go on discovering which other things are true. Our intention is to discover that \begin_inset Formula $S$ \end_inset is true; so once we achieve that, we can stop working. \layout Standard Sometimes we won't be able to extract truths from anywhere, and we will have to make suppositions: \begin_inset Quotes eld \end_inset \emph on well, I'm not sure that \begin_inset Formula $A\wedge B$ \end_inset is always true, but if it holds that \begin_inset Formula $C$ \end_inset , then it surely will be \emph default \begin_inset Quotes erd \end_inset . Then we have just discovered another truth: that \begin_inset Formula $C\Rightarrow A\wedge B$ \end_inset . \layout Standard As you can see, one has always to be thinking in where do we want to head to, because otherwise we could discover lots of things which are indeed true, but which we don't need at all. For instance, with \begin_inset Formula $A\vee B,\ \neg A\vdash B$ \end_inset we have to achieve the truth of \begin_inset Formula $B$ \end_inset . We may discover that \begin_inset Formula $\neg(A\wedge B)$ \end_inset , \begin_inset Formula $A\vee B\vee C$ \end_inset , \begin_inset Formula $(A\vee B)\Rightarrow\neg A$ \end_inset , and several other formulas, but what we really are interested in is \begin_inset Formula $B$ \end_inset and nothing else. So, if you aren't following the right way towards the solution, you can make a mess. \layout Subsection Notation \layout Standard There exist several ways to write the derivations done with natural deduction. I will use the Fitch style, because it's the one I used when learning, it's easy to understand, and occupies little space. It's something like this: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard P \backslash Rightarrow Q \backslash \backslash \layout Standard Q \backslash Rightarrow R \backslash \backslash \layout Standard \backslash fh P & H \backslash \backslash \layout Standard \backslash fa Q & E$ \backslash Rightarrow$ 1,3 \backslash \backslash \layout Standard \backslash fa R & E$ \backslash Rightarrow$ 2,4 \backslash \backslash \layout Standard \backslash fa Q \backslash wedge R & I$ \backslash wedge$ 4,5 \backslash \backslash \layout Standard P \backslash Rightarrow Q \backslash wedge R & I$ \backslash Rightarrow$ 3,6 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Standard This is sufficient to prove the validity of \begin_inset Formula $P\Rightarrow Q,\ Q\Rightarrow R\vdash P\Rightarrow Q\wedge R$ \end_inset . \layout Standard That figure is to be done line by line, from top to the bottom. The numbers from the left show the number of each line, and are always in natural order. \layout Standard The first lines contain each of the formulas which are written in the left part of the sequent. In this case, they are two: \begin_inset Formula $P\Rightarrow Q$ \end_inset and \begin_inset Formula $Q\Rightarrow R$ \end_inset . From these we will have to achieve the formula \begin_inset Formula $P\Rightarrow Q\wedge R$ \end_inset . \layout Standard On each line we write what new thing we have just discovered to be true, and to the right we note how did we discover that. Those symbols from the right side ( \begin_inset Formula $E$ \end_inset and \begin_inset Formula $I$ \end_inset ) are the abbreviations of the names of the 9 rules. For example, here we can see \emph on implication elimination \emph default ( \begin_inset Formula $E\Rightarrow$ \end_inset ), \emph on conjunction introduction \emph default ( \begin_inset Formula $I\wedge$ \end_inset ), and \emph on implication introduction \emph default ( \begin_inset Formula $I\Rightarrow$ \end_inset ). The numbers that go with them give us information about from where did we extract each necessary formula which is needed to apply the rule. They are line numbers, so, to be able to apply a rule, one has to use informati on only from the lines already written. \layout Standard Finally, that vertical line which goes from line 3 to 6 it's a hypothesis (that's why we put \begin_inset Formula $H$ \end_inset to the right). Everything which is inside it, is not always true, but only when happens \begin_inset Formula $P$ \end_inset (the heading of the hypothesis, at line 3). So, all of the work we do inside the hypothesis cannot be used outside it, because it can't be assured to be always true. \layout Standard The procedure finishes when we discover that it's true the formula at the right side of the sequent, in this case \begin_inset Formula $P\Rightarrow Q\wedge R$ \end_inset (it appears at the last line). \layout Section The derivation rules \layout Standard Here they are defined and explained the nine basic rules which are used in natural deduction. Their objective is to tell us when and how can we add new formulas which continue being true. \layout Standard Some examples (explained) are in the next section. \layout Subsection Iteration \layout Standard This is a very simple rule: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch*} \layout Standard n & A \backslash \backslash \layout Standard \backslash hline \layout Standard & A & IT n \layout Standard \backslash end{fitch*} \backslash ] \end_inset \layout Standard Well, I know, written like this is a bit strange, but I put it this way to make it useful as the definition of the rule. What is contained in the above formulation is that if on line number \begin_inset Formula $n$ \end_inset we have written \begin_inset Formula $A$ \end_inset (whatever expression it is) then we have the option to write again \begin_inset Formula $A$ \end_inset , but in the current line, and to justify that, we must write at the right \begin_inset Formula $IT\ n$ \end_inset . \layout Standard So, why would we want that? Well, for the moment, for nothing, but it will have its utility when we start working with hypothesis. Since a hypothesis is \emph on closed \emph default , all rules will have to work with formulas inside the hypothesis. If one of the formulas we want is just outside this hypothesis, we can copy it herein by using this rule called \emph on iteration \emph default . \layout Standard Some people think that it's not necessary to waste a line this way, but it's a lot clearer when this rule is used. What isn't allowed is using it only to \begin_inset Quotes eld \end_inset \emph on bring nearer \emph default \begin_inset Quotes erd \end_inset some formula which is several lines far away: it isn't necessary to rewrite a line if we have it already written in the current derivation. \layout Subsection Conjunction introduction \layout Standard The conjunction (that's the \emph on and \emph default ) can be created easily: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch*} \layout Standard m & A \backslash \backslash \layout Standard n & B \backslash \backslash \layout Standard \backslash hline \layout Standard & A \backslash wedge B & I$ \backslash wedge$ m,n \layout Standard \backslash end{fitch*} \backslash ] \end_inset \layout Standard You should be able to understand the meaning of figures like this one. When we put a long horizontal line, normally it's to separate the \emph on premises \emph default (top) from the \emph on conclusion \emph default (bottom). Premises are conditions which must be fulfilled in order to apply the rule, and conclusion (or \emph on resolvent \emph default ) is the result of the application of the rule. \layout Standard This rule says that if on one line we have written a truth, and on another line we have another one, also true, then we can write in just a line that both things are true. We must then note to the right the lines from where we picked the first and the second formulas. \layout Standard This is pretty logic, isn't it? if we know that really \emph on it's raining \emph default , and that it's true that \emph on now it's sunny \emph default , then there's no problem in saying that \emph on it's raining and sunny \emph default (yes, at the same time). If something feels strange, it's not our fault; blame the one who told us that \emph on it's raining \emph default or \emph on it's sunny \emph default . \layout Standard Remark that picking the lines reversed, you can obtain \begin_inset Formula $B\wedge A$ \end_inset , and picking the same line you can achieve \begin_inset Formula $A\wedge A$ \end_inset and \begin_inset Formula $B\wedge B$ \end_inset , which are also true. \layout Subsection Conjunction elimination \layout Standard This is just the inverse operation of the previous one. It has two parts; firstly: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch*} \layout Standard n & A \backslash wedge B \backslash \backslash \layout Standard \backslash hline \layout Standard & A & E$ \backslash wedge$ n \layout Standard \backslash end{fitch*} \backslash ] \end_inset \layout Standard And secondly, for the case you wanted \begin_inset Formula $B$ \end_inset : \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch*} \layout Standard n & A \backslash wedge B \backslash \backslash \layout Standard \backslash hline \layout Standard & B & E$ \backslash wedge$ n \layout Standard \backslash end{fitch*} \backslash ] \end_inset \layout Standard So, you can separate in several lines the \emph on conjunctands \emph default of a conjunction (yes, I think it's used that strange word). That's why this rule is called \emph on conjunction elimination \emph default , because from one line which has conjunction symbols ( \begin_inset Formula $\wedge$ \end_inset ) you can extract several which don't have it, supposedly trying to approach to the formula which we want proved. \layout Subsection Implication introduction \layout Standard This is more interesting, since it allows doing something useful with hypothesis (those subdemonstrations which have a vertical bar to the left). It's: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch*} \layout Standard m & \backslash fh A & H \backslash \backslash \layout Standard n & \backslash fa B \backslash \backslash \layout Standard \backslash hline \layout Standard & A \backslash Rightarrow B & I$ \backslash Rightarrow$ m,n \layout Standard \backslash end{fitch*} \backslash ] \end_inset \layout Standard And what it does mean is that if we supposed something (call it \begin_inset Formula $A$ \end_inset ), and we just discovered (by using the rules) that supposing \begin_inset Formula $A$ \end_inset made true \begin_inset Formula $B$ \end_inset (whatever it is), then we have something clear: we can't assure that \begin_inset Formula $B$ \end_inset always is true, but we can assure that \begin_inset Formula $A$ \end_inset implies \begin_inset Formula $B$ \end_inset , which is written \begin_inset Formula $A\Rightarrow B$ \end_inset . \layout Standard This allows us to end the subdemonstration and continue working with what we were doing before. Remember that you can't finish natural deduction inside a subdemonstration. \layout Subsection Implication elimination \layout Standard This one is simpler than the previous, since it does not deal with suppositions but with facts: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch*} \layout Standard m & A \backslash Rightarrow B \backslash \backslash \layout Standard n & A \backslash \backslash \layout Standard \backslash hline \layout Standard & B & E$ \backslash Rightarrow$ m,n \layout Standard \backslash end{fitch*} \backslash ] \end_inset \layout Standard Simply, if we are told that when \begin_inset Formula $A$ \end_inset also happens \begin_inset Formula $B$ \end_inset (that's what it means \begin_inset Formula $A\Rightarrow B$ \end_inset ), and they also tell us that now happens \begin_inset Formula $A$ \end_inset , then we can assure that \begin_inset Formula $B$ \end_inset . \layout Standard This rule is also named \emph on modus ponens \emph default . \layout Subsection Disjunction introduction \layout Standard The disjunction (that's the \emph on or \emph default ) is very easy but not obvious: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch*} \layout Standard n & A \backslash \backslash \layout Standard \backslash hline \layout Standard & A \backslash vee B & I$ \backslash vee$ n \layout Standard \backslash end{fitch*} \backslash ] \end_inset \layout Standard Well, to be exact, I will say that it's also available in the other order: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch*} \layout Standard n & A \backslash \backslash \layout Standard \backslash hline \layout Standard & B \backslash vee A & I$ \backslash vee$ n \layout Standard \backslash end{fitch*} \backslash ] \end_inset \layout Standard That's wonderful, isn't it? If we know that \begin_inset Quotes eld \end_inset \emph on it's Thursday \emph default \begin_inset Quotes erd \end_inset we also know that \begin_inset Quotes eld \end_inset \emph on it's Thursday or cows can fly \emph default \begin_inset Quotes erd \end_inset , \begin_inset Quotes eld \end_inset \emph on it's Thursday or Friday \emph default \begin_inset Quotes erd \end_inset , or even \begin_inset Quotes eld \end_inset \emph on it's Thursday... or not \emph default \begin_inset Quotes erd \end_inset . All of them are true. \layout Standard But remember that, when talking, we tend to use \emph on exclusive or \emph default ( \emph on XOR \emph default ), which is true if one of the \emph on disjunctands \emph default is true but not when both of them are true at the same time. To a logician, the common phrase \begin_inset Quotes eld \end_inset \emph on it's Thursday or Friday \emph default \begin_inset Quotes erd \end_inset holds true under three situations: when \emph on it's Thursday \emph default , when \emph on it's Friday \emph default , and when \emph on it's Thursday and Friday at the same time \emph default (something difficult in the real world, but mathematicians are capable of doing all types of suppositions...). \layout Subsection Disjunction elimination \layout Standard This is the most complicated rule, mainly because if we are given a phrase with \emph on or \emph default , like \begin_inset Quotes eld \end_inset \emph on it's Thursday or Friday \emph default \begin_inset Quotes erd \end_inset , what can we deduce from it? That \emph on it's Thursday \emph default ? No, it may be Friday. That \emph on it's Friday \emph default ? No, it may be Thursday. That \emph on it's Thursday or Friday \emph default ? Well, yes, but we already knew that... \layout Standard The rule (now I explain it): \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch*} \layout Standard m & A \backslash vee B \backslash \backslash \layout Standard & \backslash fh A & H \backslash \backslash \layout Standard n & \backslash fa C \backslash \backslash \layout Standard & \backslash fh B & H \backslash \backslash \layout Standard p & \backslash fa C \backslash \backslash \layout Standard \backslash hline \layout Standard & C & E$ \backslash vee$ m,n,p \layout Standard \backslash end{fitch*} \backslash ] \end_inset \layout Standard We need more information besides the \begin_inset Formula $A\vee B$ \end_inset . If, luckily, we happen to know \begin_inset Formula $A\Rightarrow C$ \end_inset , and also \begin_inset Formula $B\Rightarrow C$ \end_inset , then we do know what happens when \begin_inset Formula $A\vee B$ \end_inset : both one option and the other drive us to \begin_inset Formula $C$ \end_inset , so \begin_inset Formula $C$ \end_inset is true. \layout Standard This type of things only happen when the exercise is prepared so that the \emph on disjunction elimination \emph default appears, or when \begin_inset Formula $A$ \end_inset and \begin_inset Formula $B$ \end_inset are similar (then we will find some \begin_inset Formula $C$ \end_inset which is implied by both). \layout Standard Now an example: when I contracted my ADSL access to the Internet, it was with \emph on Telefónica \emph default or \emph on Terra \emph default , but I'm not sure of with which one (even they didn't know it). And in my country (Spain), any option was slow, awfully expensive, and loaded with problems. Typical Spanish. If we call all those \emph on features \emph default \begin_inset Formula $M$ \end_inset (for mockery, misery, ...), then basically any Internet Service Provider was an \begin_inset Formula $M$ \end_inset . Concretely, \begin_inset Formula $Telefonica\Rightarrow M$ \end_inset and \begin_inset Formula $Terra\Rightarrow M$ \end_inset , so undoubtedly my ADSL had to be \begin_inset Formula $M$ \end_inset , both if I had one or the other ISP. And indeed, I needed 9 months to fully subscribe to the service... Luckily all this happened now several years ago. \layout Standard This derivation rule is also called \emph on proof by cases \emph default , since we have to check each possible case to see that they all involve the same conclusion. \layout Subsection Negation introduction \layout Standard This one is nice and interesting: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch*} \layout Standard m & \backslash fh A & H \backslash \backslash \layout Standard n & \backslash fa B \backslash \backslash \layout Standard p & \backslash fa \backslash neg B \backslash \backslash \layout Standard \backslash hline \layout Standard & \backslash neg A & I$ \backslash neg$ m,n,p \layout Standard \backslash end{fitch*} \backslash ] \end_inset \layout Standard If after supposing \begin_inset Formula $A$ \end_inset , you achieved the conclusion that both \begin_inset Formula $B$ \end_inset and \begin_inset Formula $\neg B$ \end_inset are true, you're not lost, since you just discovered another truth: that it's not possible for \begin_inset Formula $A$ \end_inset to be true, that's it, \begin_inset Formula $\neg A$ \end_inset it's true. \layout Standard For instance, I confess that \emph on if I use Windows, I don't profit the time I am with my computer \emph default . Since some years, \emph on I do profit it \emph default , so the conclusion is that \emph on I don't use Windows \emph default . To achieve that conclusion, the path that you would follow (maybe without thinking) is precisely the one that this rule needs: suppose that \emph on I do use Windows \emph default , in that case \emph on I wouldn't profit my computer \emph default . But I said that \emph on I do profit it \emph default , so that supposition must be wrong. \layout Standard This procedure is called \emph on reduction to the absurd \emph default ( \emph on reductio ad absurdum \emph default ): suppose something to achieve a contradiction and be able to assert that what we supposed is false. It's specially useful if you start supposing \emph on the contrary \emph default of what you want to prove: if any contradiction can be discovered, then it's almost all done. \layout Standard I should note that this is an \emph on abuse of notation \emph default : following all the laws of logic, it happens that each subdemonstration needs \emph on one \emph default conclusion (not two); and at the above hypothesis, it's not clear which one is the conclusion ( \begin_inset Formula $B$ \end_inset or \begin_inset Formula $\neg B$ \end_inset ?). The correct way to write it would be using \emph on conjunction introduction \emph default to say that \begin_inset Formula $B\wedge\neg B$ \end_inset , and this one is the conclusion which shows the wrongness of the initial hypothesis. But my teachers didn't write that line. \layout Subsection Negation elimination \layout Standard This one is too simple, but we also have to know it: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch*} \layout Standard n & \backslash neg \backslash neg A \backslash \backslash \layout Standard \backslash hline \layout Standard & A & E$ \backslash neg$ n \layout Standard \backslash end{fitch*} \backslash ] \end_inset \layout Standard So, when we see the negation of the negation of something, we can take off these two following negations. \layout Standard Remember that the negation of \begin_inset Quotes eld \end_inset \emph on this is white \emph default \begin_inset Quotes erd \end_inset is not \begin_inset Quotes eld \end_inset \emph on this is black \emph default \begin_inset Quotes erd \end_inset but \begin_inset Quotes eld \end_inset \emph on this is not white \emph default \begin_inset Quotes erd \end_inset . \layout Subsection No more rules \layout Standard That's it, there are no more basic rules. Well, there still exist some more to deal with \emph on quantifiers \emph default and two about \emph on true \emph default and \emph on false \emph default , which I will explain later, but with the former 9 we're able to try to prove the validity of any sequent in this document (except the ones with quantifiers...). \layout Standard Remember again that there are no more rules: you can't change from \begin_inset Formula $A\vee\neg A$ \end_inset to \begin_inset Formula $\blacksquare$ \end_inset ( \emph on true \emph default ) directly, or from \begin_inset Formula $\neg(A\vee B)$ \end_inset to \begin_inset Formula $\neg A\wedge\neg B$ \end_inset , nor use the distributive, associative or commutative property. You have to proceed always step by step; even the simple changes aren't allowed (currently). Why? Because probably they aren't that simple: you will understand it when having to prove things like that \begin_inset Formula $A\vee\neg A$ \end_inset is always true... (it's in the next section). \layout Section Explained exercises \layout Standard Exercises from several levels, explained step by step. If you still want more examples (but without comments) look into the last section. What I'm trying to explain here is not the rules, but the way of thinking so that you can devise the magic idea which solves the problem. \layout Standard This is what I more lacked when I had to study natural deduction. \layout Subsection A very simple one. \begin_inset Formula $P,\ P\Rightarrow Q\vdash P\wedge Q$ \end_inset \layout Standard The solution to \begin_inset Formula $P,\ P\Rightarrow Q\vdash P\wedge Q$ \end_inset is: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard P \backslash \backslash \layout Standard P \backslash Rightarrow Q \backslash \backslash \layout Standard Q & E$ \backslash Rightarrow$ 2,1 \backslash \backslash \layout Standard P \backslash wedge Q & I$ \backslash wedge$ 1,3 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Standard Here we won't have to think much, we just have to use correctly the rules and their justifications. \layout Standard Firstly, understand what has been told to us: they say that now happen \emph on two \emph default things, the first is that \begin_inset Formula $P$ \end_inset and the second is that \begin_inset Formula $P\Rightarrow Q$ \end_inset (they are the two formulas written to the left of the \begin_inset Formula $\vdash$ \end_inset ). These two things we will note, one on each line, since at this demonstration they will always be true (liking it or not). \layout Standard The goal of this demonstration is to know that \begin_inset Formula $P\wedge Q$ \end_inset is also true, as we have been told that when \begin_inset Formula $P$ \end_inset and \begin_inset Formula $P\Rightarrow Q$ \end_inset are true, then \begin_inset Formula $P\wedge Q$ \end_inset also is, and we want to check if that's right. Finally we achieved it, since on the last line we see the \begin_inset Formula $P\wedge Q$ \end_inset written. \layout Standard But how do we start? Remember where do we want to head to. If \begin_inset Formula $P\wedge Q$ \end_inset has to be true, then both \begin_inset Formula $P$ \end_inset and \begin_inset Formula $Q$ \end_inset should be true; let's attempt to prove that they really are. \layout Standard \begin_inset Formula $P$ \end_inset is true, since they said so, and we have it written on line 1. \layout Standard But we weren't told that \begin_inset Formula $Q$ \end_inset was true. What do we know about \begin_inset Formula $Q$ \end_inset ? Searching it on lines 1 and 2, the only we know about \begin_inset Formula $Q$ \end_inset is that it's true when happens \begin_inset Formula $P$ \end_inset (that's what says line 2). But \begin_inset Formula $P$ \end_inset is true, so we can use one of the rules to deduce \begin_inset Formula $Q$ \end_inset from the \begin_inset Formula $P\Rightarrow Q$ \end_inset and \begin_inset Formula $P$ \end_inset . Remark what is the most important change when we go from \begin_inset Formula $P\Rightarrow Q$ \end_inset to \begin_inset Formula $Q$ \end_inset : we stopped using the implication symbol; so the rule we will need is the one called \emph on implication elimination \emph default . \layout Standard To use this rule, we look at its definition, and see that we have to write in a new line \begin_inset Formula $Q$ \end_inset , and as a justification \begin_inset Formula $E\Rightarrow\ 2,1$ \end_inset needs to be written. The \begin_inset Formula $E$ \end_inset is from \emph on elimination \emph default , the \begin_inset Formula $\Rightarrow$ \end_inset means \emph on implication \emph default , the first number is the one from the line which does contain the implication ( \begin_inset Formula $P\Rightarrow Q$ \end_inset ), and the second number is from the line which has the known truth ( \begin_inset Formula $P$ \end_inset ). It's incorrect to write them reversed ( \begin_inset Formula $E\Rightarrow\ 1,2$ \end_inset ), since the definition of the rule says that the line which has the implication should be cited first. \layout Standard We have just applied the rule, and now we know three truths: \begin_inset Formula $P$ \end_inset , \begin_inset Formula $P\Rightarrow Q$ \end_inset , and \begin_inset Formula $Q$ \end_inset . They are all equally true. Now we're nearer to our objective, \begin_inset Formula $P\wedge Q$ \end_inset , since we know that \begin_inset Formula $P$ \end_inset and \begin_inset Formula $Q$ \end_inset are true, so \begin_inset Formula $P\wedge Q$ \end_inset also has to be true (it's obvious). In the formula we search there's a conjunction sign ( \begin_inset Formula $\wedge$ \end_inset ) which we don't have, so we need to use the \emph on conjunction introduction \emph default to be able to say that \begin_inset Formula $P\wedge Q$ \end_inset is true because \begin_inset Formula $P$ \end_inset is and also \begin_inset Formula $Q$ \end_inset . As a justification we write \begin_inset Formula $I\wedge\ 1,3$ \end_inset (the line where it says \begin_inset Formula $P$ \end_inset , and the one which says \begin_inset Formula $Q$ \end_inset ). Don't put \begin_inset Formula $I\wedge\ 3,1$ \end_inset , that would be to affirm that \begin_inset Formula $Q\wedge P$ \end_inset , which is not what we're trying to prove. \layout Standard Then we know 4 truths: \begin_inset Formula $P$ \end_inset , \begin_inset Formula $P\Rightarrow Q$ \end_inset , \begin_inset Formula $Q$ \end_inset , and \begin_inset Formula $P\wedge Q$ \end_inset . We could continue finding more things which are true, but we've already finished, since we had been told to prove that \begin_inset Formula $P\wedge Q$ \end_inset is true, and we just achieved that (in line 4). So that will be the last line, and we don't have to write anything else. \layout Standard Ah, and an example of this derivation, but with words: \begin_inset Quotes eld \end_inset \emph on now it's summer, and in summer it's warm. That's why now it's summer and it's warm \emph default \begin_inset Quotes erd \end_inset . \layout Subsection A bit more complicated. \begin_inset Formula $P\wedge Q\Rightarrow R,\ Q\Rightarrow P,\ Q\vdash R$ \end_inset \layout Standard Try yourself \begin_inset Formula $P\wedge Q\Rightarrow R,\ Q\Rightarrow P,\ Q\vdash R$ \end_inset . Then look the solution: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard P \backslash wedge Q \backslash Rightarrow R \backslash \backslash \layout Standard Q \backslash Rightarrow P \backslash \backslash \layout Standard Q \backslash \backslash \layout Standard P & E$ \backslash Rightarrow$ 2,3 \backslash \backslash \layout Standard P \backslash wedge Q & I$ \backslash wedge$ 4,3 \backslash \backslash \layout Standard R & E$ \backslash Rightarrow$ 1,5 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Standard The only way to achieve \begin_inset Formula $R$ \end_inset is using the first formula, \begin_inset Formula $P\wedge Q\Rightarrow R$ \end_inset , but we can only use it when \begin_inset Formula $P\wedge Q$ \end_inset is true, so we're going for that. \layout Standard We know that \begin_inset Formula $Q\Rightarrow P$ \end_inset (line 2) and also \begin_inset Formula $Q$ \end_inset (line 3), so we deduce \begin_inset Formula $P$ \end_inset . Since \begin_inset Formula $P$ \end_inset is now true and also \begin_inset Formula $Q$ \end_inset , \begin_inset Formula $P\wedge Q$ \end_inset is too. Until now it's similar to the previous exercise. \layout Standard Finally, we have \begin_inset Formula $P\wedge Q\Rightarrow R$ \end_inset , and know that \begin_inset Formula $P\wedge Q$ \end_inset , so we finish by saying \begin_inset Formula $R$ \end_inset . \layout Subsection Starting to make suppositions. \begin_inset Formula $P\Rightarrow Q,\ Q\Rightarrow R\vdash P\Rightarrow Q\wedge R$ \end_inset \layout Standard This one, \begin_inset Formula $P\Rightarrow Q,\ Q\Rightarrow R\vdash P\Rightarrow Q\wedge R$ \end_inset , is more interesting: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard P \backslash Rightarrow Q \backslash \backslash \layout Standard Q \backslash Rightarrow R \backslash \backslash \layout Standard \backslash fh P & H \backslash \backslash \layout Standard \backslash fa Q & E$ \backslash Rightarrow$ 1,3 \backslash \backslash \layout Standard \backslash fa R & E$ \backslash Rightarrow$ 2,4 \backslash \backslash \layout Standard \backslash fa Q \backslash wedge R & I$ \backslash wedge$ 4,5 \backslash \backslash \layout Standard P \backslash Rightarrow Q \backslash wedge R & I$ \backslash Rightarrow$ 3,6 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Standard Note the following details: \layout Itemize We aren't told any information about what does happen now (we don't have formulas like \begin_inset Formula $P$ \end_inset , or \begin_inset Formula $Q\wedge R$ \end_inset , etc.). They only say things like that \emph on if happened \begin_inset Formula $P$ \end_inset , then \begin_inset Formula $Q$ \end_inset \emph default \emph on would also happen \emph default . \layout Itemize In the same way, what we must prove is not that \emph on just now happens something \emph default , but that \emph on if it happened \begin_inset Formula $P$ \end_inset , then \begin_inset Formula $Q$ \end_inset and \begin_inset Formula $R$ \end_inset would be true. \layout Itemize \begin_inset Formula $P\Rightarrow Q\wedge R$ \end_inset is an implication ( \emph on something implies something \emph default ), because operator \begin_inset Formula $\Rightarrow$ \end_inset has less priority than \begin_inset Formula $\wedge$ \end_inset . It's a big error to understand that formula as \begin_inset Formula $(P\Rightarrow Q)\wedge R$ \end_inset . \layout Standard As the formula we want is an implication ( \begin_inset Formula $P\Rightarrow Q\wedge R$ \end_inset ), we will have to use the \emph on implication introduction \emph default , but this rule needs having a subdemonstration (look it up at its definition). \layout Standard It isn't hard to understand why: \begin_inset Formula $P\Rightarrow Q\wedge R$ \end_inset says that \emph on if it happens \begin_inset Formula $P$ \end_inset , then happens \begin_inset Formula $Q\wedge R$ \end_inset \emph default , so the first we should do is to suppose that \begin_inset Formula $P$ \end_inset really does happen. Then we will have to discover that, in this case when \begin_inset Formula $P$ \end_inset is true, it is also true \begin_inset Formula $Q\wedge R$ \end_inset . When we get that, we will apply the rule and write everything politely: \begin_inset Formula $P\Rightarrow Q\wedge R$ \end_inset . \layout Standard For that reason, at line 3 we make an hypothesis (justified by the \begin_inset Formula $H$ \end_inset at the right): suppose that \begin_inset Formula $P$ \end_inset is true. Now we're starting a subdemonstration, where we will be able to use the truths that were on the father demonstration (lines 1 and 2 in this case), and also we can use \begin_inset Formula $P$ \end_inset as if it were another truth. \layout Standard We made this hypothesis aiming to know that \begin_inset Formula $Q\wedge R$ \end_inset , so we deduce it similarly to the previous exercises. Notice that we use truths from inside and from outside the subdemonstration, and also that, while we haven't finished it, that vertical line to the left must be put. \layout Standard In line 6 we now have \begin_inset Formula $Q\wedge R$ \end_inset , which is what we were looking for. Using the \emph on implication introduction \emph default rule, we can go outside this subdemonstration by saying that \emph on if the hypothesis is true, then what we deduced from it also is true \emph default . We stop putting that vertical line, since \begin_inset Formula $P\Rightarrow Q\wedge R$ \end_inset is always true (it doesn't depend on whether \begin_inset Formula $P$ \end_inset is true or not). The justification we used, \begin_inset Formula $I\Rightarrow\ 3,6$ \end_inset , says that 3 is the line where we made the supposition, and 6 the line where we discovered something interesting which happens when we make that supposition. \layout Standard \begin_inset Formula $P\Rightarrow Q\wedge R$ \end_inset is what we wanted, so we have finished. We finish as always, since we're outside any subdemonstration. \layout Subsection Using iteration. \begin_inset Formula $P\vdash Q\Rightarrow P$ \end_inset \layout Standard This is a short one: \begin_inset Formula $P\vdash Q\Rightarrow P$ \end_inset . Solution: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard P \backslash \backslash \layout Standard \backslash fh Q & H \backslash \backslash \layout Standard \backslash fa P & IT 1 \backslash \backslash \layout Standard Q \backslash Rightarrow P & I$ \backslash Rightarrow$ 2,3 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Standard The way is clear: we have to suppose \begin_inset Formula $Q$ \end_inset , and finally see that, in that case, \begin_inset Formula $P$ \end_inset is true. The trick: \begin_inset Formula $P$ \end_inset is always true, whether we suppose \begin_inset Formula $Q$ \end_inset or not. \layout Standard We must use \emph on implication introduction \emph default , but this needs a hypothesis, and, some lines below, the result of the supposition. Only then we can close the hypothesis. \layout Standard So after opening it (line 2), we must do something to write down that \begin_inset Formula $P$ \end_inset . Since we already have it written in line 1, we simply put \begin_inset Formula $P$ \end_inset again and justify it with \begin_inset Formula $IT\ 1$ \end_inset , which means \begin_inset Quotes eld \end_inset \emph on I copied this from line 1 \emph default \begin_inset Quotes erd \end_inset . The \begin_inset Formula $IT$ \end_inset is for \emph on iteration \emph default . \layout Standard We now fulfill the requirements to apply the rule, so we apply it, closing the subdemonstration, and we've ended. \layout Subsection Reduction to the absurd. \begin_inset Formula $P\Rightarrow Q,\ \neg Q\vdash\neg P$ \end_inset \layout Standard This is a very useful technique. Validity of \begin_inset Formula $P\Rightarrow Q,\ \neg Q\vdash\neg P$ \end_inset is proved with: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard P \backslash Rightarrow Q \backslash \backslash \layout Standard \backslash neg Q \backslash \backslash \layout Standard \backslash fh P & H \backslash \backslash \layout Standard \backslash fa Q & E$ \backslash Rightarrow$ 1,3 \backslash \backslash \layout Standard \backslash fa \backslash neg Q & IT 2 \backslash \backslash \layout Standard \backslash neg P & I$ \backslash neg$ 3,4,5 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Standard What has to be achieved here is \begin_inset Formula $\neg P$ \end_inset , which is the \emph on negation of something \emph default , so the rule which will help is the \emph on negation introduction \emph default , also known as \emph on reduction to the absurd \emph default . \layout Standard The way to act will be to suppose the contrary of \begin_inset Formula $\neg P$ \end_inset (which is \begin_inset Formula $P$ \end_inset ) and find a contradiction (any). Supposing \begin_inset Formula $P$ \end_inset will lead us to \begin_inset Formula $Q$ \end_inset (by \emph on implication elimination \emph default ), and, as we also have \begin_inset Formula $\neg Q$ \end_inset , we can apply the rule. This \begin_inset Formula $\neg Q$ \end_inset should be inserted in the current subdemonstration with the \emph on iteration \emph default rule, so that it is together with the \begin_inset Formula $Q$ \end_inset and \emph on inside \emph default the subdemonstration. Everything which is inside the subdemonstration is consequence of \begin_inset Formula $P$ \end_inset , so it is important to see that both \begin_inset Formula $Q$ \end_inset and \begin_inset Formula $\neg Q$ \end_inset also are. \layout Standard For the \emph on negation introduction \emph default , the way to justify this rule is putting the line number of where does the (wrong) supposition start, and the numbers of the two lines where we saw the contradiction. The conclusion of this rule is the contrary of what we just supposed, in this case \begin_inset Formula $\neg P$ \end_inset , so we can finish the derivation here. \layout Standard This reasoning is actually made without much thinking. In words it would be something like: \begin_inset Quotes eld \end_inset \emph on of course that \begin_inset Formula $\neg P$ \end_inset , since if it were \begin_inset Formula $P$ \end_inset then \begin_inset Formula $Q$ \end_inset , and you say that \begin_inset Formula $\neg Q$ \end_inset , so it can't be that \begin_inset Formula $P$ \end_inset \emph default \begin_inset Quotes erd \end_inset . \layout Subsection With subdemonstrations. \begin_inset Formula $P\Rightarrow(Q\Rightarrow R)\vdash Q\Rightarrow(P\Rightarrow R)$ \end_inset \layout Standard Things get harder. Here's the solution to \begin_inset Formula $P\Rightarrow(Q\Rightarrow R)\vdash Q\Rightarrow(P\Rightarrow R)$ \end_inset : \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard P \backslash Rightarrow (Q \backslash Rightarrow R) \backslash \backslash \layout Standard \backslash fh Q & H \backslash \backslash \layout Standard \backslash fa \backslash fh P & H \backslash \backslash \layout Standard \backslash fa \backslash fa Q \backslash Rightarrow R & E$ \backslash Rightarrow$ 1,3 \backslash \backslash \layout Standard \backslash fa \backslash fa R & E$ \backslash Rightarrow$ 4,2 \backslash \backslash \layout Standard \backslash fa P \backslash Rightarrow R & I$ \backslash Rightarrow$ 3,5 \backslash \backslash \layout Standard Q \backslash Rightarrow (P \backslash Rightarrow R) & I$ \backslash Rightarrow$ 2,6 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Standard But first: here we will only use the two rules that help adding and removing implications, since it's the only operator appearing in the formulas. \layout Standard We want \begin_inset Formula $Q\Rightarrow(P\Rightarrow R)$ \end_inset , so we will have to do a hypothesis \begin_inset Formula $Q$ \end_inset inside of which we should prove that \begin_inset Formula $P\Rightarrow R$ \end_inset . We now do that to simplify the problem: we open a subdemonstration at line 2. We won't close it until we discover that \begin_inset Formula $P\Rightarrow R$ \end_inset is true. \layout Standard Now the problem is somehow easier. We just need to prove \begin_inset Formula $P\Rightarrow R$ \end_inset , and we have two lines with two truths: the first says that \begin_inset Formula $P\Rightarrow(Q\Rightarrow R)$ \end_inset , and the second says that \begin_inset Formula $Q$ \end_inset . \layout Standard How can we achieve the \begin_inset Formula $P\Rightarrow R$ \end_inset ? Well, as always: we must suppose \begin_inset Formula $P$ \end_inset , and achieve that \begin_inset Formula $R$ \end_inset is true, in some way. Even if it doesn't seem very simple, it's what must be done, since \emph on implication introduction \emph default works that way. So we're going to open another hypothesis, now supposing \begin_inset Formula $P$ \end_inset , and let's see if we achieve \begin_inset Formula $R$ \end_inset . This will be a hypothesis inside a hypothesis, but there's no problem in doing that. \layout Standard After writing line 3, and being inside a \emph on subsubdemonstration \emph default , we have available that \begin_inset Formula $P\Rightarrow(Q\Rightarrow R)$ \end_inset , that \begin_inset Formula $Q$ \end_inset , and that \begin_inset Formula $P$ \end_inset . We must prove \begin_inset Formula $R$ \end_inset . Now it isn't that hard, is it? If we know that \begin_inset Formula $P$ \end_inset , we can use \emph on implication elimination \emph default on line 1, and we will get the true formula \begin_inset Formula $Q\Rightarrow R$ \end_inset . Since \begin_inset Formula $Q$ \end_inset is also true (line 2), we can apply that rule again to discover that \begin_inset Formula $R$ \end_inset . \layout Standard We then see that supposing \begin_inset Formula $P$ \end_inset leads us to the conclusion \begin_inset Formula $R$ \end_inset , so we can write down \begin_inset Formula $P\Rightarrow R$ \end_inset , which is what we wanted. Now we've gone outside the subsubdemonstration, and we're only under the supposition that \begin_inset Formula $Q$ \end_inset is true. As we now see that this supposition implies the truth of the formula \begin_inset Formula $P\Rightarrow R$ \end_inset , we can end this subdemonstration concluding that \begin_inset Formula $Q\Rightarrow(P\Rightarrow R)$ \end_inset . \layout Standard \begin_inset Formula $Q\Rightarrow(P\Rightarrow R)$ \end_inset is precisely what had to be proven, so we're finished. \layout Subsection One with proof by cases. \begin_inset Formula $P\vee(Q\wedge R)\vdash P\vee Q$ \end_inset \layout Standard It will be needed the most complex derivation rule: the \emph on disjunction elimination \emph default . \begin_inset Formula $P\vee(Q\wedge R)\vdash P\vee Q$ \end_inset solved: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard P \backslash vee (Q \backslash wedge R) \backslash \backslash \layout Standard \backslash fh P & H \backslash \backslash \layout Standard \backslash fa P \backslash vee Q & I$ \backslash vee$ 2 \backslash \backslash \layout Standard \backslash fh Q \backslash wedge R & H \backslash \backslash \layout Standard \backslash fa Q & E$ \backslash wedge$ 4 \backslash \backslash \layout Standard \backslash fa P \backslash vee Q & I$ \backslash vee$ 5 \backslash \backslash \layout Standard P \backslash vee Q & E$ \backslash vee$ 1,3,6 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Standard You already know the rules, so I just explain the way of thinking of a human who doesn't know natural deduction but can think a little: \layout Standard We need to know that \begin_inset Formula $P\vee Q$ \end_inset is always true. The expression from the left, \begin_inset Formula $P\vee(Q\wedge R)$ \end_inset , can be made true because of two causes: \layout Itemize if it's true because \begin_inset Formula $P$ \end_inset is true, then \begin_inset Formula $P\vee Q$ \end_inset is true. \layout Itemize if it's true because \begin_inset Formula $Q\wedge R$ \end_inset is true, then both \begin_inset Formula $Q$ \end_inset and \begin_inset Formula $R$ \end_inset are true, so \begin_inset Formula $P\vee Q$ \end_inset is true because of \begin_inset Formula $Q$ \end_inset . \layout Standard So, anyway, \begin_inset Formula $P\vee Q$ \end_inset is true. \layout Standard Well, now we just need to translate all this to logical language, following the same order in which we thought that, and proceeding slowly. \layout Standard We start proving one path, then the other, and finally we apply the \emph on disjunction elimination \emph default . To justify it we must write the line where the disjunction is in, and the two lines from inside each subdemonstration where we saw that both supposing one thing or supposing the other leads to the same result. \layout Standard Notice that, even if we discovered that \begin_inset Formula $P\Rightarrow P\vee Q$ \end_inset and that \begin_inset Formula $Q\wedge R\Rightarrow P\vee Q$ \end_inset , it isn't necessary to use \emph on implication introduction \emph default to keep this written down. \layout Standard The hardest thing in \emph on proof by cases \emph default is to decide which will be the expression to prove in both cases. It must be exactly the same in both cases! \layout Subsection One to think. \begin_inset Formula $L\wedge M\Rightarrow\neg P,\ I\Rightarrow P,\ M,\ I\vdash\neg L$ \end_inset \layout Standard Try \begin_inset Formula $L\wedge M\Rightarrow\neg P,\ I\Rightarrow P,\ M,\ I\vdash\neg L$ \end_inset only thinking; then write it down on paper. It's something like: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard L \backslash wedge M \backslash Rightarrow \backslash neg P \backslash \backslash \layout Standard I \backslash Rightarrow P \backslash \backslash \layout Standard M \backslash \backslash \layout Standard I \backslash \backslash \layout Standard \backslash fh L & H \backslash \backslash \layout Standard \backslash fa L \backslash wedge M & I$ \backslash wedge$ 5,3 \backslash \backslash \layout Standard \backslash fa \backslash neg P & E$ \backslash Rightarrow$ 1,6 \backslash \backslash \layout Standard \backslash fa P & E$ \backslash Rightarrow$ 2,4 \backslash \backslash \layout Standard \backslash neg L & I$ \backslash neg$ 5,7,8 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Standard I will put it by words: \begin_inset Quotes eld \end_inset \emph on if you use Linux and Mozilla as a browser, you avoid problems. In contrast, if you use Internet Explorer you will have problems. Now you use Mozilla, but also Internet Explorer sometimes. Consequently, I know that you don't use Linux \emph default \begin_inset Quotes erd \end_inset . \layout Standard Maybe that seems evident: \begin_inset Quotes eld \end_inset \emph on of course, since IE is not on Linux \emph default \begin_inset Quotes erd \end_inset , but notice that I never said that. There isn't the \begin_inset Formula $I\Rightarrow\neg L$ \end_inset anywhere. \layout Standard The way in which you should think when you prepare this exercise is: \layout Enumerate I need to prove \begin_inset Formula $\neg L$ \end_inset , which is the negation of something. It can't be seen any rule of the form \emph on something implies \begin_inset Formula $\neg L$ \end_inset \emph default which allows me to obtain it directly. We should think of another way, for example \emph on negation introduction \emph default ( \emph on reduction to the absurd \emph default ): suppose that I do use Linux. \layout Enumerate In the case when I use Linux, I would use both Linux and Mozilla, since I already used Mozilla before (it's the third truth which is written in the original problem). \layout Enumerate Using both Linux and Mozilla, I wouldn't have computer problems, since \begin_inset Formula $L\wedge M\Rightarrow\neg P$ \end_inset . \layout Enumerate But I also used Internet Explorer (fourth truth), and since IE generates problems, I will have problems. \begin_inset Formula $P$ \end_inset . \layout Enumerate I got a contradiction: \begin_inset Formula $\neg P$ \end_inset and \begin_inset Formula $P$ \end_inset . So, what's happening is that the supposition I did of using Linux is wrong: actually, \begin_inset Formula $\neg L$ \end_inset . \layout Standard Now you just have to follow the same procedure, but writing down each step, and using the derivation rules. What you will obtain is the figure above, which happens to have 5 procedure lines (the first 4 are only to copy the truths). Each line corresponds with the steps given here. \layout Subsection Left side empty. \begin_inset Formula $\vdash P\Rightarrow P$ \end_inset \layout Standard Proving \begin_inset Formula $\vdash P\Rightarrow P$ \end_inset is very easy and short: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard \backslash fh P & H \backslash \backslash \layout Standard \backslash fa P & IT 1 \backslash \backslash \layout Standard P \backslash Rightarrow P & I$ \backslash Rightarrow$ 1,2 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Standard This case didn't occur before: now it seems that the left part of the sequent is empty. It means that we are not given any truth from which we can deduce \begin_inset Formula $P\Rightarrow P$ \end_inset . Why? Because \begin_inset Formula $P\Rightarrow P$ \end_inset is always true, not depending on the value of \begin_inset Formula $P$ \end_inset or other formulas. \layout Standard It's more comfortable and interesting to solve one of these demonstrations, since you start working directly on the formula which you want to achieve. But beware, since there are some \emph on absolute truths \emph default (always true) very hard and long to prove. \layout Standard Note down this: whenever the left side is empty, you must start doing a hypothesis (what else could you do?). \layout Standard To achieve \begin_inset Formula $P\Rightarrow P$ \end_inset we do as always: suppose that \begin_inset Formula $P$ \end_inset and try to see that \begin_inset Formula $P$ \end_inset is true. Since we just supposed it on the first line, we can use the \emph on iteration \emph default rule to copy it inside, and we finish the subdemonstration by using \emph on implication introduction \emph default . And we're done, in only three lines. \layout Standard Remark that \begin_inset Formula $P\Rightarrow P$ \end_inset is true because \begin_inset Formula $\blacksquare\Rightarrow\blacksquare$ \end_inset and \begin_inset Formula $\square\Rightarrow\square$ \end_inset . Well, and furthermore, remember also that \begin_inset Formula $\square\Rightarrow\blacksquare$ \end_inset , but \begin_inset Formula $\blacksquare\nRightarrow\square$ \end_inset . \layout Subsection Suppose the contrary. \begin_inset Formula $\vdash\neg(P\wedge\neg P)$ \end_inset \layout Standard Another simple one, \begin_inset Formula $\vdash\neg(P\wedge\neg P)$ \end_inset . It's done this way: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard \backslash fh P \backslash wedge \backslash neg P & H \backslash \backslash \layout Standard \backslash fa P & E$ \backslash wedge$ 1 \backslash \backslash \layout Standard \backslash fa \backslash neg P & E$ \backslash wedge$ 1 \backslash \backslash \layout Standard \backslash neg (P \backslash wedge \backslash neg P) & I$ \backslash neg$ 1,2 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Standard We all know that two contrary things can't happen at the same time, but, how can this be proved? We must use the \emph on reduction to the absurd \emph default : \layout Standard Suppose that it does happen \begin_inset Formula $P\wedge\neg P$ \end_inset . Then happen both \begin_inset Formula $P$ \end_inset and \begin_inset Formula $\neg P$ \end_inset , both at the same time, which is a contradiction. So, the supposition we just done can't be true: it's false. This way we can prove \begin_inset Formula $\neg(P\wedge\neg P)$ \end_inset . \layout Standard When you see something so \emph on clear \emph default and \emph on obvious \emph default as \begin_inset Formula $\neg(P\wedge\neg P)$ \end_inset , then its contrary will be \emph on clearly \emph default false and absurd. So, it won't be too difficult to see that it doesn't hold and that it contradic ts itself. Once done, we can assure that the original formula is true since its contrary is false. \layout Subsection This one seems easy. \begin_inset Formula $\vdash P\vee\neg P$ \end_inset \layout Standard Let's see if \begin_inset Formula $\vdash P\vee\neg P$ \end_inset is as easy as some say: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard \backslash fh \backslash neg (P \backslash vee \backslash neg P) & H \backslash \backslash \layout Standard \backslash fa \backslash fh P & H \backslash \backslash \layout Standard \backslash fa \backslash fa P \backslash vee \backslash neg P & I$ \backslash vee$ 2 \backslash \backslash \layout Standard \backslash fa \backslash fa \backslash neg (P \backslash vee \backslash neg P) & IT 1 \backslash \backslash \layout Standard \backslash fa \backslash neg P & I$ \backslash neg$ 2,3,4 \backslash \backslash \layout Standard \backslash fa \backslash fh \backslash neg P & H \backslash \backslash \layout Standard \backslash fa \backslash fa P \backslash vee \backslash neg P & I$ \backslash vee$ 6 \backslash \backslash \layout Standard \backslash fa \backslash fa \backslash neg (P \backslash vee \backslash neg P) & IT 1 \backslash \backslash \layout Standard \backslash fa \backslash neg \backslash neg P & I$ \backslash neg$ 6,7,8 \backslash \backslash \layout Standard \backslash fa P & E$ \backslash neg$ 9 \backslash \backslash \layout Standard \backslash neg \backslash neg (P \backslash vee \backslash neg P) & I$ \backslash neg$ 1,5,10 \backslash \backslash \layout Standard P \backslash vee \backslash neg P & E$ \backslash neg$ 11 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Standard One of the simplest but longest I found. It seems even unnecessary to prove this, since everyone knows that between \begin_inset Quotes eld \end_inset \emph on today it's Thursday \emph default \begin_inset Quotes erd \end_inset and \begin_inset Quotes eld \end_inset \emph on today it's not Thursday \emph default \begin_inset Quotes erd \end_inset , one of them is true (they can't be both be false at the same time). \layout Standard We could start by thinking in the \emph on proof by cases \emph default method, since from \begin_inset Formula $P$ \end_inset we can extract \begin_inset Formula $P\vee\neg P$ \end_inset , and from \begin_inset Formula $\neg P$ \end_inset we can extract \begin_inset Formula $P\vee\neg P$ \end_inset , so, the same formula. But this doesn't help, since \emph on proof by cases \emph default is the \emph on disjunction elimination \emph default , and we don't have any disjunction to eliminate; in fact, we also don't have the truth formula \begin_inset Formula $A\vee B$ \end_inset in which \begin_inset Formula $A\Rightarrow C$ \end_inset and \begin_inset Formula $B\Rightarrow C$ \end_inset , as the rule needs. Actually, we don't have any formula which we know it's true (as the left part of the sequent is empty). \layout Standard We know that we must start with a hypothesis (there's no alternative). Since it's rather clear that \begin_inset Formula $P\vee\neg P$ \end_inset is true, it may also be easy to prove that its contrary, \begin_inset Formula $\neg(P\vee\neg P)$ \end_inset , is false. So we will use \emph on reduction to the absurd \emph default : doing that supposition on line 1, we must achieve a contradiction, any one. \layout Standard I proposed myself to achieve the contradiction \begin_inset Formula $\neg P$ \end_inset and \begin_inset Formula $P$ \end_inset . But we don't have any of these formulas; how can we obtain them? Doing \emph on reduction to the absurd \emph default again is an option: to see that \begin_inset Formula $\neg P$ \end_inset , suppose that \begin_inset Formula $P$ \end_inset and get a contradiction. As we did in another occasions, it's very useful to profit the capabilities of the \emph on disjunction introduction \emph default : having supposed \begin_inset Formula $P$ \end_inset , we can convert it to \begin_inset Formula $P\vee\neg P$ \end_inset to search our contradiction. As we have the \begin_inset Formula $\neg(P\vee\neg P)$ \end_inset at the top, we can use it to finish by demonstrating \begin_inset Formula $\neg P$ \end_inset . We can do the same to prove \begin_inset Formula $P$ \end_inset , but this time supposing \begin_inset Formula $\neg P$ \end_inset . \layout Standard Having obtained \begin_inset Formula $P$ \end_inset and \begin_inset Formula $\neg P$ \end_inset after supposing \begin_inset Formula $\neg(P\vee\neg P)$ \end_inset , we see that this formula can't be true, so its negation, \begin_inset Formula $\neg\neg(P\vee\neg P)$ \end_inset , is. By \emph on negation elimination \emph default , we get our searched formula: \begin_inset Formula $P\vee\neg P$ \end_inset . \layout Standard I did it this way to make it rather symmetrical, but it can be shorter if we search another contradiction, for instance \begin_inset Formula $P\vee\neg P$ \end_inset and \begin_inset Formula $\neg(P\vee\neg P)$ \end_inset . Then it would be like this: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard \backslash fh \backslash neg (P \backslash vee \backslash neg P) & H \backslash \backslash \layout Standard \backslash fa \backslash fh P & H \backslash \backslash \layout Standard \backslash fa \backslash fa P \backslash vee \backslash neg P & I$ \backslash vee$ 2 \backslash \backslash \layout Standard \backslash fa \backslash fa \backslash neg (P \backslash vee \backslash neg P) & IT 1 \backslash \backslash \layout Standard \backslash fa \backslash neg P & I$ \backslash neg$ 2,3,4 \backslash \backslash \layout Standard \backslash fa P \backslash vee \backslash neg P & I$ \backslash vee$ 5 \backslash \backslash \layout Standard \backslash fa \backslash neg (P \backslash vee \backslash neg P) & IT 1 \backslash \backslash \layout Standard \backslash neg \backslash neg (P \backslash vee \backslash neg P) & I$ \backslash neg$ 1,6,7 \backslash \backslash \layout Standard P \backslash vee \backslash neg P & E$ \backslash neg$ 8 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Subsection An interesting one. \begin_inset Formula $P\vee Q,\ \neg P\vdash Q$ \end_inset \layout Standard Another which seems easy: \begin_inset Formula $P\vee Q,\ \neg P\vdash Q$ \end_inset . Let's see: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard P \backslash vee Q \backslash \backslash \layout Standard \backslash neg P \backslash \backslash \layout Standard \backslash fh P & H \backslash \backslash \layout Standard \backslash fa \backslash fh \backslash neg Q & H \backslash \backslash \layout Standard \backslash fa \backslash fa \backslash neg P & IT 2 \backslash \backslash \layout Standard \backslash fa \backslash fa P & IT 3 \backslash \backslash \layout Standard \backslash fa \backslash neg \backslash neg Q & I$ \backslash neg$ 4,5,6 \backslash \backslash \layout Standard \backslash fa Q & E$ \backslash neg$ 7 \backslash \backslash \layout Standard \backslash fh Q & H \backslash \backslash \layout Standard \backslash fa Q & IT 9 \backslash \backslash \layout Standard Q & E$ \backslash vee$ 1,8,10 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Standard It's very easy to understand by anyone: it holds \begin_inset Formula $P\vee Q$ \end_inset , but \begin_inset Formula $P$ \end_inset is false, so the truth is \begin_inset Formula $Q$ \end_inset . \layout Standard It can be done in several ways, but at some time you will have to use \emph on disjunction elimination \emph default to do something with the \begin_inset Formula $P\vee Q$ \end_inset . We're going to prove that both \begin_inset Formula $P$ \end_inset and \begin_inset Formula $Q$ \end_inset lead to the same place, which will be our target formula \begin_inset Formula $Q$ \end_inset (since it's possible, let's go directly for \begin_inset Formula $Q$ \end_inset ). \layout Standard We open subdemonstration supposing that \begin_inset Formula $P$ \end_inset , and we must see that \begin_inset Formula $Q$ \end_inset . It isn't too hard since we have \begin_inset Formula $\neg P$ \end_inset on line 2; this helps contradicting anything we want. Since what we're searching is \begin_inset Formula $Q$ \end_inset , we suppose \begin_inset Formula $\neg Q$ \end_inset and by \emph on reduction to the absurd \emph default we obtain \begin_inset Formula $\neg\neg Q$ \end_inset , which is \begin_inset Formula $Q$ \end_inset . \layout Standard The other path, when we suppose \begin_inset Formula $Q$ \end_inset true, leads us directly to \begin_inset Formula $Q$ \end_inset . \layout Standard In conclusion, both paths go to \begin_inset Formula $Q$ \end_inset and by \emph on disjunction elimination \emph default we get the proof that \begin_inset Formula $Q$ \end_inset is always certain. \layout Subsection I had this one in an exam. \begin_inset Formula $A\vee B,\ A\Rightarrow C,\ \neg D\Rightarrow\neg B\vdash C\vee D$ \end_inset \layout Standard In the final exam of \emph on ILO \emph default they were asking \begin_inset Formula $A\vee B,\ A\Rightarrow C,\ \neg D\Rightarrow\neg B\vdash C\vee D$ \end_inset , and I needed a very very long time until I got it: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard A \backslash vee B \backslash \backslash \layout Standard A \backslash Rightarrow C \backslash \backslash \layout Standard \backslash neg D \backslash Rightarrow \backslash neg B \backslash \backslash \layout Standard \backslash fh A & H \backslash \backslash \layout Standard \backslash fa C & E$ \backslash Rightarrow$ 2,4 \backslash \backslash \layout Standard \backslash fa C \backslash vee D & I$ \backslash vee$ 5 \backslash \backslash \layout Standard \backslash fh B & H \backslash \backslash \layout Standard \backslash fa \backslash fh \backslash neg D & H \backslash \backslash \layout Standard \backslash fa \backslash fa \backslash neg B & E$ \backslash Rightarrow$ 3,8 \backslash \backslash \layout Standard \backslash fa \backslash fa B & IT 7 \backslash \backslash \layout Standard \backslash fa \backslash neg \backslash neg D & I$ \backslash neg$ 8,9,10 \backslash \backslash \layout Standard \backslash fa D & E$ \backslash neg$ 11 \backslash \backslash \layout Standard \backslash fa C \backslash vee D & I$ \backslash vee$ 12 \backslash \backslash \layout Standard C \backslash vee D & E$ \backslash vee$ 1,6,13 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Standard Remark that the result we're searching, \begin_inset Formula $C\vee D$ \end_inset , is a disjunction. Since you already know the \emph on disjunction introduction \emph default , you could simply search \begin_inset Formula $C$ \end_inset , and then use that rule to get \begin_inset Formula $C\vee D$ \end_inset . Or if with \begin_inset Formula $C$ \end_inset didn't work, you could try with \begin_inset Formula $D$ \end_inset , since if \begin_inset Formula $D$ \end_inset is true, then \begin_inset Formula $C\vee D$ \end_inset also is, and we're done. \layout Standard Unfortunately, \begin_inset Formula $C$ \end_inset is not always true, and \begin_inset Formula $D$ \end_inset also isn't always true (on the other hand, \begin_inset Formula $C\vee D$ \end_inset is always true, and that's what we're trying to prove). After seeing this, we must search another method which works with the two formulas, \begin_inset Formula $C$ \end_inset and \begin_inset Formula $D$ \end_inset , at the same time, since it seems that if we take only one without looking at the other, then it does not provide much information. \layout Standard To use the \begin_inset Formula $A\vee B$ \end_inset we must use \emph on proof by cases \emph default . We will try to see that both \begin_inset Formula $A$ \end_inset and \begin_inset Formula $B$ \end_inset lead to \begin_inset Formula $C\vee D$ \end_inset , since if we can do that, we will have finished. \layout Standard \begin_inset Formula $A$ \end_inset implies \begin_inset Formula $C$ \end_inset , and if \begin_inset Formula $C$ \end_inset is true then \begin_inset Formula $C\vee D$ \end_inset also is, so \begin_inset Formula $A$ \end_inset implies \begin_inset Formula $C\vee D$ \end_inset . \layout Standard With \begin_inset Formula $B$ \end_inset , what we know doesn't relate it to \begin_inset Formula $C$ \end_inset but to \begin_inset Formula $D$ \end_inset . We want \begin_inset Formula $C\vee D$ \end_inset . Hardly we will make true \begin_inset Formula $C\vee D$ \end_inset because of \begin_inset Formula $C$ \end_inset , so we will try to make true just the \begin_inset Formula $D$ \end_inset . To do so, we will use \emph on reduction to the absurd \emph default : suppose that \begin_inset Formula $D$ \end_inset is false, then it holds that \begin_inset Formula $\neg B$ \end_inset thanks to the formula on line 3. But we were under the supposition that \begin_inset Formula $B$ \end_inset was true, so our hypothesis \begin_inset Formula $\neg D$ \end_inset can't be true, thus \begin_inset Formula $D$ \end_inset is true, and so is \begin_inset Formula $C\vee D$ \end_inset . \layout Standard Since \begin_inset Formula $A\vee B$ \end_inset is true, and both paths lead to \begin_inset Formula $C\vee D$ \end_inset , we finally see that \begin_inset Formula $C\vee D$ \end_inset is always true. \layout Standard If you are skilled working with logical formulas, you will have seen that \begin_inset Formula $\neg D\Rightarrow\neg B$ \end_inset is \begin_inset Formula $B\Rightarrow D$ \end_inset . This simplifies the problem and helps understanding it faster. But anyway, you can't change \begin_inset Formula $\neg D\Rightarrow\neg B$ \end_inset to \begin_inset Formula $B\Rightarrow D$ \end_inset directly, you would have to do it step by step. \layout Subsection A \begin_inset Quotes eld \end_inset short \begin_inset Quotes erd \end_inset one. \begin_inset Formula $A\Longleftrightarrow B\vdash(A\wedge B)\vee(\neg A\wedge\neg B)$ \end_inset \layout Standard Seems easy: if two expressions are equivalent, it's because they are both true, or both false. I could prove the validity of \begin_inset Formula $A\Longleftrightarrow B\vdash(A\wedge B)\vee(\neg A\wedge\neg B)$ \end_inset this way: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard (A \backslash Rightarrow B) \backslash wedge (B \backslash Rightarrow A) \backslash \backslash \layout Standard \backslash fh \backslash neg (A \backslash vee \backslash neg A) & H \backslash \backslash \layout Standard \backslash fa \backslash fh A & H \backslash \backslash \layout Standard \backslash fa \backslash fa A \backslash vee \backslash neg A & I$ \backslash vee$ 3 \backslash \backslash \layout Standard \backslash fa \backslash fa \backslash neg (A \backslash vee \backslash neg A) & IT 2 \backslash \backslash \layout Standard \backslash fa \backslash neg A & I$ \backslash neg$ 3,4,5 \backslash \backslash \layout Standard \backslash fa A \backslash vee \backslash neg A & I$ \backslash vee$ 6 \backslash \backslash \layout Standard \backslash fa \backslash neg (A \backslash vee \backslash neg A) & IT 2 \backslash \backslash \layout Standard \backslash neg \backslash neg (A \backslash vee \backslash neg A) & I$ \backslash neg$ 2,7,8 \backslash \backslash \layout Standard A \backslash vee \backslash neg A & E$ \backslash neg$ 9 \backslash \backslash \layout Standard \backslash fh A & H \backslash \backslash \layout Standard \backslash fa A \backslash Rightarrow B & E$ \backslash wedge$ 1 \backslash \backslash \layout Standard \backslash fa B & E$ \backslash Rightarrow$ 12,11 \backslash \backslash \layout Standard \backslash fa A \backslash wedge B & I$ \backslash wedge$ 11,13 \backslash \backslash \layout Standard \backslash fa (A \backslash wedge B) \backslash vee ( \backslash neg A \backslash wedge \backslash neg B) & I$ \backslash vee$ 14 \backslash \backslash \layout Standard \backslash fh \backslash neg A & H \backslash \backslash \layout Standard \backslash fa \backslash fh B & H \backslash \backslash \layout Standard \backslash fa \backslash fa B \backslash Rightarrow A & E$ \backslash wedge$ 1 \backslash \backslash \layout Standard \backslash fa \backslash fa A & E$ \backslash Rightarrow$ 18,17 \backslash \backslash \layout Standard \backslash fa \backslash fa \backslash neg A & IT 16 \backslash \backslash \layout Standard \backslash fa \backslash neg B & I$ \backslash neg$ 17,19,20 \backslash \backslash \layout Standard \backslash fa \backslash neg A \backslash wedge \backslash neg B & I$ \backslash wedge$ 16,21 \backslash \backslash \layout Standard \backslash fa (A \backslash wedge B) \backslash vee ( \backslash neg A \backslash wedge \backslash neg B) & I$ \backslash vee$ 22 \backslash \backslash \layout Standard (A \backslash wedge B) \backslash vee ( \backslash neg A \backslash wedge \backslash neg B) & E$ \backslash vee$ 10,15,23 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Standard Firstly: we can't write \begin_inset Formula $A\Longleftrightarrow B$ \end_inset since we don't have rules for \begin_inset Formula $\Longleftrightarrow$ \end_inset . Since it is seldom used, when a \begin_inset Formula $\Longleftrightarrow$ \end_inset appears we are allowed to change it to \begin_inset Formula $(A\Rightarrow B)\wedge(B\Rightarrow A)$ \end_inset , which is the same. \layout Standard Well, this is the only idea I had... I leave as an exercise to find a shorter way to do it (if it does exist). What I did here was to write down that \begin_inset Formula $A\vee\neg A$ \end_inset is true (we already did this exercise, and here I just copied the same steps). Once I know that \begin_inset Formula $A\vee\neg A$ \end_inset holds, I see that both the case \begin_inset Formula $A$ \end_inset and the case \begin_inset Formula $\neg A$ \end_inset lead to the same formula, which is the solution. \layout Section Wrong things \layout Standard Common errors you mustn't do. Remember that a logic professor will correct your exercises with a \emph on true \emph default or a \emph on false \emph default , so learn to do this perfectly. \layout Subsection Introduction and elimination of \emph on \begin_inset Quotes eld \end_inset what it would be nice to have \begin_inset Quotes erd \end_inset \layout Standard The rules like \emph on introduction \emph default and \emph on elimination \emph default are not to allow you writing anything you want, but to help you using or creating a formula with a concrete operator. \layout Standard That's why, if you have \begin_inset Formula $P$ \end_inset , you can't say \begin_inset Quotes eld \end_inset \emph on now I do \emph default negation introduction \emph on and get \begin_inset Formula $\neg P$ \end_inset , which is what I needed \emph default \begin_inset Quotes erd \end_inset . There are some requisites for each rule, and if you don't fulfill them, you can't apply that rule. \layout Standard For instance: the rule \emph on implication elimination \emph default doesn't allow to use the formulas in the first line this way: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard P \backslash Rightarrow Q \backslash wedge R \backslash \backslash \layout Standard Q \backslash wedge R & E$ \backslash Rightarrow$ 1,1 \layout Standard \backslash end{fitch} { \backslash textcolor{red}{ \backslash bigotimes INCORRECTO \backslash bigotimes}} \backslash ] \end_inset \layout Standard To be able to do this, we would need to be sure that \begin_inset Formula $P$ \end_inset is always true; then we could apply the rule, correctly writing the line numbers. \layout Subsection Iterate something from a non attainable subdemonstration \layout Standard Inside the main demonstration (which goes from the first line to the last), we can open \emph on child demonstrations \emph default ( \emph on subdemonstrations \emph default ). Inside any subdemonstration we can also have a \emph on subsubdemonstration \emph default , which would have as father the subdemonstration and as grandfather the main demonstration. \layout Standard To understand this, here is the solved example \begin_inset Formula $A\vee B,\ A\Rightarrow C,\ \neg D\Rightarrow\neg B\vdash C\vee D$ \end_inset : \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard A \backslash vee B \backslash \backslash \layout Standard A \backslash Rightarrow C \backslash \backslash \layout Standard \backslash neg D \backslash Rightarrow \backslash neg B \backslash \backslash \layout Standard \backslash fh A & H \backslash \backslash \layout Standard \backslash fa C & E$ \backslash Rightarrow$ 2,4 \backslash \backslash \layout Standard \backslash fa C \backslash vee D & I$ \backslash vee$ 5 \backslash \backslash \layout Standard \backslash fh B & H \backslash \backslash \layout Standard \backslash fa \backslash fh \backslash neg D & H \backslash \backslash \layout Standard \backslash fa \backslash fa \backslash neg B & E$ \backslash Rightarrow$ 3,8 \backslash \backslash \layout Standard \backslash fa \backslash fa B & IT 7 \backslash \backslash \layout Standard \backslash fa \backslash neg \backslash neg D & I$ \backslash neg$ 8,9,10 \backslash \backslash \layout Standard \backslash fa D & E$ \backslash neg$ 11 \backslash \backslash \layout Standard \backslash fa C \backslash vee D & I$ \backslash vee$ 12 \backslash \backslash \layout Standard C \backslash vee D & E$ \backslash vee$ 1,6,13 \layout Standard \backslash end{fitch} \backslash ] \end_inset \layout Standard Well, any demonstration can only access the formulas from inside itself, inside its father, inside the father of its father, inside the father of the father of its father, ... All these are called \emph on ancestors \emph default , so: \emph on a demonstration can access itself and its ancestors \emph default . \layout Standard For this reason, it we are on line 10, the derivation rules can use formulas from the following places: \layout Itemize the current demonstration (lines 8 and 9 currently). \layout Itemize father demonstration of the 8-10 one, so, from line 7. \layout Itemize from the demonstration father of the one which starts at line 7, that's it, lines 1 to 3. \layout Standard Bet never we could use the formulas from lines 4 to 6, which is the demonstratio n \emph on uncle \emph default of the current one (brother of its father), because all that demonstration is based on the hypothesis that \begin_inset Formula $A$ \end_inset (line 4), and we're not doing that supposition anymore. \layout Standard In logical language, one says that a formula \begin_inset Formula $A$ \end_inset is \emph on actual \emph default at formula \begin_inset Formula $B$ \end_inset if being in \begin_inset Formula $B$ \end_inset we can use \begin_inset Formula $A$ \end_inset . For this to be true, \begin_inset Formula $A$ \end_inset must have been written before \begin_inset Formula $B$ \end_inset , and some ancestor of \begin_inset Formula $B$ \end_inset must be father of \begin_inset Formula $A$ \end_inset . \layout Standard So, to prove \begin_inset Formula $P\wedge Q$ \end_inset we can't do this: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard \backslash fh P & H \backslash \backslash \layout Standard \backslash fa \backslash fh Q & H \backslash \backslash \layout Standard \backslash fa \backslash fa P \backslash wedge Q & I$ \backslash wedge$ 1,2 \backslash \backslash \layout Standard P \backslash wedge Q & IT 3 \layout Standard \backslash end{fitch} { \backslash textcolor{red}{ \backslash bigotimes INCORRECTO \backslash bigotimes}} \backslash ] \end_inset \layout Subsection Misplace parenthesis \layout Standard When I wrote the definitions of the rules, I used the letters \begin_inset Formula $A$ \end_inset and \begin_inset Formula $B$ \end_inset , but these can represent any expression. \layout Standard For instance, here we do \emph on negation introduction \emph default , in which -following the rule- we suppose some formula \begin_inset Formula $A$ \end_inset , attain a contradiction, and we conclude \begin_inset Formula $\neg A$ \end_inset , so, the original formula, but negated. Let's see: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch*} \layout Standard 1 & \backslash fh P \backslash Rightarrow Q & H \backslash \backslash \layout Standard \backslash ldots & \backslash fa \backslash ldots \backslash \backslash \layout Standard 7 & \backslash neg P \backslash Rightarrow Q & I$ \backslash neg$ 1, \backslash ldots \layout Standard \backslash end{fitch*} { \backslash textcolor{red}{ \backslash bigotimes INCORRECTO \backslash bigotimes}} \backslash ] \end_inset \layout Standard I think it's clear that the \begin_inset Formula $A$ \end_inset which appears in the rule represents to \begin_inset Formula $P\Rightarrow Q$ \end_inset in this example. The problem comes when we do the \begin_inset Formula $\neg A$ \end_inset . The negation of \begin_inset Formula $P\Rightarrow Q$ \end_inset is not \begin_inset Formula $\neg P\Rightarrow Q$ \end_inset , but \begin_inset Formula $\neg(P\Rightarrow Q)$ \end_inset . It's necessary that parenthesis because if not present, the negation affects only \begin_inset Formula $P$ \end_inset . \layout Standard If you don't know when to put parenthesis, always put them, and then try to remove the unneeded ones. For instance, if you must write that \begin_inset Formula $\neg P\vee R$ \end_inset implies \begin_inset Formula $R\wedge Q$ \end_inset , put parenthesis around each expression and thus write \begin_inset Formula $(\neg P\vee R)\Rightarrow(R\wedge Q)$ \end_inset . This way, there are absolutely no errors. Now learn when is it possible to remove parenthesis, and take away all that you can. In this case, both can be suppressed and it remains \begin_inset Formula $\neg P\vee R\Rightarrow R\wedge Q$ \end_inset . \layout Subsection Finish inside a subdemonstration \layout Standard You can't finish the deduction inside a subdemonstration. The last line can't have any vertical line to the left. \layout Standard The reason is that everything from inside the subdemonstration is valid only when the supposition is really true, and what the original problem asks is to prove that the formula at the right of the \begin_inset Formula $\vdash$ \end_inset is \emph on always \emph default true. \layout Standard Here's a sample of what can be tried by someone very astute who wants to prove \begin_inset Formula $P\wedge Q$ \end_inset : \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch} \layout Standard \backslash fh P & H \backslash \backslash \layout Standard \backslash fa \backslash fh Q & H \backslash \backslash \layout Standard \backslash fa \backslash fa P \backslash wedge Q & I$ \backslash wedge$ 1,2 \layout Standard \backslash end{fitch} { \backslash textcolor{red}{ \backslash bigotimes INCORRECTO \backslash bigotimes}} \backslash ] \end_inset \layout Standard We supposed \begin_inset Formula $P$ \end_inset , and also \begin_inset Formula $Q$ \end_inset . In that case, of course it's true that \begin_inset Formula $P\wedge Q$ \end_inset , but only in that case. We can't affirm to anyone that \begin_inset Formula $P\wedge Q$ \end_inset is always true. So, we should start closing the two demonstrations (first the inner one, and then the outer one) to extract some conclusion which is always valid. \layout Standard Neither could we do that \emph on iteration \emph default thing at line 4. I already explained this before. \layout Subsection Skip steps \layout Standard Even if you know equivalences between formulas, it's much better if you don't use them. For instance, if you have to write the negation of \begin_inset Formula $\neg P$ \end_inset , don't write \begin_inset Formula $P$ \end_inset directly, but \begin_inset Formula $\neg\neg P$ \end_inset . \layout Standard Understand that not everything is so obvious as it seems, and that someone may ask you to prove things like \begin_inset Formula $P\vdash\neg\neg P$ \end_inset , where if you could use those simplifications, you would do almost no work. \layout Standard Another example: going from \begin_inset Formula $\neg(A\vee B)$ \end_inset in one line to having \begin_inset Formula $\neg A\wedge\neg B$ \end_inset in the next can't be justified with any of the 9 rules. But if you succeed in proving and understanding that \begin_inset Formula $\neg(A\vee B)\vdash\neg A\wedge\neg B$ \end_inset , then maybe you can add that as an additional rule to use in future demonstrati ons. I will give some of these in the next section. \layout Section Making it harder \layout Standard Here I will finish the explanation of everything else that I was taught about natural deduction (even if we didn't use it very much). The quantifiers thing is really important, but more complex. \layout Subsection Rules about truth and false \layout Standard We can work directly with the values \begin_inset Formula $\blacksquare$ \end_inset ( \emph on true \emph default ) and \begin_inset Formula $\square$ \end_inset ( \emph on false \emph default ), and also introduce or eliminate them from our demonstration following some easy rules. \layout Subsubsection Truth introduction \layout Standard This is the easiest one: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch*} \layout Standard \backslash hline \layout Standard & \backslash blacksquare & I$ \backslash blacksquare$ \layout Standard \backslash end{fitch*} \backslash ] \end_inset \layout Standard So, always, and with no requirements, we can write down that \begin_inset Formula $\blacksquare$ \end_inset is true, because it really is. \layout Subsubsection False elimination \layout Standard A funny one: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch*} \layout Standard n & \backslash square \backslash \backslash \layout Standard \backslash hline \layout Standard & A & E$ \backslash square$ n \layout Standard \backslash end{fitch*} \backslash ] \end_inset \layout Standard Explanation: if we achieved the conclusion that \begin_inset Formula $\square$ \end_inset is true, then we have already achieved a state where we can invent anything and affirm that it's true; at least, as true as the idea of \begin_inset Formula $\square$ \end_inset ( \emph on false \emph default ) being true. \layout Standard This rule is called \emph on ex falso quodlibet sequitur \emph default , something like \begin_inset Quotes eld \end_inset \emph on from false can follow anything \emph default \begin_inset Quotes erd \end_inset . \layout Subsection Rules about quantifiers \layout Standard We're too limited if we can only say things like \begin_inset Formula $P$ \end_inset , \begin_inset Formula $Q$ \end_inset , \begin_inset Formula $R$ \end_inset , ... to translate phrases to logical language. Quantifiers will allow us to do much more. \layout Subsubsection What's that \layout Standard I won't be able to explain everything, since various previous concepts are needed, but I will try to say a little about them. First, some changes: \layout Standard Now we won't talk just about general facts ( \emph on it rains \emph default , \emph on it's warm \emph default , etc.), but we will have a \emph on domain \emph default of known things, and we will have to say which property is true for each element. \layout Standard For instance: we have the domain \begin_inset Formula $\{ p,\ t,\ r\}$ \end_inset , which represent respectively to \emph on PROLOG \emph default (a logical programming language), a \emph on telephone \emph default , and a \emph on radio \emph default . \emph on p \emph default , \emph on t \emph default , \emph on r \emph default . \layout Standard We also add a \emph on predicate letter \emph default (they're not called \emph on propositional letters \emph default anymore) \begin_inset Formula $E$ \end_inset , which will have the following meaning: when we write \begin_inset Formula $Ex$ \end_inset (read \begin_inset Quotes eld \end_inset \emph on \begin_inset Formula $E$ \end_inset of \begin_inset Formula $x$ \end_inset \emph default \begin_inset Quotes erd \end_inset , but written together) we mean that \emph on \begin_inset Formula $x$ \end_inset is an electronic device \emph default . We will also have \begin_inset Formula $Sx$ \end_inset to say that \emph on \begin_inset Formula $x$ \end_inset is a piece of software \emph default , and \begin_inset Formula $Tx$ \end_inset which will mean that \emph on \begin_inset Formula $x$ \end_inset is a text processor \emph default . \layout Standard Now we know that are true \begin_inset Formula $Et$ \end_inset , \begin_inset Formula $Er$ \end_inset , \begin_inset Formula $Sp$ \end_inset and nothing else. \layout Standard Quantifiers make possible to write truths referring to some elements from the domain. There exist two quantifiers: \layout Itemize Universal quantifier: \begin_inset Formula $\forall$ \end_inset . When we put \begin_inset Formula $\forall xPx$ \end_inset ( \begin_inset Quotes eld \end_inset \emph on for all \begin_inset Formula $x$ \end_inset , \begin_inset Formula $P$ \end_inset of \begin_inset Formula $x$ \end_inset \emph default \begin_inset Quotes erd \end_inset ), we mean that all elements on the domain make true the property \begin_inset Formula $P$ \end_inset . \layout Itemize Existential quantifier: \begin_inset Formula $\exists$ \end_inset . \begin_inset Formula $\exists xPx$ \end_inset ( \begin_inset Quotes eld \end_inset \emph on there exists \begin_inset Formula $x$ \end_inset such that \begin_inset Formula $P$ \end_inset of \begin_inset Formula $x$ \end_inset \emph default \begin_inset Quotes erd \end_inset ) we mean that at least one element from the domain makes true the property \begin_inset Formula $P$ \end_inset . \layout Standard For instance, now are true the following formulas: \begin_inset Formula $\forall x(Ex\vee Sx)$ \end_inset , \begin_inset Formula $\neg\exists xTx$ \end_inset , \begin_inset Formula $\forall x(Tx\Rightarrow\neg Ex)$ \end_inset , \begin_inset Formula $\exists xEx\wedge\exists xSx$ \end_inset and several more. Quantifiers have the same priority as the operator \begin_inset Formula $\neg$ \end_inset . \layout Standard The rules explained here will work only with \emph on free substitutions \emph default . Sorry for not saying what that means, but I don't want to go out of topic. \layout Subsubsection Existential introduction \layout Standard If we see a proof of its existence, we can say that a property is true for some element: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch*} \layout Standard n & A \backslash {t/x \backslash } \backslash \backslash \layout Standard \backslash hline \layout Standard & \backslash exists x A & I$ \backslash exists$ n,t \layout Standard \backslash end{fitch*} \backslash ] \end_inset \layout Standard That \begin_inset Formula $A\{ t/x\}$ \end_inset is a \emph on substitution \emph default (maybe read \begin_inset Quotes eld \end_inset \emph on \begin_inset Formula $t$ \end_inset over \begin_inset Formula $x$ \end_inset \emph default \begin_inset Quotes erd \end_inset and is done by changing \begin_inset Formula $x$ \end_inset to \begin_inset Formula $t$ \end_inset ). \layout Standard This rule says that if we see \begin_inset Formula $At$ \end_inset , where \begin_inset Formula $t$ \end_inset is any element, we can say that \begin_inset Formula $\exists xAx$ \end_inset , because we know that when \begin_inset Formula $x$ \end_inset is \begin_inset Formula $t$ \end_inset then the formula is true. \layout Subsubsection Existential elimination \layout Standard Extracting some truth from a \begin_inset Formula $\exists xPx$ \end_inset is tricky, but it's done this way: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch*} \layout Standard m & \backslash exists x A \backslash \backslash \layout Standard n & \backslash fh A \backslash {a/x \backslash } & H \backslash \backslash \layout Standard p & \backslash fa B \backslash \backslash \layout Standard \backslash hline \layout Standard & B & E$ \backslash exists$ m,n,p,a \layout Standard \backslash end{fitch*} \backslash ] \end_inset \layout Standard So, if one of the \begin_inset Formula $A$ \end_inset implies \begin_inset Formula $B$ \end_inset , then we know that \begin_inset Formula $B$ \end_inset , since we know that one of the \begin_inset Formula $A$ \end_inset is true. No \begin_inset Formula $a$ \end_inset should appear in \begin_inset Formula $B$ \end_inset nor in any attainable hypothesis (sorry for the cryptical phrases, they are part of the theory). \layout Subsubsection Universal introduction \layout Standard Well, this one is easy: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch*} \layout Standard n & A \backslash \backslash \layout Standard \backslash hline \layout Standard & \backslash forall x A & I$ \backslash forall$ n \layout Standard \backslash end{fitch*} \backslash ] \end_inset \layout Standard So, if we know that \begin_inset Formula $A$ \end_inset is always true, then it is true for any value of \begin_inset Formula $x$ \end_inset . No \emph on free \emph default \begin_inset Formula $x$ \end_inset should appear in any attainable hypothesis. \layout Subsubsection Universal elimination \layout Standard Another easy one: \layout Standard \begin_inset ERT status Collapsed \layout Standard \backslash [ \backslash begin{fitch*} \layout Standard n & \backslash forall x A \backslash \backslash \layout Standard \backslash hline \layout Standard & A \backslash {t/x \backslash } & E$ \backslash forall$ n,t \layout Standard \backslash end{fitch*} \backslash ] \end_inset \layout Standard If we know that \begin_inset Formula $A$ \end_inset always holds for any element, then we can select an element (anyone) and we also know that \begin_inset Formula $A$ \end_inset is true on that element. \layout Subsubsection Examples \layout Standard At the last section there are several examples with quantifiers, but without explanations. Probably you will have to look for them in some logic book if you're trying to understand them. \layout Subsection Derived rules \layout Standard In some books or tutorials more rules are allowed (apart from the basic 9) in order to deal with formulas more easily. They represent an abstraction: stop working in the details to dedicate our work in more complex problems (it's like the \emph on high level \emph default programming languages). \layout Standard If you decide to use them, you will lose a lot of interesting work to do, but you will finish faster. My advice is to only use a rule if you know how to prove its validity by using the 9 basic rules. \layout Standard Some of the ones I found at several places are: \layout Itemize \emph on Law of double negation \emph default : allows changing \begin_inset Formula $A$ \end_inset to \begin_inset Formula $\neg\neg A$ \end_inset and viceversa. \layout Itemize \emph on Modus Tollens \emph default : having \begin_inset Formula $A\Rightarrow B$ \end_inset and \begin_inset Formula $\neg B$ \end_inset , then \begin_inset Formula $\neg A$ \end_inset . \layout Itemize \emph on Disjunctive syllogism \emph default : if \begin_inset Formula $A\vee B$ \end_inset and \begin_inset Formula $\neg A$ \end_inset , then \begin_inset Formula $B$ \end_inset . And if \begin_inset Formula $A\vee B$ \end_inset and \begin_inset Formula $\neg B$ \end_inset , then it's \begin_inset Formula $A$ \end_inset . \layout Itemize \emph on Elimination of \begin_inset Formula $\neg$ \end_inset \begin_inset Formula $\Rightarrow$ \end_inset \emph default : if you have \begin_inset Formula $\neg(A\Rightarrow B)$ \end_inset , then happen both \begin_inset Formula $A$ \end_inset and \begin_inset Formula $\neg B$ \end_inset . \layout Itemize \emph on Elimination of \begin_inset Formula $\neg$ \end_inset \begin_inset Formula $\vee$ \end_inset \emph default : if you have \begin_inset Formula $\neg(A\vee B)$ \end_inset , then \begin_inset Formula $\neg A$ \end_inset , and also \begin_inset Formula $\neg B$ \end_inset . \layout Itemize \emph on Elimination of \begin_inset Formula $\neg\wedge$ \end_inset \emph default : if you have \begin_inset Formula $\neg(A\wedge B)$ \end_inset , then \begin_inset Formula $\neg A\vee\neg B$ \end_inset . \layout Itemize \emph on Theorems which you can use when you want \emph default : \begin_inset Formula $A\Rightarrow A$ \end_inset , \begin_inset Formula $A\vee\neg A$ \end_inset , \begin_inset Formula $\neg(A\wedge\neg A)$ \end_inset and more. \layout Itemize \emph on Change of equivalent formulas \emph default : if \begin_inset Formula $A\Longleftrightarrow B$ \end_inset , then where it says \begin_inset Formula $A$ \end_inset you can put \begin_inset Formula $B$ \end_inset and viceversa. \layout Standard There are lots more; but if someone requests you an exercise, they will tell you which rules are allowed and which not (for instance, in class we were allowed to use only the basic ones). \layout Section Extra \layout Standard If you already knew everything I explained, or have doubts about other topics unrelated to the way of doing natural deduction, stay at this section. \layout Subsection Why is it called natural deduction? \layout Standard Because the procedures to be applied are the same that the ones people use when they think. \layout Standard You can see that at most solved exercises in this manual. Express the sequents by words, tell them to someone, and after some time he/she will be saying \begin_inset Quotes eld \end_inset \emph on of course it's like that, since ... \emph default \begin_inset Quotes erd \end_inset . You will see that anyone is able to explain how to use some of the 9 derivation rules, even without knowing their name or existence. \layout Standard For this reason, to discover the solution to a natural deduction problem, forget about \emph on introduction \emph default and \emph on elimination \emph default rules, and think normally, changing the letters to simple actions if necessary. It can help to think of concepts like \emph on it rains \emph default , \emph on it doesn't rain \emph default , \emph on it's sunny \emph default , \emph on I don't get wet \emph default , ... since they are short words and, moreover, everyone has a clear understanding of what does happen when it rains, and can rapidly relate \emph on not getting wet \emph default with \emph on being sunny and not raining \emph default , or even more complex formulas. \layout Subsection Is the solution unique? \layout Standard No. The more complex the exercise, the more ways to solve it correctly there are. In the section about explained exercises, I already gave several solutions to one of them. \layout Standard Of course, you can start deducing things which are absolutely unneeded, and you will achieve a solution different from the others. But it's better to try to solve each exercise in the minimum number of steps. \layout Subsection Other ways to prove validity \layout Standard Natural deduction is a way to prove the validity of a sequent, but there exist still more. Some of them are: \layout Subsubsection Brute force \layout Standard We can list all the possible combinations of values for each variable, and check that, for each combination, if the left part of the sequent is true then the right part is also true. \layout Standard Working with \begin_inset Formula $n$ \end_inset variables, you will have to test \begin_inset Formula $2^{n}$ \end_inset cases. \layout Standard The problem here are quantifiers, since now there's a domain involved. And we're not able to list some of the possible existing domains, since a domain can have infinite elements. \layout Subsubsection Refutation theorem \layout Standard Refutation theorem says that \begin_inset Formula $\Gamma\vDash A\Longleftrightarrow\ \nVdash\Gamma,\neg A$ \end_inset . \layout Standard In words: the set of formulas \begin_inset Formula $\Gamma$ \end_inset ( \emph on gamma \emph default ) has as consequence \begin_inset Formula $A$ \end_inset