50 lines
No EOL
13 KiB
HTML
50 lines
No EOL
13 KiB
HTML
<!DOCTYPE html><html><head><meta content="text/html; charset=utf-8" http-equiv="Content-Type" /><meta content="width=device-width, initial-scale=1" name="viewport" /><!--replace-start-0--><!--replace-start-5--><!--replace-start-8--><title>Disjunction Elimination - My Zettelkasten</title><!--replace-end-8--><!--replace-end-5--><!--replace-end-0--><link href="https://cdn.jsdelivr.net/npm/fomantic-ui@2.8.7/dist/semantic.min.css" rel="stylesheet" /><link href="https://fonts.googleapis.com/css?family=Merriweather|Libre+Franklin|Roboto+Mono&display=swap" rel="stylesheet" /><!--replace-start-1--><!--replace-start-4--><!--replace-start-7--><link href="https://raw.githubusercontent.com/srid/neuron/master/assets/neuron.svg" rel="icon" /><meta content="This rule is sometimes also referred to as Constructive Dilemma. This can be a bit tricky to understand because the goal is to derive or introduce a new proposition separate from the disjunction you start out with. This may be disjunction, a single proposition or a proposition containing any other l" name="description" /><meta content="Disjunction Elimination" property="og:title" /><meta content="My Zettelkasten" property="og:site_name" /><meta content="article" property="og:type" /><meta content="Disjunction_Elimination" property="neuron:zettel-id" /><meta content="Disjunction_Elimination" property="neuron:zettel-slug" /><meta content="logic" property="neuron:zettel-tag" /><meta content="propositional-logic" property="neuron:zettel-tag" /><script type="application/ld+json">[]</script><style type="text/css">body{background-color:#eeeeee !important;font-family:"Libre Franklin", serif !important}body .ui.container{font-family:"Libre Franklin", serif !important}body h1, h2, h3, h4, h5, h6, .ui.header, .headerFont{font-family:"Merriweather", sans-serif !important}body code, pre, tt, .monoFont{font-family:"Roboto Mono","SFMono-Regular","Menlo","Monaco","Consolas","Liberation Mono","Courier New", monospace !important}body div.z-index p.info{color:#808080}body div.z-index ul{list-style-type:square;padding-left:1.5em}body div.z-index .uplinks{margin-left:0.29999em}body .zettel-content h1#title-h1{background-color:rgba(33,133,208,0.1)}body nav.bottomPane{background-color:rgba(33,133,208,2.0e-2)}body div#footnotes{border-top-color:#2185d0}body p{line-height:150%}body img{max-width:100%}body .deemphasized{font-size:0.94999em}body .deemphasized:hover{opacity:1}body .deemphasized:not(:hover){opacity:0.69999}body .deemphasized:not(:hover) a{color:#808080 !important}body div.container.universe{padding-top:1em}body div.zettel-view ul{padding-left:1.5em;list-style-type:square}body div.zettel-view .pandoc .highlight{background-color:#ffff00}body div.zettel-view .pandoc .ui.disabled.fitted.checkbox{margin-right:0.29999em;vertical-align:middle}body div.zettel-view .zettel-content .metadata{margin-top:1em}body div.zettel-view .zettel-content .metadata div.date{text-align:center;color:#808080}body div.zettel-view .zettel-content h1{padding-top:0.2em;padding-bottom:0.2em;text-align:center}body div.zettel-view .zettel-content h2{border-bottom:solid 1px #4682b4;margin-bottom:0.5em}body div.zettel-view .zettel-content h3{margin:0px 0px 0.4em 0px}body div.zettel-view .zettel-content h4{opacity:0.8}body div.zettel-view .zettel-content div#footnotes{margin-top:4em;border-top-style:groove;border-top-width:2px;font-size:0.9em}body div.zettel-view .zettel-content div#footnotes ol > li > p:only-of-type{display:inline;margin-right:0.5em}body div.zettel-view .zettel-content aside.footnote-inline{width:30%;padding-left:15px;margin-left:15px;float:right;background-color:#d3d3d3}body div.zettel-view .zettel-content .overflows{overflow:auto}body div.zettel-view .zettel-content code{margin:auto auto auto auto;font-size:100%}body div.zettel-view .zettel-content p code, li code, ol code{padding:0.2em 0.2em 0.2em 0.2em;background-color:#f5f2f0}body div.zettel-view .zettel-content pre{overflow:auto}body div.zettel-view .zettel-content dl dt{font-weight:bold}body div.zettel-view .zettel-content blockquote{background-color:#f9f9f9;border-left:solid 10px #cccccc;margin:1.5em 0px 1.5em 0px;padding:0.5em 10px 0.5em 10px}body div.zettel-view .zettel-content.raw{background-color:#dddddd}body .ui.label.zettel-tag{color:#000000}body .ui.label.zettel-tag a{color:#000000}body nav.bottomPane ul.backlinks > li{padding-bottom:0.4em;list-style-type:disc}body nav.bottomPane ul.context-list > li{list-style-type:lower-roman}body .footer-version img{-webkit-filter:grayscale(100%);-moz-filter:grayscale(100%);-ms-filter:grayscale(100%);-o-filter:grayscale(100%);filter:grayscale(100%)}body .footer-version img:hover{-webkit-filter:grayscale(0%);-moz-filter:grayscale(0%);-ms-filter:grayscale(0%);-o-filter:grayscale(0%);filter:grayscale(0%)}body .footer-version, .footer-version a, .footer-version a:visited{color:#808080}body .footer-version a{font-weight:bold}body .footer-version{margin-top:1em !important;font-size:0.69999em}@media only screen and (max-width: 768px){body div#zettel-container{margin-left:0.4em !important;margin-right:0.4em !important}}body span.zettel-link-container span.zettel-link a{color:#2185d0;font-weight:bold;text-decoration:none}body span.zettel-link-container span.zettel-link a:hover{background-color:rgba(33,133,208,0.1)}body span.zettel-link-container span.extra{color:auto}body span.zettel-link-container.errors{border:solid 1px #ff0000}body span.zettel-link-container.errors span.zettel-link a:hover{text-decoration:none !important;cursor:not-allowed}body [data-tooltip]:after{font-size:0.69999em}body div.tag-tree div.node{font-weight:bold}body div.tag-tree div.node a.inactive{color:#555555}body .tree.flipped{-webkit-transform:rotate(180deg);-moz-transform:rotate(180deg);-ms-transform:rotate(180deg);-o-transform:rotate(180deg);transform:rotate(180deg)}body .tree{overflow:auto}body .tree ul.root{padding-top:0px;margin-top:0px}body .tree ul{position:relative;padding:1em 0px 0px 0px;white-space:nowrap;margin:0px auto 0px auto;text-align:center}body .tree ul::after{content:"";display:table;clear:both}body .tree ul:last-child{padding-bottom:0.1em}body .tree li{display:inline-block;vertical-align:top;text-align:center;list-style-type:none;position:relative;padding:1em 0.5em 0em 0.5em}body .tree li::before{content:"";position:absolute;top:0px;right:50%;border-top:solid 2px #cccccc;width:50%;height:1.19999em}body .tree li::after{content:"";position:absolute;top:0px;right:50%;border-top:solid 2px #cccccc;width:50%;height:1.19999em}body .tree li::after{right:auto;left:50%;border-left:solid 2px #cccccc}body .tree li:only-child{padding-top:0em}body .tree li:only-child::after{display:none}body .tree li:only-child::before{display:none}body .tree li:first-child::before{border-style:none;border-width:0px}body .tree li:first-child::after{border-radius:5px 0px 0px 0px}body .tree li:last-child::after{border-style:none;border-width:0px}body .tree li:last-child::before{border-right:solid 2px #cccccc;border-radius:0px 5px 0px 0px}body .tree ul ul::before{content:"";position:absolute;top:0px;left:50%;border-left:solid 2px #cccccc;width:0px;height:1.19999em}body .tree li div.forest-link{border:solid 2px #cccccc;padding:0.2em 0.29999em 0.2em 0.29999em;text-decoration:none;display:inline-block;border-radius:5px 5px 5px 5px;color:#333333;position:relative;top:2px}body .tree.flipped li div.forest-link{-webkit-transform:rotate(180deg);-moz-transform:rotate(180deg);-ms-transform:rotate(180deg);-o-transform:rotate(180deg);transform:rotate(180deg)}</style><script
|
|
async=""
|
|
id="MathJax-script"
|
|
src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"
|
|
></script>
|
|
<link
|
|
href="https://cdnjs.cloudflare.com/ajax/libs/prism/1.23.0/themes/prism.min.css"
|
|
rel="stylesheet"
|
|
/><link rel="preconnect" href="https://fonts.googleapis.com" /><link
|
|
rel="preconnect"
|
|
href="https://fonts.gstatic.com"
|
|
crossorigin
|
|
/><link
|
|
href="https://fonts.googleapis.com/css2?family=IBM+Plex+Mono:ital,wght@0,100;0,200;0,300;0,400;0,500;0,600;0,700;1,100;1,200;1,300;1,400;1,500;1,600;1,700&family=IBM+Plex+Sans+Condensed:ital,wght@0,100;0,200;0,300;0,400;0,500;0,600;0,700;1,100;1,200;1,300;1,400;1,500;1,600;1,700&family=IBM+Plex+Sans:ital,wght@0,100;0,200;0,300;0,400;0,500;0,600;0,700;1,100;1,200;1,300;1,400;1,500;1,600;1,700&family=IBM+Plex+Serif:ital,wght@0,100;0,200;0,300;0,400;0,500;0,600;0,700;1,100;1,200;1,300;1,400;1,500;1,600;1,700&display=swap"
|
|
rel="stylesheet"
|
|
/>
|
|
<script src="https://cdnjs.cloudflare.com/ajax/libs/prism/1.23.0/components/prism-core.min.js"></script>
|
|
<script src="https://cdnjs.cloudflare.com/ajax/libs/prism/1.23.0/plugins/autoloader/prism-autoloader.min.js"></script>
|
|
<style>
|
|
body .ui.container,
|
|
body ul {
|
|
font-family: "IBM Plex Sans" !important;
|
|
}
|
|
body blockquote {
|
|
border-left-width: 3px !important;
|
|
font-style: italic;
|
|
}
|
|
.headerFont,
|
|
.ui.header,
|
|
body h1,
|
|
h2,
|
|
h3,
|
|
h4,
|
|
h5,
|
|
h6 {
|
|
font-family: "IBM Plex Sans Condensed" !important;
|
|
}
|
|
body p {
|
|
line-height: 1.4;
|
|
}
|
|
.monoFont,
|
|
body code,
|
|
pre,
|
|
tt {
|
|
font-family: "IBM Plex Mono" !important;
|
|
font-size: 12px !important;
|
|
line-height: 1.4 !important;
|
|
}
|
|
</style>
|
|
<!--replace-end-7--><!--replace-end-4--><!--replace-end-1--></head><body><div class="ui fluid container universe"><!--replace-start-2--><!--replace-start-3--><!--replace-start-6--><div class="ui text container" id="zettel-container" style="position: relative"><div class="zettel-view"><article class="ui raised attached segment zettel-content"><div class="pandoc"><h1 id="title-h1">Disjunction Elimination</h1><p>This rule is sometimes also referred to as <em>Constructive Dilemma</em>. This can be a bit tricky to understand because the goal is to derive or <em>introduce</em> a new proposition separate from the disjunction you start out with. This may be disjunction, a single proposition or a proposition containing any other logical connective. You do this by constructing two sub-proofs, one for each of the disjuncts comprising the disjunction you start out with. If you can derive your target proposition as the conclusion of each subproof then you may invoke the conclusion in the main proof and take it to be derived.</p><p><img src="/static/disjunc-elim.png" /></p><p><em>Here is an example where Disjunction Elimination is used to derive a new disjunction.</em></p><p><img src="/static/proofs-drawio-Page-6.drawio.png" /></p><p><em>Here are two further examples that use Disjunction Elimination to derive singular propositions</em></p><p><img src="/static/ORelim1.png" /> <img src="/static/ORelim2.png" /></p></div></article><nav class="ui attached segment deemphasized backlinksPane" id="neuron-backlinks-pane"><h3 class="ui header">Backlinks</h3><ul class="backlinks"><li><span class="zettel-link-container cf"><span class="zettel-link"><a href="Strategies_for_constructing_proofs.html">Strategies for constructing proofs in propositional logic</a></span></span><ul class="context-list" style="zoom: 85%;"><li class="item"><div class="pandoc"><p>Our starting assumption is to a disjunction. Thus we can apply <span class="zettel-link-container cf"><span class="zettel-link" title="Zettel: Disjunction Elimination"><a href="Disjunction_Elimination.html">Disjunction Elimination</a></span></span> to show that our goal sentence <span class="math inline">\(\lnot(A \land B)\)</span> follows from each of the disjuncts (<span class="math inline">\(\lnot A\)</span> and <span class="math inline">\(\lnot B\)</span>) in dedicated sub-proofs. If we can do this, we have the right to derive <span class="math inline">\(\lnot (A \land B)\)</span>.</p></div></li><li class="item"><div class="pandoc"><p>Having done this, we can discharge the <span class="zettel-link-container cf"><span class="zettel-link" title="Zettel: Disjunction Elimination"><a href="Disjunction_Elimination.html">Disjunction Elimination</a></span></span> sub-proofs and derive <span class="math inline">\(\lnot (A \land B)\)</span> from <span class="math inline">\(\lnot A \lor \lnot B\)</span></p></div></li></ul></li><li><span class="zettel-link-container cf"><span class="zettel-link"><a href="Formal_proofs_in_propositional_logic.html">Formal proofs in propositional logic</a></span></span><ul class="context-list" style="zoom: 85%;"><li class="item"><div class="pandoc"><span class="zettel-link-container cf"><span class="zettel-link" title="Zettel: Disjunction Elimination"><a href="Disjunction_Elimination.html">Disjunction Elimination</a></span></span></div></li><li class="item"><div class="pandoc"><span class="zettel-link-container cf"><span class="zettel-link" title="Zettel: Disjunction Elimination"><a href="Disjunction_Elimination.html">Disjunction Elimination</a></span></span></div></li></ul></li></ul></nav><nav class="ui attached segment deemphasized bottomPane" id="neuron-tags-pane"><div><span class="ui basic label zettel-tag" title="Tag">logic</span><span class="ui basic label zettel-tag" title="Tag">propositional-logic</span></div></nav><nav class="ui bottom attached icon compact inverted menu blue" id="neuron-nav-bar"><!--replace-start-9--><!--replace-end-9--><a class="right item" href="impulse.html" title="Open Impulse"><i class="wave square icon"></i></a></nav></div></div><!--replace-end-6--><!--replace-end-3--><!--replace-end-2--><div class="ui center aligned container footer-version"><div class="ui tiny image"><a href="https://neuron.zettel.page"><img alt="logo" src="https://raw.githubusercontent.com/srid/neuron/master/assets/neuron.svg" title="Generated by Neuron 1.9.35.3" /></a></div></div></div></body></html> |