{"action":"opened","issue":{"url":"https://api.github.com/repos/guevara/read-it-later/issues/1857","repository_url":"https://api.github.com/repos/guevara/read-it-later","labels_url":"https://api.github.com/repos/guevara/read-it-later/issues/1857/labels{/name}","comments_url":"https://api.github.com/repos/guevara/read-it-later/issues/1857/comments","events_url":"https://api.github.com/repos/guevara/read-it-later/issues/1857/events","html_url":"https://github.com/guevara/read-it-later/issues/1857","id":392055469,"node_id":"MDU6SXNzdWUzOTIwNTU0Njk=","number":1857,"title":"Jeremy Siek: How to Prove It","user":{"login":"guevara","id":228309,"node_id":"MDQ6VXNlcjIyODMwOQ==","avatar_url":"https://avatars1.githubusercontent.com/u/228309?v=4","gravatar_id":"","url":"https://api.github.com/users/guevara","html_url":"https://github.com/guevara","followers_url":"https://api.github.com/users/guevara/followers","following_url":"https://api.github.com/users/guevara/following{/other_user}","gists_url":"https://api.github.com/users/guevara/gists{/gist_id}","starred_url":"https://api.github.com/users/guevara/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/guevara/subscriptions","organizations_url":"https://api.github.com/users/guevara/orgs","repos_url":"https://api.github.com/users/guevara/repos","events_url":"https://api.github.com/users/guevara/events{/privacy}","received_events_url":"https://api.github.com/users/guevara/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":0,"created_at":"2018-12-18T08:59:40Z","updated_at":"2018-12-18T08:59:40Z","closed_at":null,"author_association":"OWNER","body":"Jeremy Siek: How to Prove It<br>\n<br>\nhttps://ift.tt/2iVAD1I<br>\n<br>\n<br>\n<br>\n<div>\n<div>\n<p>One of the better books that introduces rigorous proof is <i>How to Prove It</i> by Daniel J. Velleman. Here I'm going to discuss one of the key skills from that book, which is recognizing what form of proof is appropriate for the kind of thing you want to prove. This skill is the easy part of doing proofs, but I find that many students are too slow in this regard. Analogous to a computer game, one needs to become fast with the button combinations. You shouldn't have to think consciously about them. The same is true for the basics of proof. There's a bunch of stuff that should be automatic, at the tips of your fingers. Once this is accomplished, your mind is then free to think about the truly hard aspects of more difficult proofs.</p>\n<p>For today, what we're going to prove is formulas in propositional logic. These formulas form a little language, defined by the grammar below. We'll use lowercase letters to represent propositional variables. These variables represent statements such as \"socrates is mortal\". We'll use uppercase letters as placeholders for formulas. The kinds of formulas, working left to right, are variables, the trivial formulas <span><span><span><span>T</span><span>r</span><span>u</span><span>e</span></span></span></span><span tabindex=\"0\"><span><span><span><span><span><span><span><span>T</span><span>r</span><span>u</span><span>e</span></span></span></span></span></span></span></span></span> and <span><span><span><span>F</span><span>a</span><span>l</span><span>s</span><span>e</span></span></span></span><span tabindex=\"0\"><span><span><span><span><span><span><span><span>F</span><span>a</span><span>l</span><span>s</span><span>e</span></span></span></span></span></span></span></span></span>, negation (<span><span><span>&not;</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>&not;</span></span></span></span></span></span></span>), logical and (<span><span><span>&and;</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>&and;</span></span></span></span></span></span></span>), logical or (<span><span><span>&or;</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>&or;</span></span></span></span></span></span></span>), and implication (<span><span><span>&rarr;</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>&rarr;</span></span></span></span></span></span></span>). We refer to the symbols <span><span><span>&and;</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>&and;</span></span></span></span></span></span></span>, <span><span><span>&or;</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>&or;</span></span></span></span></span></span></span>, etc. as <i>logical connectives</i>. <span><span><span><span><span><span><span>Variables</span></span><span><span>p</span><span>,</span><span>q</span></span></span><span><span><span>Formulas</span></span><span><span>P</span><span>,</span><span>Q</span><span>,</span><span>R</span></span><span><span>::=</span></span><span><span>p</span><span>&#8739;</span><span><span>T</span><span>r</span><span>u</span><span>e</span></span><span>&#8739;</span><span><span>F</span><span>a</span><span>l</span><span>s</span><span>e</span></span><span>&#8739;</span><span>&not;</span><span>P</span></span></span><span><span><span>&#8739;</span><span>P</span><span>&and;</span><span>Q</span><span>&#8739;</span><span>P</span><span>&or;</span><span>Q</span><span>&#8739;</span><span>P</span><span>&rarr;</span><span>Q</span></span></span></span></span></span></span></p>\n<p><span tabindex=\"0\"><span><span><span><span><span><span><span><span><span><span><span><span><span>Variables</span></span></span></span><span><span><span><span>Formulas</span></span></span></span></span></span><span><span><span><span><span><span>p</span><span>,</span><span>q</span></span></span></span><span><span><span><span>P</span><span>,</span><span>Q</span><span>,</span><span>R</span></span></span></span></span></span><span><span><span><span><span><span>:<span>:</span><span>=</span></span></span></span></span></span></span><span><span><span><span><span><span>p</span><span>&#8739;</span><span><span><span>T</span><span>r</span><span>u</span><span>e</span></span></span><span>&#8739;</span><span><span><span>F</span><span>a</span><span>l</span><span>s</span><span>e</span></span></span><span>&#8739;</span><span>&not;</span><span>P</span></span></span></span><span><span><span><span>&#8739;</span><span>P</span><span>&and;</span><span>Q</span><span>&#8739;</span><span>P</span><span>&or;</span><span>Q</span><span>&#8739;</span><span>P</span><span>&rarr;</span><span>Q</span></span></span></span></span></span></span></span></span></span></span></span></span></span></p>\nThe following is an example of a formula: <span><span><span>(</span><span>p</span><span>&rarr;</span><span>q</span><span>)</span><span>&and;</span><span>&not;</span><span>q</span><span>&rarr;</span><span>&not;</span><span>p</span></span></span>\n<p><span tabindex=\"0\"><span><span><span><span><span><span>(</span><span>p</span><span>&rarr;</span><span>q</span><span>)</span><span>&and;</span><span>&not;</span><span>q</span><span>&rarr;</span><span>&not;</span><span>p</span></span></span></span></span></span></span></p>\n<h3>Identify the Main Connective</h3>\n<p>The first skill needed to recognize what form of proof is needed to prove a formula, such as the one above, is the ability to identify the <i>main connective</i> of a formula. The main connective is at the root of the parse tree for the formula. One can construct a parse tree by starting at the leaves and working your way towards the root. The leaves are the formulas that don't have any sub-parts. Constructing a parse tree is equivalent to adding parentheses to every sub-part of a formula, which is what we'll do here. In the above formula, the leaves are: <span><span><span>p</span><span>,</span><span>q</span><span>,</span><span>q</span><span>,</span><span>p</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>p</span><span>,</span><span>q</span><span>,</span><span>q</span><span>,</span><span>p</span></span></span></span></span></span></span>. Working from the first <span><span><span>p</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>p</span></span></span></span></span></span></span> and <span><span><span>q</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>q</span></span></span></span></span></span></span> we have <span><span><span>(</span><span>p</span><span>&rarr;</span><span>q</span><span>)</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>(</span><span>p</span><span>&rarr;</span><span>q</span><span>)</span></span></span></span></span></span></span>. (We just used the grammar rule <span><span><span>P</span><span>::=</span><span>P</span><span>&rarr;</span><span>Q</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>P</span><span>:<span>:</span><span>=</span></span><span>P</span><span>&rarr;</span><span>Q</span></span></span></span></span></span></span>.) Working our way from the last <span><span><span>p</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>p</span></span></span></span></span></span></span> we have <span><span><span>(</span><span>&not;</span><span>p</span><span>)</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>(</span><span>&not;</span><span>p</span><span>)</span></span></span></span></span></span></span>. For the second occurrence of <span><span><span>q</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>q</span></span></span></span></span></span></span> we have two choices, we can either go to the left to form <span><span><span>(</span><span>&not;</span><span>q</span><span>)</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>(</span><span>&not;</span><span>q</span><span>)</span></span></span></span></span></span></span> or we can go to the right and form <span><span><span>(</span><span>q</span><span>&rarr;</span><span>(</span><span>&not;</span><span>p</span><span>)</span><span>)</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>(</span><span>q</span><span>&rarr;</span><span>(</span><span>&not;</span><span>p</span><span>)</span><span>)</span></span></span></span></span></span></span>. Here we need to use the precedence of the connectives to decide what to do. The grammar above lists the formulas in the order of their precedence. So <span><span><span>&not;</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>&not;</span></span></span></span></span></span></span> is higher precedence than <span><span><span>&rarr;</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>&rarr;</span></span></span></span></span></span></span>, so we go to the left and form <span><span><span>(</span><span>&not;</span><span>q</span><span>)</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>(</span><span>&not;</span><span>q</span><span>)</span></span></span></span></span></span></span>. So far, we have parses for <span><span><span>(</span><span>p</span><span>&rarr;</span><span>q</span><span>)</span><span>,</span><span>(</span><span>&not;</span><span>q</span><span>)</span><span>,</span><span>(</span><span>&not;</span><span>p</span><span>)</span></span></span></p>\n<p><span tabindex=\"0\"><span><span><span><span><span><span>(</span><span>p</span><span>&rarr;</span><span>q</span><span>)</span><span>,</span><span>(</span><span>&not;</span><span>q</span><span>)</span><span>,</span><span>(</span><span>&not;</span><span>p</span><span>)</span></span></span></span></span></span></span></p>\nNext, we need to decide whether to combine <span><span><span>(</span><span>p</span><span>&rarr;</span><span>q</span><span>)</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>(</span><span>p</span><span>&rarr;</span><span>q</span><span>)</span></span></span></span></span></span></span> and <span><span><span>(</span><span>&not;</span><span>q</span><span>)</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>(</span><span>&not;</span><span>q</span><span>)</span></span></span></span></span></span></span> with the connective <span><span><span>&and;</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>&and;</span></span></span></span></span></span></span>, or whether to combine <span><span><span>(</span><span>&not;</span><span>q</span><span>)</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>(</span><span>&not;</span><span>q</span><span>)</span></span></span></span></span></span></span> and <span><span><span>(</span><span>&not;</span><span>p</span><span>)</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>(</span><span>&not;</span><span>p</span><span>)</span></span></span></span></span></span></span> with the connective <span><span><span>&rarr;</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>&rarr;</span></span></span></span></span></span></span>. Again, we consider the precedences, and here <span><span><span>&and;</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>&and;</span></span></span></span></span></span></span> has higher precedence than <span><span><span>&rarr;</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>&rarr;</span></span></span></span></span></span></span>. So we have the parses: <span><span><span>(</span><span>(</span><span>p</span><span>&rarr;</span><span>q</span><span>)</span><span>&and;</span><span>(</span><span>&not;</span><span>q</span><span>)</span><span>)</span><span>,</span><span>(</span><span>&not;</span><span>p</span><span>)</span></span></span>\n<p><span tabindex=\"0\"><span><span><span><span><span><span>(</span><span>(</span><span>p</span><span>&rarr;</span><span>q</span><span>)</span><span>&and;</span><span>(</span><span>&not;</span><span>q</span><span>)</span><span>)</span><span>,</span><span>(</span><span>&not;</span><span>p</span><span>)</span></span></span></span></span></span></span></p>\nThe last step is to parse the last connective, <span><span><span>&rarr;</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>&rarr;</span></span></span></span></span></span></span>, and complete the tree: <span><span><span>(</span><span>(</span><span>(</span><span>p</span><span>&rarr;</span><span>q</span><span>)</span><span>&and;</span><span>(</span><span>&not;</span><span>q</span><span>)</span><span>)</span><span>&rarr;</span><span>(</span><span>&not;</span><span>p</span><span>)</span><span>)</span></span></span>\n<p><span tabindex=\"0\"><span><span><span><span><span><span>(</span><span>(</span><span>(</span><span>p</span><span>&rarr;</span><span>q</span><span>)</span><span>&and;</span><span>(</span><span>&not;</span><span>q</span><span>)</span><span>)</span><span>&rarr;</span><span>(</span><span>&not;</span><span>p</span><span>)</span><span>)</span></span></span></span></span></span></span></p>\nThe root of the tree is the last connective that we added to complete the parse, in this case, the right-most <span><span><span>&rarr;</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>&rarr;</span></span></span></span></span></span></span>. So we have found the main connective. It's also important to know the two sub-trees of the main connective. In this case, <span><span><span>(</span><span>(</span><span>p</span><span>&rarr;</span><span>q</span><span>)</span><span>&and;</span><span>(</span><span>&not;</span><span>q</span><span>)</span><span>)</span><span>(</span><span>&not;</span><span>p</span><span>)</span></span></span>\n<p><span tabindex=\"0\"><span><span><span><span><span><span>(</span><span>(</span><span>p</span><span>&rarr;</span><span>q</span><span>)</span><span>&and;</span><span>(</span><span>&not;</span><span>q</span><span>)</span><span>)</span><span>(</span><span>&not;</span><span>p</span><span>)</span></span></span></span></span></span></span></p>\n<h3>Prove It!</h3>\n<p>Now that we've found the main connective, we just do a simple table look-up to figure out what form of proof we should use. Here's the table, which we call the prove-it table.</p>\n<ol>\n<li>\n<span><span><span>&not;</span><span>P</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>&not;</span><span>P</span></span></span></span></span></span></span>: assume <span><span><span>P</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>P</span></span></span></span></span></span></span> and prove <span><span><span><span>F</span><span>a</span><span>l</span><span>s</span><span>e</span></span></span></span><span tabindex=\"0\"><span><span><span><span><span><span><span><span>F</span><span>a</span><span>l</span><span>s</span><span>e</span></span></span></span></span></span></span></span></span>.</li>\n<li>\n<span><span><span>P</span><span>&and;</span><span>Q</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>P</span><span>&and;</span><span>Q</span></span></span></span></span></span></span>: prove <span><span><span>P</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>P</span></span></span></span></span></span></span> and also prove <span><span><span>Q</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>Q</span></span></span></span></span></span></span>.</li>\n<li>\n<span><span><span>P</span><span>&or;</span><span>Q</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>P</span><span>&or;</span><span>Q</span></span></span></span></span></span></span>: prove one of <span><span><span>P</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>P</span></span></span></span></span></span></span> or <span><span><span>Q</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>Q</span></span></span></span></span></span></span>.</li>\n<li>\n<span><span><span>P</span><span>&rarr;</span><span>Q</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>P</span><span>&rarr;</span><span>Q</span></span></span></span></span></span></span>: assume <span><span><span>P</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>P</span></span></span></span></span></span></span> and then prove <span><span><span>Q</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>Q</span></span></span></span></span></span></span>.</li>\n</ol>\n<p>Our main connective is</p>\n<span><span><span>&rarr;</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>&rarr;</span></span></span></span></span></span></span>\n<p>, so we can begin our proof using prove-it rule 4:</p>\n<blockquote>Assume <span><span><span>(</span><span>p</span><span>&rarr;</span><span>q</span><span>)</span><span>&and;</span><span>(</span><span>&not;</span><span>q</span><span>)</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>(</span><span>p</span><span>&rarr;</span><span>q</span><span>)</span><span>&and;</span><span>(</span><span>&not;</span><span>q</span><span>)</span></span></span></span></span></span></span>.<br>\n<blockquote>\n<span><span><span>&#8942;</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>&#8942;</span></span></span></span></span></span></span><br>\nTherefore <span><span><span>(</span><span>&not;</span><span>p</span><span>)</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>(</span><span>&not;</span><span>p</span><span>)</span></span></span></span></span></span></span>.</blockquote>\nTherefore <span><span><span>(</span><span>(</span><span>p</span><span>&rarr;</span><span>q</span><span>)</span><span>&and;</span><span>(</span><span>&not;</span><span>q</span><span>)</span><span>)</span><span>&rarr;</span><span>(</span><span>&not;</span><span>p</span><span>)</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>(</span><span>(</span><span>p</span><span>&rarr;</span><span>q</span><span>)</span><span>&and;</span><span>(</span><span>&not;</span><span>q</span><span>)</span><span>)</span><span>&rarr;</span><span>(</span><span>&not;</span><span>p</span><span>)</span></span></span></span></span></span></span>.</blockquote>\n<p>The</p>\n<span><span><span>&#8942;</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>&#8942;</span></span></span></span></span></span></span>\n<p>represents the part of the proof that we haven't finished yet. The table told use to assume</p>\n<span><span><span>P</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>P</span></span></span></span></span></span></span>\n<p>, meaning that we should assume the first sub-tree under the implication, which in this case was</p>\n<span><span><span>(</span><span>(</span><span>p</span><span>&rarr;</span><span>q</span><span>)</span><span>&and;</span><span>(</span><span>&not;</span><span>q</span><span>)</span><span>)</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>(</span><span>(</span><span>p</span><span>&rarr;</span><span>q</span><span>)</span><span>&and;</span><span>(</span><span>&not;</span><span>q</span><span>)</span><span>)</span></span></span></span></span></span></span>\n<p>. We need to prove</p>\n<span><span><span>Q</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>Q</span></span></span></span></span></span></span>\n<p>, the second sub-tree, which in this case is</p>\n<span><span><span>(</span><span>&not;</span><span>p</span><span>)</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>(</span><span>&not;</span><span>p</span><span>)</span></span></span></span></span></span></span>\n<p>.</p>\n<p>At this point we need to prove <span><span><span>(</span><span>&not;</span><span>p</span><span>)</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>(</span><span>&not;</span><span>p</span><span>)</span></span></span></span></span></span></span>, so we repeat the above process. The main connective is <span><span><span>&not;</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>&not;</span></span></span></span></span></span></span>, so rule 1 of the prove-it table tells us to assume <span><span><span>p</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>p</span></span></span></span></span></span></span> and prove <span><span><span><span>F</span><span>a</span><span>l</span><span>s</span><span>e</span></span></span></span><span tabindex=\"0\"><span><span><span><span><span><span><span><span>F</span><span>a</span><span>l</span><span>s</span><span>e</span></span></span></span></span></span></span></span></span>.</p>\n<blockquote>Assume <span><span><span>(</span><span>(</span><span>p</span><span>&rarr;</span><span>q</span><span>)</span><span>&and;</span><span>(</span><span>&not;</span><span>q</span><span>)</span><span>)</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>(</span><span>(</span><span>p</span><span>&rarr;</span><span>q</span><span>)</span><span>&and;</span><span>(</span><span>&not;</span><span>q</span><span>)</span><span>)</span></span></span></span></span></span></span>.<br>\n<blockquote>Assume <span><span><span>p</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>p</span></span></span></span></span></span></span>.\n<blockquote>\n<span><span><span>&#8942;</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>&#8942;</span></span></span></span></span></span></span><br>\nTherefore <span><span><span><span>F</span><span>a</span><span>l</span><span>s</span><span>e</span></span></span></span><span tabindex=\"0\"><span><span><span><span><span><span><span><span>F</span><span>a</span><span>l</span><span>s</span><span>e</span></span></span></span></span></span></span></span></span>.</blockquote>\nTherefore <span><span><span>(</span><span>&not;</span><span>p</span><span>)</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>(</span><span>&not;</span><span>p</span><span>)</span></span></span></span></span></span></span>.</blockquote>\nTherefore <span><span><span>(</span><span>(</span><span>p</span><span>&rarr;</span><span>q</span><span>)</span><span>&and;</span><span>(</span><span>&not;</span><span>q</span><span>)</span><span>)</span><span>&rarr;</span><span>(</span><span>&not;</span><span>p</span><span>)</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>(</span><span>(</span><span>p</span><span>&rarr;</span><span>q</span><span>)</span><span>&and;</span><span>(</span><span>&not;</span><span>q</span><span>)</span><span>)</span><span>&rarr;</span><span>(</span><span>&not;</span><span>p</span><span>)</span></span></span></span></span></span></span>.</blockquote>\n<p>At this point we're a bit stuck, there are no more main connectives to find in the simple formula</p>\n<span><span><span><span>F</span><span>a</span><span>l</span><span>s</span><span>e</span></span></span></span><span tabindex=\"0\"><span><span><span><span><span><span><span><span>F</span><span>a</span><span>l</span><span>s</span><span>e</span></span></span></span></span></span></span></span></span>\n<p>. But that's ok, we have lots of assumptions to use!</p>\n<p>Aside: the fancy name for a prove-it rule is an <i>introduction rule</i>.</p>\n<h3>Use It!</h3>\n<p>Using assumptions and previously-proven facts is a lot like proving formulas: find the main connective and then do a table look-up. The only difference is that we use a different table, shown below, which we call the use-it table.</p>\n<ol>\n<li>From <span><span><span>&not;</span><span>P</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>&not;</span><span>P</span></span></span></span></span></span></span> and <span><span><span>P</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>P</span></span></span></span></span></span></span>: have <span><span><span>Q</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>Q</span></span></span></span></span></span></span>. (You get to choose any formula!)</li>\n<li>From <span><span><span>P</span><span>&and;</span><span>Q</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>P</span><span>&and;</span><span>Q</span></span></span></span></span></span></span>: have <span><span><span>P</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>P</span></span></span></span></span></span></span>.</li>\n<li>From <span><span><span>P</span><span>&and;</span><span>Q</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>P</span><span>&and;</span><span>Q</span></span></span></span></span></span></span>: have <span><span><span>Q</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>Q</span></span></span></span></span></span></span>.</li>\n<li>From <span><span><span>P</span><span>&or;</span><span>Q</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>P</span><span>&or;</span><span>Q</span></span></span></span></span></span></span>, <span><span><span>P</span><span>&rarr;</span><span>R</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>P</span><span>&rarr;</span><span>R</span></span></span></span></span></span></span>, and <span><span><span>Q</span><span>&rarr;</span><span>R</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>Q</span><span>&rarr;</span><span>R</span></span></span></span></span></span></span>: have <span><span><span>R</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>R</span></span></span></span></span></span></span>.</li>\n<li>From <span><span><span>P</span><span>&rarr;</span><span>Q</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>P</span><span>&rarr;</span><span>Q</span></span></span></span></span></span></span> and <span><span><span>P</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>P</span></span></span></span></span></span></span>: have <span><span><span>Q</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>Q</span></span></span></span></span></span></span>.</li>\n</ol>\n<p>We have the assumption <span><span><span>(</span><span>(</span><span>p</span><span>&rarr;</span><span>q</span><span>)</span><span>&and;</span><span>(</span><span>&not;</span><span>q</span><span>)</span><span>)</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>(</span><span>(</span><span>p</span><span>&rarr;</span><span>q</span><span>)</span><span>&and;</span><span>(</span><span>&not;</span><span>q</span><span>)</span><span>)</span></span></span></span></span></span></span>, whose main connective is <span><span><span>&and;</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>&and;</span></span></span></span></span></span></span>, so we apply the use-it rules 2 and 3.</p>\n<blockquote>Assume <span><span><span>(</span><span>(</span><span>p</span><span>&rarr;</span><span>q</span><span>)</span><span>&and;</span><span>(</span><span>&not;</span><span>q</span><span>)</span><span>)</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>(</span><span>(</span><span>p</span><span>&rarr;</span><span>q</span><span>)</span><span>&and;</span><span>(</span><span>&not;</span><span>q</span><span>)</span><span>)</span></span></span></span></span></span></span>.<br>\n<blockquote>Have <span><span><span>p</span><span>&rarr;</span><span>q</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>p</span><span>&rarr;</span><span>q</span></span></span></span></span></span></span>.<br>\nHave <span><span><span>&not;</span><span>q</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>&not;</span><span>q</span></span></span></span></span></span></span>.<br>\nAssume <span><span><span>p</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>p</span></span></span></span></span></span></span>.\n<blockquote>\n<span><span><span>&#8942;</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>&#8942;</span></span></span></span></span></span></span><br>\nTherefore <span><span><span><span>F</span><span>a</span><span>l</span><span>s</span><span>e</span></span></span></span><span tabindex=\"0\"><span><span><span><span><span><span><span><span>F</span><span>a</span><span>l</span><span>s</span><span>e</span></span></span></span></span></span></span></span></span>.</blockquote>\nTherefore <span><span><span>(</span><span>&not;</span><span>p</span><span>)</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>(</span><span>&not;</span><span>p</span><span>)</span></span></span></span></span></span></span>.</blockquote>\nTherefore <span><span><span>(</span><span>(</span><span>p</span><span>&rarr;</span><span>q</span><span>)</span><span>&and;</span><span>(</span><span>&not;</span><span>q</span><span>)</span><span>)</span><span>&rarr;</span><span>(</span><span>&not;</span><span>p</span><span>)</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>(</span><span>(</span><span>p</span><span>&rarr;</span><span>q</span><span>)</span><span>&and;</span><span>(</span><span>&not;</span><span>q</span><span>)</span><span>)</span><span>&rarr;</span><span>(</span><span>&not;</span><span>p</span><span>)</span></span></span></span></span></span></span>.</blockquote>\n<p>Next we apply use-it rule 5 with</p>\n<span><span><span>p</span><span>&rarr;</span><span>q</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>p</span><span>&rarr;</span><span>q</span></span></span></span></span></span></span>\n<p>and</p>\n<span><span><span>p</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>p</span></span></span></span></span></span></span>\n<p>to deduce</p>\n<span><span><span>q</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>q</span></span></span></span></span></span></span>\n<p>. (The fancy name for use-it rule 5 is</p>\n<i>modus ponens</i>\n<p>.)</p>\n<blockquote>Assume <span><span><span>(</span><span>(</span><span>p</span><span>&rarr;</span><span>q</span><span>)</span><span>&and;</span><span>(</span><span>&not;</span><span>q</span><span>)</span><span>)</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>(</span><span>(</span><span>p</span><span>&rarr;</span><span>q</span><span>)</span><span>&and;</span><span>(</span><span>&not;</span><span>q</span><span>)</span><span>)</span></span></span></span></span></span></span>.<br>\n<blockquote>Have <span><span><span>p</span><span>&rarr;</span><span>q</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>p</span><span>&rarr;</span><span>q</span></span></span></span></span></span></span>.<br>\nHave <span><span><span>&not;</span><span>q</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>&not;</span><span>q</span></span></span></span></span></span></span>.<br>\nAssume <span><span><span>p</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>p</span></span></span></span></span></span></span>.\n<blockquote>Have <span><span><span>q</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>q</span></span></span></span></span></span></span>.<br>\n<span><span><span>&#8942;</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>&#8942;</span></span></span></span></span></span></span><br>\nTherefore <span><span><span><span>F</span><span>a</span><span>l</span><span>s</span><span>e</span></span></span></span><span tabindex=\"0\"><span><span><span><span><span><span><span><span>F</span><span>a</span><span>l</span><span>s</span><span>e</span></span></span></span></span></span></span></span></span>.</blockquote>\nTherefore <span><span><span>(</span><span>&not;</span><span>p</span><span>)</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>(</span><span>&not;</span><span>p</span><span>)</span></span></span></span></span></span></span>.</blockquote>\nTherefore <span><span><span>(</span><span>(</span><span>p</span><span>&rarr;</span><span>q</span><span>)</span><span>&and;</span><span>(</span><span>&not;</span><span>q</span><span>)</span><span>)</span><span>&rarr;</span><span>(</span><span>&not;</span><span>p</span><span>)</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>(</span><span>(</span><span>p</span><span>&rarr;</span><span>q</span><span>)</span><span>&and;</span><span>(</span><span>&not;</span><span>q</span><span>)</span><span>)</span><span>&rarr;</span><span>(</span><span>&not;</span><span>p</span><span>)</span></span></span></span></span></span></span>.</blockquote>\n<p>We now have</p>\n<span><span><span>q</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>q</span></span></span></span></span></span></span>\n<p>and</p>\n<span><span><span>&not;</span><span>q</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>&not;</span><span>q</span></span></span></span></span></span></span>\n<p>, so we can conclude anything at all. (We've reached a contradiction.) We want to prove</p>\n<span><span><span><span>F</span><span>a</span><span>l</span><span>s</span><span>e</span></span></span></span><span tabindex=\"0\"><span><span><span><span><span><span><span><span>F</span><span>a</span><span>l</span><span>s</span><span>e</span></span></span></span></span></span></span></span></span>\n<p>, so that's what we'll choose. Thus, we don't need any more steps in the proof, so we remove the vertical dots and our proof is complete.</p>\n<blockquote>Assume <span><span><span>(</span><span>(</span><span>p</span><span>&rarr;</span><span>q</span><span>)</span><span>&and;</span><span>(</span><span>&not;</span><span>q</span><span>)</span><span>)</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>(</span><span>(</span><span>p</span><span>&rarr;</span><span>q</span><span>)</span><span>&and;</span><span>(</span><span>&not;</span><span>q</span><span>)</span><span>)</span></span></span></span></span></span></span>.<br>\n<blockquote>Have <span><span><span>p</span><span>&rarr;</span><span>q</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>p</span><span>&rarr;</span><span>q</span></span></span></span></span></span></span>.<br>\nHave <span><span><span>&not;</span><span>q</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>&not;</span><span>q</span></span></span></span></span></span></span>.<br>\nAssume <span><span><span>p</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>p</span></span></span></span></span></span></span>.\n<blockquote>Have <span><span><span>q</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>q</span></span></span></span></span></span></span>.<br>\nTherefore <span><span><span><span>F</span><span>a</span><span>l</span><span>s</span><span>e</span></span></span></span><span tabindex=\"0\"><span><span><span><span><span><span><span><span>F</span><span>a</span><span>l</span><span>s</span><span>e</span></span></span></span></span></span></span></span></span>.</blockquote>\nTherefore <span><span><span>(</span><span>&not;</span><span>p</span><span>)</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>(</span><span>&not;</span><span>p</span><span>)</span></span></span></span></span></span></span>.</blockquote>\nTherefore <span><span><span>(</span><span>(</span><span>p</span><span>&rarr;</span><span>q</span><span>)</span><span>&and;</span><span>(</span><span>&not;</span><span>q</span><span>)</span><span>)</span><span>&rarr;</span><span>(</span><span>&not;</span><span>p</span><span>)</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>(</span><span>(</span><span>p</span><span>&rarr;</span><span>q</span><span>)</span><span>&and;</span><span>(</span><span>&not;</span><span>q</span><span>)</span><span>)</span><span>&rarr;</span><span>(</span><span>&not;</span><span>p</span><span>)</span></span></span></span></span></span></span>.</blockquote>\n<p>Also, the name for the formula we just proved is</p>\n<i>modus tolens</i>\n<p>.</p>\n<p>In general, the fancy name for a use-it rule is an <i>elimination rule</i>.</p>\n<h3>More Practice</h3>\n<p>In the above proof, we didn't get a chance to apply the use-it rule 4 or prove-it rule 3, so let's look at another proof. Let's prove <span><span><span>(</span><span>p</span><span>&or;</span><span>q</span><span>)</span><span>&and;</span><span>(</span><span>&not;</span><span>p</span><span>&or;</span><span>r</span><span>)</span><span>&rarr;</span><span>q</span><span>&or;</span><span>r</span></span></span></p>\n<p><span tabindex=\"0\"><span><span><span><span><span><span>(</span><span>p</span><span>&or;</span><span>q</span><span>)</span><span>&and;</span><span>(</span><span>&not;</span><span>p</span><span>&or;</span><span>r</span><span>)</span><span>&rarr;</span><span>q</span><span>&or;</span><span>r</span></span></span></span></span></span></span></p>\nSkipping a couple steps that we already know how to do, we arrive at the following partial proof.\n<blockquote>Assume <span><span><span>(</span><span>p</span><span>&or;</span><span>q</span><span>)</span><span>&and;</span><span>(</span><span>&not;</span><span>p</span><span>&or;</span><span>r</span><span>)</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>(</span><span>p</span><span>&or;</span><span>q</span><span>)</span><span>&and;</span><span>(</span><span>&not;</span><span>p</span><span>&or;</span><span>r</span><span>)</span></span></span></span></span></span></span>.\n<blockquote>Have <span><span><span>p</span><span>&or;</span><span>q</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>p</span><span>&or;</span><span>q</span></span></span></span></span></span></span>.<br>\nHave <span><span><span>&not;</span><span>p</span><span>&or;</span><span>r</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>&not;</span><span>p</span><span>&or;</span><span>r</span></span></span></span></span></span></span>.<br>\n<span><span><span>&#8942;</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>&#8942;</span></span></span></span></span></span></span><br>\nTherefore <span><span><span>q</span><span>&or;</span><span>r</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>q</span><span>&or;</span><span>r</span></span></span></span></span></span></span>.</blockquote>\nTherefore <span><span><span>(</span><span>p</span><span>&or;</span><span>q</span><span>)</span><span>&and;</span><span>(</span><span>&not;</span><span>p</span><span>&or;</span><span>r</span><span>)</span><span>&rarr;</span><span>q</span><span>&or;</span><span>r</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>(</span><span>p</span><span>&or;</span><span>q</span><span>)</span><span>&and;</span><span>(</span><span>&not;</span><span>p</span><span>&or;</span><span>r</span><span>)</span><span>&rarr;</span><span>q</span><span>&or;</span><span>r</span></span></span></span></span></span></span>.</blockquote>\n<p>We have two formulas whose main connective is a logical or, so we need to apply use-it rule 4. This rule is also know as reasoning by cases. We have to choose between using fact</p>\n<span><span><span>p</span><span>&or;</span><span>q</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>p</span><span>&or;</span><span>q</span></span></span></span></span></span></span>\n<p>or the fact</p>\n<span><span><span>&not;</span><span>p</span><span>&or;</span><span>r</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>&not;</span><span>p</span><span>&or;</span><span>r</span></span></span></span></span></span></span>\n<p>. Sometimes choices like this matter, and you might end up wasting time by making the wrong choice, but that's water under the bridge and you can always backtrack and try the other option. Also, as you gain in skill you'll be able to look a bit into the future, like a good chess player, and figure out which choice is better. Sometimes a choice like this doesn't matter because you're going to end up using both assumptions and it doesn't matter what order to use them in.</p>\n<p>Here we're going to use the first fact first, <span><span><span>p</span><span>&or;</span><span>q</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>p</span><span>&or;</span><span>q</span></span></span></span></span></span></span>. Now, to apply use-it rule 4 to this assumption, we need two more things that we don't have. We need <span><span><span>p</span><span>&rarr;</span><span>R</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>p</span><span>&rarr;</span><span>R</span></span></span></span></span></span></span> and <span><span><span>q</span><span>&rarr;</span><span>R</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>q</span><span>&rarr;</span><span>R</span></span></span></span></span></span></span>. We get to choose what <span><span><span>R</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>R</span></span></span></span></span></span></span> stands for. Once we've applied rule 4, we'll know this <span><span><span>R</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>R</span></span></span></span></span></span></span> is true, so let's choose what we're trying to prove, <span><span><span>q</span><span>&or;</span><span>r</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>q</span><span>&or;</span><span>r</span></span></span></span></span></span></span>. Our partial proof expands to the following.</p>\n<blockquote>Assume <span><span><span>(</span><span>p</span><span>&or;</span><span>q</span><span>)</span><span>&and;</span><span>(</span><span>&not;</span><span>p</span><span>&or;</span><span>r</span><span>)</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>(</span><span>p</span><span>&or;</span><span>q</span><span>)</span><span>&and;</span><span>(</span><span>&not;</span><span>p</span><span>&or;</span><span>r</span><span>)</span></span></span></span></span></span></span>.\n<blockquote>Have <span><span><span>p</span><span>&or;</span><span>q</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>p</span><span>&or;</span><span>q</span></span></span></span></span></span></span>.<br>\nHave <span><span><span>&not;</span><span>p</span><span>&or;</span><span>r</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>&not;</span><span>p</span><span>&or;</span><span>r</span></span></span></span></span></span></span>.<br>\nAssume <span><span><span>p</span></span></span><span tabindex=\"0\"><span><span><span><span><span><span>p</span></span></span></span></span></span></span>.\n<blockquote>\n<span><span><span>&#8942;</span></span></span><br>\nTherefore <span><span><span>q</span><span>&or;</span><span>r</span></span></span>.<br>\n</blockquote>\nTherefore <span><span><span>p</span><span>&rarr;</span><span>(</span><span>q</span><span>&or;</span><span>r</span><span>)</span></span></span>.<br>\nAssume <span><span><span>q</span></span></span>.\n<blockquote>\n<span><span><span>&#8942;</span></span></span><br>\nTherefore <span><span><span>q</span><span>&or;</span><span>r</span></span></span>.<br>\n</blockquote>\nTherefore <span><span><span>q</span><span>&rarr;</span><span>(</span><span>q</span><span>&or;</span><span>r</span><span>)</span></span></span>.<br>\nTherefore <span><span><span>q</span><span>&or;</span><span>r</span></span></span>.</blockquote>\nTherefore <span><span><span>(</span><span>p</span><span>&or;</span><span>q</span><span>)</span><span>&and;</span><span>(</span><span>&not;</span><span>p</span><span>&or;</span><span>r</span><span>)</span><span>&rarr;</span><span>q</span><span>&or;</span><span>r</span></span></span>.</blockquote>\n<p>The second case, in which we assume</p>\n<span><span><span>q</span></span></span>\n<p>is easy. We just apply prove-it rule 3. So we've connected those dots.</p>\n<blockquote>Assume <span><span><span>(</span><span>p</span><span>&or;</span><span>q</span><span>)</span><span>&and;</span><span>(</span><span>&not;</span><span>p</span><span>&or;</span><span>r</span><span>)</span></span></span>.\n<blockquote>Have <span><span><span>p</span><span>&or;</span><span>q</span></span></span>.<br>\nHave <span><span><span>&not;</span><span>p</span><span>&or;</span><span>r</span></span></span>.<br>\nAssume <span><span><span>p</span></span></span>.\n<blockquote>\n<span><span><span>&#8942;</span></span></span><br>\nTherefore <span><span><span>q</span><span>&or;</span><span>r</span></span></span>.<br>\n</blockquote>\nTherefore <span><span><span>p</span><span>&rarr;</span><span>(</span><span>q</span><span>&or;</span><span>r</span><span>)</span></span></span>.<br>\nAssume <span><span><span>q</span></span></span>.\n<blockquote>Therefore <span><span><span>q</span><span>&or;</span><span>r</span></span></span>.<br>\n</blockquote>\nTherefore <span><span><span>q</span><span>&rarr;</span><span>(</span><span>q</span><span>&or;</span><span>r</span><span>)</span></span></span>.<br>\nTherefore <span><span><span>q</span><span>&or;</span><span>r</span></span></span>.</blockquote>\nTherefore <span><span><span>(</span><span>p</span><span>&or;</span><span>q</span><span>)</span><span>&and;</span><span>(</span><span>&not;</span><span>p</span><span>&or;</span><span>r</span><span>)</span><span>&rarr;</span><span>q</span><span>&or;</span><span>r</span></span></span>.</blockquote>\n<p>To deal with the other set of vertical dots, the way forward is not so obvious. But we do have one more fact to use:</p>\n<span><span><span>&not;</span><span>p</span><span>&or;</span><span>r</span></span></span>\n<p>. To apply use-it rule 4, we'll need to prove a pair of implications. Again, let's choose</p>\n<span><span><span>q</span><span>&or;</span><span>r</span></span></span>\n<p>as the</p>\n<span><span><span>R</span></span></span>\n<p>.</p>\n<blockquote>Assume <span><span><span>(</span><span>p</span><span>&or;</span><span>q</span><span>)</span><span>&and;</span><span>(</span><span>&not;</span><span>p</span><span>&or;</span><span>r</span><span>)</span></span></span>.\n<blockquote>Have <span><span><span>p</span><span>&or;</span><span>q</span></span></span>.<br>\nHave <span><span><span>&not;</span><span>p</span><span>&or;</span><span>r</span></span></span>.<br>\nAssume <span><span><span>p</span></span></span>.\n<blockquote>Assume <span><span><span>&not;</span><span>p</span></span></span>.\n<blockquote>\n<span><span><span>&#8942;</span></span></span><br>\nTherefore <span><span><span>q</span><span>&or;</span><span>r</span></span></span>.</blockquote>\nTherefore <span><span><span>&not;</span><span>p</span><span>&rarr;</span><span>(</span><span>q</span><span>&or;</span><span>r</span><span>)</span></span></span>.<br>\nAssume <span><span><span>r</span></span></span>.\n<blockquote>\n<span><span><span>&#8942;</span></span></span><br>\nTherefore <span><span><span>q</span><span>&or;</span><span>r</span></span></span>.</blockquote>\nTherefore <span><span><span>&not;</span><span>p</span><span>&rarr;</span><span>(</span><span>q</span><span>&or;</span><span>r</span><span>)</span></span></span>.<br>\nTherefore <span><span><span>q</span><span>&or;</span><span>r</span></span></span>.<br>\n</blockquote>\nTherefore <span><span><span>p</span><span>&rarr;</span><span>(</span><span>q</span><span>&or;</span><span>r</span><span>)</span></span></span>.<br>\nAssume <span><span><span>q</span></span></span>.\n<blockquote>Therefore <span><span><span>q</span><span>&or;</span><span>r</span></span></span>.<br>\n</blockquote>\nTherefore <span><span><span>q</span><span>&rarr;</span><span>(</span><span>q</span><span>&or;</span><span>r</span><span>)</span></span></span>.<br>\nTherefore <span><span><span>q</span><span>&or;</span><span>r</span></span></span>.</blockquote>\nTherefore <span><span><span>(</span><span>p</span><span>&or;</span><span>q</span><span>)</span><span>&and;</span><span>(</span><span>&not;</span><span>p</span><span>&or;</span><span>r</span><span>)</span><span>&rarr;</span><span>q</span><span>&or;</span><span>r</span></span></span>.</blockquote>\n<p>The first set of dots can be eliminated by use-it rule 1 and the second set of dots can be eliminated by prove it rule 3. So our completed proof is as follows.</p>\n<blockquote>Assume <span><span><span>(</span><span>p</span><span>&or;</span><span>q</span><span>)</span><span>&and;</span><span>(</span><span>&not;</span><span>p</span><span>&or;</span><span>r</span><span>)</span></span></span>.\n<blockquote>Have <span><span><span>p</span><span>&or;</span><span>q</span></span></span>.<br>\nHave <span><span><span>&not;</span><span>p</span><span>&or;</span><span>r</span></span></span>.<br>\nAssume <span><span><span>p</span></span></span>.\n<blockquote>Assume <span><span><span>&not;</span><span>p</span></span></span>.\n<blockquote>Therefore <span><span><span>q</span><span>&or;</span><span>r</span></span></span>.</blockquote>\nTherefore <span><span><span>&not;</span><span>p</span><span>&rarr;</span><span>(</span><span>q</span><span>&or;</span><span>r</span><span>)</span></span></span>.<br>\nAssume <span><span><span>r</span></span></span>.\n<blockquote>Therefore <span><span><span>q</span><span>&or;</span><span>r</span></span></span>.</blockquote>\nTherefore <span><span><span>&not;</span><span>p</span><span>&rarr;</span><span>(</span><span>q</span><span>&or;</span><span>r</span><span>)</span></span></span>.<br>\nTherefore <span><span><span>q</span><span>&or;</span><span>r</span></span></span>.<br>\n</blockquote>\nTherefore <span><span><span>p</span><span>&rarr;</span><span>(</span><span>q</span><span>&or;</span><span>r</span><span>)</span></span></span>.<br>\nAssume <span><span><span>q</span></span></span>.\n<blockquote>Therefore <span><span><span>q</span><span>&or;</span><span>r</span></span></span>.<br>\n</blockquote>\nTherefore <span><span><span>q</span><span>&rarr;</span><span>(</span><span>q</span><span>&or;</span><span>r</span><span>)</span></span></span>.<br>\nTherefore <span><span><span>q</span><span>&or;</span><span>r</span></span></span>.</blockquote>\nTherefore <span><span><span>(</span><span>p</span><span>&or;</span><span>q</span><span>)</span><span>&and;</span><span>(</span><span>&not;</span><span>p</span><span>&or;</span><span>r</span><span>)</span><span>&rarr;</span><span>q</span><span>&or;</span><span>r</span></span></span>.</blockquote>\n<p>Aside: The formula we have just proved is known as the</p>\n<i>resolution rule</i>\n<p>.</p>\n<h3>But this doesn't look like a real proof!</h3>\n<p>If you've read one or more proofs in textbooks, you might be thinking at this point that what you've seen above doesn't look like the proofs you've seen in the past. That's because seasoned mathematicians expect that you can do proofs such as the ones above in your head, and don't write down those parts of the proofs. That is, they skip lots of steps and only write down the really important stuff. So why is it a good idea to start by writing down proofs such as the ones above? It's great practice! It's the only way I know that you'll gain enough experience that you'll be able do these simple proofs in your head with confidence.</p>\n<h3>Conclusion</h3>\n<p>The basics of proof is simple. Look at what you need to prove, find the main connective, and find what to do in the prove-it table. Repeat until you run into a dead end. Then look at what you know (assumptions and facts you've already proved), find the main connectives in those formulas, and apply the use-it rules. Hopefully that let's you connect all the dots! Happy propositional proving.</p>\n</div>\n</div>\n<br>\n<br>\n<br>\n<br>\nGuru<br>\n<br>\nvia siek.blogspot.com https://ift.tt/1GndmOw<br>\n<br>\nDecember 18, 2018 at 04:52PM"}}
{"actor":{"display_login":"guevara"}}