Newest questions tagged proof-golf - Code Golf Stack Exchange most recent 30 from codegolf.stackexchange.com 2019-11-15T05:23:54Z https://codegolf.stackexchange.com/feeds/tag?tagnames=proof-golf&sort=newest https://creativecommons.org/licenses/by-sa/4.0/rdf https://codegolf.stackexchange.com/q/168528 21 Existential Golf Wheat Wizard https://codegolf.stackexchange.com/users/56656 2018-07-13T16:39:34Z 2018-07-14T01:59:56Z <p>Math has a lot of symbols. Some might say too many symbols. So lets do some math with pictures.</p> <p>Lets have a paper, which we will draw on. To start the paper is empty, we will say that is equivalent to \$\top\$ or \$\textit{true}\$.</p> <p>If we write other things on the paper they will also be true.</p> <p>For example</p> <p><a href="https://i.stack.imgur.com/d6UrV.png" rel="noreferrer"><img src="https://i.stack.imgur.com/d6UrV.png" alt="P and Q"></a></p> <p>Indicates that the claims \$P\$ and \$Q\$ are true.</p> <p>Now let us say that if we draw a circle around some statement that statement is false. This represents logical not.</p> <p>For example:</p> <p><a href="https://i.stack.imgur.com/D3EmF.png" rel="noreferrer"><img src="https://i.stack.imgur.com/D3EmF.png" alt="not P and Q"></a></p> <p>Indicates that \$P\$ is false and \$Q\$ is true.</p> <p>We can even place the circle around multiple sub-statements:</p> <p><a href="https://i.stack.imgur.com/F7RgN.png" rel="noreferrer"><img src="https://i.stack.imgur.com/F7RgN.png" alt="not (P and Q)"></a></p> <p>Since the part inside the circle normally reads as \$P\text{ and }Q\$ by putting a circle around it it means \$\text{not }(P\text{ and }Q)\$. We can even nest circles</p> <p><a href="https://i.stack.imgur.com/Cct9N.png" rel="noreferrer"><img src="https://i.stack.imgur.com/Cct9N.png" alt="not (not P and Q)"></a></p> <p>This reads as \$\text{not }((\text{not }P)\text{ and }Q)\$.</p> <p>If we draw a circle with nothing in it, that represents \$\bot\$ or \$\textit{false}\$. </p> <p><a href="https://i.stack.imgur.com/9YRJ1.png" rel="noreferrer"><img src="https://i.stack.imgur.com/9YRJ1.png" alt="False"></a></p> <p>Since empty space was true, then the negation of true is false.</p> <p>Now using this simple visual method we can actually represent any statement in propositional logic.</p> <h1>Proofs</h1> <p>The next step after being able to represent statements is being able to prove them. For proofs we have 4 different rules that can be used to transform a graph. We always start with an empty sheet which as we know is a vacuous truth and then use these different rules to transform our empty sheet of paper into a theorem.</p> <p>Our first inference rule is <em>Insertion</em>.</p> <h3>Insertion</h3> <p>We will call the number of negations between a sub-graph and the top level it's "depth". <em>Insertion</em> allows us to introduce any statement we wish at an odd depth.</p> <p>Here is an example of us performing insertion:</p> <p><a href="https://i.stack.imgur.com/NNNzs.png" rel="noreferrer"><img src="https://i.stack.imgur.com/NNNzs.png" alt="Insertion Example"></a></p> <p>Here we chose \$P\$, but we could just as well choose any statement we wanted.</p> <h3>Erasure</h3> <p>The next inference rule is <em>Erasure</em>. <em>Erasure</em> tells us that if we have a statement that is at a even depth we can remove it entirely.</p> <p>Here is an example of erasure being applied:</p> <p><a href="https://i.stack.imgur.com/xZwt3.png" rel="noreferrer"><img src="https://i.stack.imgur.com/xZwt3.png" alt="Erasure example"></a></p> <p>Here we erased the \$Q\$, because it was \$2\$ levels nested. Even if we wanted to we could not have erased \$P\$ because it is \$1\$ level nested.</p> <h3>Double Cut</h3> <p><em>Double Cut</em> is an equivalence. Which means, unlike the previous inferences it can also be reversed. <em>Double Cut</em> tells us that we can draw two circles around any sub-graph, and if there are two circles around a sub-graph we can remove them both.</p> <p>Here is an example of the <em>Double Cut</em> being used</p> <p><a href="https://i.stack.imgur.com/eouBJ.png" rel="noreferrer"><img src="https://i.stack.imgur.com/eouBJ.png" alt="Double Cut example"></a></p> <p>Here we use <em>Double Cut</em> on \$Q\$.</p> <h3>Iteration</h3> <p><em>Iteration</em> is a equivalence as well.<sup>1</sup> It's reverse is called <em>Deiteration</em> If we have a statement and a cut on the same level, we can copy that statement inside of a cut.</p> <p>For example:</p> <p><a href="https://i.stack.imgur.com/5PgO9.png" rel="noreferrer"><img src="https://i.stack.imgur.com/5PgO9.png" alt="Iteration example"></a></p> <p><em>Deiteration</em> allows us to reverse an <em>Iteration</em>. A statement can be removed via <em>Deiteration</em> if there exists a copy of it at the next level up.</p> <hr> <p>This format of representation and proof is not of my own invention. They are a minor modification of a diagrammatic logic are called <a href="https://en.wikipedia.org/wiki/Existential_graph" rel="noreferrer">Alpha Existential Graphs</a>. If you want to read more on this, there is not a ton of literature, but the linked article is a good start.</p> <hr> <h1>Task</h1> <p>Your task will be to prove the following theorem:</p> <p><a href="https://i.stack.imgur.com/d3Pyh.png" rel="noreferrer"><img src="https://i.stack.imgur.com/d3Pyh.png" alt="Łukasiewicz - Tarksi Axiom"></a></p> <p>This, when translated into traditional logic symbolization is </p> <p>\$((A\to(B\to A))\to(((\neg C\to(D\to\neg E))\to((C\to(D\to F))\to((E\to D)\to(E\to F))))\to G))\to(H\to G)\$.</p> <p>Also known as the <a href="https://en.wikipedia.org/wiki/List_of_Hilbert_systems#Implication_and_negation" rel="noreferrer">Łukasiewicz-Tarski Axiom</a>.</p> <p>It may seem involved but existential graphs are <em>very</em> efficient when it comes to proof length. I selected this theorem because I do think it is an appropriate length for a fun and challenging puzzle. If you are having trouble with this one I would recommend trying some more basic theorems first to get the hang of the system. A list of these can be found at the bottom of the post.</p> <p>This is <a href="/questions/tagged/proof-golf" class="post-tag" title="show questions tagged &#39;proof-golf&#39;" rel="tag">proof-golf</a> so your score will be the total number of steps in your proof from start to finish. The goal is to minimize your score.</p> <h1>Format</h1> <p>The format for this challenge is flexible you can submit answers in any format that is clearly readable, including hand-drawn or rendered formats. However for clarity I suggest the following simple format:</p> <ul> <li><p>We represent a cut with parentheses, whatever we are cutting is put inside of the parens. The empty cut would just be <code>()</code> for example.</p></li> <li><p>We represent atoms with just their letters.</p></li> </ul> <p>As an example here is the goal statement in this format:</p> <pre><code>(((A((B(A))))(((((C)((D((E)))))(((C((D(F))))(((E(D))((E(F))))))))(G))))((H(G)))) </code></pre> <p>This format is nice because it is both human and machine readable, so including it in your post would be nice.</p> <p>If you want some nice(ish) diagrams here is some code that converts this format to \$\LaTeX\$:</p> <p><a href="https://tio.run/##jZJRT8IwEMff9ykuC8naTAhq4sMMJvrmsz6YUGJqV0fD1pGtCGHhs89rN8YQVLa0D9f7/@5/7c15uZBpWtexFCpTWwlRBM/ayEQWMHyAF1MonXjd6QYmoLQyQMp5voYNhTCEaTAKriDlpYEBNPGZ58UFX1vatMXNLO8E3S9iBaXhYgGF5PEcF5CABBBBQO0u8lhSNOAzZnOJb4t31kgnCuHW@fKvxlSoQqSSjK7pPdON4FCmL7mjjg9/2dgbcCl98U3kBPQ42BAbIDH5EgltWg/c78z7rbVYfTWEsJNSy3dNQtflOVVXaggI6FT/XceR@Z@3wU2eXeD6zIOgV42qauBSW44/2F32OI2bd/ynMzsHvud9rtL0Vb7ZQTsZqP1Z2c5MLlaZ1EbgpJYVFtExT3Mtd0wztirlEqvyRFZGLbYu9iETpau9zIXsWXVwijbGiLet7RiTOj5ko7eMKz1ROPEFFwZaN3VN8KP0ERd5ovQb" rel="noreferrer" title="Haskell – Try It Online">Try it online!</a></p> <p>As for your actual work I recommend pencil and paper when working out. I find that text just isn't as intuitive as paper when it comes to existential graphs.</p> <h1>Example proof</h1> <p>In this example proof we will prove the following theorem:</p> <p><a href="https://i.stack.imgur.com/u1jdT.png" rel="noreferrer"><img src="https://i.stack.imgur.com/u1jdT.png" alt="Law of contra-positives"></a></p> <p>Now this may seem alien to you at first but if we translate this into traditional logic notation we get \$(A\rightarrow B)\rightarrow(\neg B\rightarrow \neg A)\$, also known as the law of contra-positives.</p> <p><strong>Proof:</strong></p> <p><a href="https://i.stack.imgur.com/lgPrY.png" rel="noreferrer"><img src="https://i.stack.imgur.com/lgPrY.png" alt="Example Proof 1"></a></p> <h1>Practice Theorems</h1> <p>Here are some simple theorems you can use to practice the system:</p> <h3>Łukasiewicz' Second Axiom</h3> <p><a href="https://i.stack.imgur.com/9eghU.png" rel="noreferrer"><img src="https://i.stack.imgur.com/9eghU.png" alt="Łukasiewicz&#39; Second Axiom"></a></p> <h3>Meredith's Axiom</h3> <p><a href="https://i.stack.imgur.com/3rpSS.png" rel="noreferrer"><img src="https://i.stack.imgur.com/3rpSS.png" alt="Meredith&#39;s Axiom"></a></p> <p><sup>1: Most sources use a more sophisticated and powerful version of <em>Iteration</em>, but to keep this challenge simple I am using this version. They are functionally equivalent.</sup></p> https://codegolf.stackexchange.com/q/161172 38 (A → B) → (¬B → ¬A) Wheat Wizard https://codegolf.stackexchange.com/users/56656 2018-04-03T15:31:51Z 2019-02-12T03:57:13Z <p>Well I think it is about time we have another <a href="/questions/tagged/proof-golf" class="post-tag" title="show questions tagged &#39;proof-golf&#39;" rel="tag">proof-golf</a> question.</p> <p>This time we are going to prove the well known logical truth</p> <p><span class="math-container">\$(A \rightarrow B) \rightarrow (\neg B \rightarrow \neg A)\$</span></p> <p>To do this we will use Łukasiewicz's third <a href="https://en.wikipedia.org/wiki/Axiom_schema" rel="nofollow noreferrer">Axiom Schema</a>, an incredibly elegant set of three axioms that are complete over <a href="https://en.wikipedia.org/wiki/Propositional_calculus#Example_1._Simple_axiom_system" rel="nofollow noreferrer">propositional logic</a>.</p> <p>Here is how it works:</p> <h1>Axioms</h1> <p>The Łukasiewicz system has three axioms. They are:</p> <p><span class="math-container">\$\phi\rightarrow(\psi\rightarrow\phi)\$</span></p> <p><span class="math-container">\$(\phi\rightarrow(\psi\rightarrow\chi))\rightarrow((\phi\rightarrow\psi)\rightarrow(\phi\rightarrow\chi))\$</span></p> <p><span class="math-container">\$(\neg\phi\rightarrow\neg\psi)\rightarrow(\psi\rightarrow\phi)\$</span></p> <p>The axioms are universal truths regardless of what we choose for <span class="math-container">\$\phi\$</span>, <span class="math-container">\$\psi\$</span> and <span class="math-container">\$\chi\$</span>. At any point in the proof we can introduce one of these axioms. When we introduce an axiom you replace each case of <span class="math-container">\$\phi\$</span>, <span class="math-container">\$\psi\$</span> and <span class="math-container">\$\chi\$</span>, with a "complex expression". A complex expression is any expression made from Atoms, (represented by the letters <span class="math-container">\$A\$</span>-<span class="math-container">\$Z\$</span>), and the operators implies (<span class="math-container">\$\rightarrow\$</span>) and not (<span class="math-container">\$\neg\$</span>).</p> <p>For example if I wanted to introduce the first axiom (L.S.1) I could introduce</p> <p><span class="math-container">\$A\rightarrow(B\rightarrow A)\$</span></p> <p>or</p> <p><span class="math-container">\$(A\rightarrow A)\rightarrow(\neg D\rightarrow(A\rightarrow A))\$</span></p> <p>In the first case <span class="math-container">\$\phi\$</span> was <span class="math-container">\$A\$</span> and <span class="math-container">\$\psi\$</span> was <span class="math-container">\$B\$</span>, while in the second case both were more involved expressions. <span class="math-container">\$\phi\$</span> was <span class="math-container">\$(A\rightarrow A)\$</span> and <span class="math-container">\$\psi\$</span> was <span class="math-container">\$\neg D\$</span>.</p> <p>What substitutions you choose to use will be dependent on what you need in the proof at the moment.</p> <h2>Modus Ponens</h2> <p>Now that we can introduce statements we need to relate them together to make new statements. The way that this is done in Łukasiewicz's Axiom Schema (L.S) is with Modus Ponens. Modus Ponens allows us to take two statements of the form</p> <p><span class="math-container">\$\phi\$</span></p> <p><span class="math-container">\$\phi\rightarrow \psi\$</span></p> <p>and instantiate a new statement</p> <p><span class="math-container">\$\psi\$</span></p> <p>Just like with our Axioms <span class="math-container">\$\phi\$</span> and <span class="math-container">\$\psi\$</span> can stand in for any arbitrary statement.</p> <p>The two statements can be anywhere in the proof, they don't have to be next to each other or any special order.</p> <h2>Task</h2> <p>Your task will be to prove <a href="https://en.wikipedia.org/wiki/Contraposition" rel="nofollow noreferrer">the law of contrapositives</a>. This is the statement</p> <p><span class="math-container">\$(A\rightarrow B)\rightarrow(\neg B\rightarrow\neg A)\$</span></p> <p>Now you might notice that this is rather familiar, it is an instantiation of the reverse of our third axiom </p> <p><span class="math-container">\$(\neg\phi\rightarrow\neg\psi)\rightarrow(\psi\rightarrow\phi)\$</span></p> <p>However this is no trivial feat.</p> <h2>Scoring</h2> <p>Scoring for this challenge is pretty simple, each time you instantiate an axiom counts as a point and each use of modus ponens counts as a point. This is essentially the number of lines in your proof. The goal should be to minimize your score (make it as low as possible).</p> <h2>Example Proof</h2> <p>Ok now lets use this to construct a small proof. We will prove <span class="math-container">\$A\rightarrow A\$</span>.</p> <p>Sometimes it is best to work backwards since we know where we want to be we can figure how we might get there. In this case since we want to end with <span class="math-container">\$A\rightarrow A\$</span> and this is not one of our axioms we know the last step must be modus ponens. Thus the end of our proof will look like </p> <pre><code>φ φ → (A → A) A → A M.P. </code></pre> <p><a href="https://a-ta.co/mathjax/!XGJlZ2lue2dhdGhlcip9ClxwaGlcXApccGhpXHJpZ2h0YXJyb3coQVxyaWdodGFycm93IEEpXFwKQVxyaWdodGFycm93IEEgXHRhZyp7TS5QLn1cXApcZW5ke2dhdGhlcip9.svg" rel="nofollow noreferrer">TeX</a></p> <p>Where <span class="math-container">\$\phi\$</span> is an expression we don't yet know the value of. Now we will focus on <span class="math-container">\$\phi\rightarrow(A\rightarrow A)\$</span>. This can be introduced either by modus ponens or L.S.3. L.S.3 requires us to prove <span class="math-container">\$(\neg A\rightarrow\neg A)\$</span> which seems just as hard as <span class="math-container">\$(A\rightarrow A)\$</span>, so we will go with modus ponens. So now our proof looks like</p> <pre><code>φ ψ ψ → (φ → (A → A)) φ → (A → A) M.P. A → A M.P. </code></pre> <p><a href="https://a-ta.co/mathjax/!XGJlZ2lue2dhdGhlcip9ClxwaGkgXFwKXHBzaSBcXApccHNpIFxyaWdodGFycm93IChccGhpIFxyaWdodGFycm93CihBIFxyaWdodGFycm93IEEpKVxcClxwaGkgXHJpZ2h0YXJyb3cKKEEgXHJpZ2h0YXJyb3cgQSkgXHRhZyp7TS5QLn1cXApBIFxyaWdodGFycm93IEEgXHRhZyp7TS5QLn1cXApcZW5ke2dhdGhlcip9.svg" rel="nofollow noreferrer">TeX</a></p> <p>Now <span class="math-container">\$\psi\rightarrow(\phi\rightarrow(A\rightarrow A))\$</span> looks a lot like our second axiom L.S.2 so we will fill it in as L.S.2</p> <pre><code>A → χ A → (χ → A) (A → (χ → A)) → ((A → χ) → (A → A)) L.S.2 (A → χ) → (A → A) M.P. A → A M.P. </code></pre> <p><a href="https://a-ta.co/mathjax/!XGJlZ2lue2dhdGhlcip9CihBIFxyaWdodGFycm93IFxjaGkpIFxcCihBIFxyaWdodGFycm93IChcY2hpIFxyaWdodGFycm93IEEpKSBcXAooQSBccmlnaHRhcnJvdyAoXGNoaSBccmlnaHRhcnJvdyBBKSkKXHJpZ2h0YXJyb3cgKChBIFxyaWdodGFycm93ClxjaGkpXHJpZ2h0YXJyb3cKKEEgXHJpZ2h0YXJyb3cgQSkpIFx0YWcqe0wuUy4yfVxcCihBIFxyaWdodGFycm93IFxjaGkpIFxyaWdodGFycm93CihBIFxyaWdodGFycm93IEEpIFx0YWcqe00uUC59XFwKQSBccmlnaHRhcnJvdyBBIFx0YWcqe00uUC59XFwKXGVuZHtnYXRoZXIqfQ==.svg" rel="nofollow noreferrer">TeX</a></p> <p>Now our second statement <span class="math-container">\$(A\rightarrow(\chi\rightarrow A))\$</span> can pretty clearly be constructed from L.S.1 so we will fill that in as such</p> <pre><code>A → χ A → (χ → A) L.S.1 (A → (χ → A)) → ((A → χ) → (A → A)) L.S.2 (A → χ) → (A → A) M.P. A → A M.P. </code></pre> <p><a href="https://a-ta.co/mathjax/!XGJlZ2lue2dhdGhlcip9CihBIFxyaWdodGFycm93IFxjaGkpIFxcCkEgXHJpZ2h0YXJyb3cgKFxjaGkgXHJpZ2h0YXJyb3cgQSkKXHRhZyp7TC5TLjF9XFwKKEEgXHJpZ2h0YXJyb3cgKFxjaGkgXHJpZ2h0YXJyb3cgQSkpClxyaWdodGFycm93ICgoQSBccmlnaHRhcnJvdwpcY2hpKVxyaWdodGFycm93CihBIFxyaWdodGFycm93IEEpKSBcdGFnKntMLlMuMn1cXAooQSBccmlnaHRhcnJvdyBcY2hpKSBccmlnaHRhcnJvdwooQSBccmlnaHRhcnJvdyBBKSBcdGFnKntNLlAufVxcCkEgXHJpZ2h0YXJyb3cgQSBcdGFnKntNLlAufVxcClxlbmR7Z2F0aGVyKn0=.svg" rel="nofollow noreferrer">TeX</a></p> <p>Now we just need to find a <span class="math-container">\$\chi\$</span> such that we can prove <span class="math-container">\$A\rightarrow\chi\$</span>. This can very easily be done with L.S.1 so we will try that</p> <pre><code>A → (ω → A) L.S.1 A → ((ω → A) → A) L.S.1 (A → ((ω → A) → A)) → ((A → (ω → A)) → (A → A)) L.S.2 (A → (ω → A)) → (A → A) M.P. A → A M.P. </code></pre> <p><a href="https://a-ta.co/mathjax/!XGJlZ2lue2dhdGhlcip9CihBXHJpZ2h0YXJyb3coXG9tZWdhXHJpZ2h0YXJyb3cgQSkpClxcCkFccmlnaHRhcnJvdygoXG9tZWdhXHJpZ2h0YXJyb3cgQSkKXHJpZ2h0YXJyb3cgQSlcdGFnKntMLlMuMX1cXAooQVxyaWdodGFycm93KChcb21lZ2FccmlnaHRhcnJvdyBBKQpccmlnaHRhcnJvdyBBKSlccmlnaHRhcnJvdygoQQpccmlnaHRhcnJvdyhcb21lZ2FccmlnaHRhcnJvdyBBKSkKXHJpZ2h0YXJyb3coQSBccmlnaHRhcnJvdyBBKSkKXHRhZyp7TC5TLjJ9XFwKKEFccmlnaHRhcnJvdyhcb21lZ2FccmlnaHRhcnJvdyBBKSkKXHJpZ2h0YXJyb3cKKEFccmlnaHRhcnJvdyBBKVx0YWcqe00uUC59XFwKQVxyaWdodGFycm93IEFcdGFnKntNLlAufVxcClxlbmR7Z2F0aGVyKn0=.svg" rel="nofollow noreferrer">TeX</a></p> <p>Now since all of our steps our justified we can fill in <span class="math-container">\$\omega\$</span>, as any statement we want and the proof will be valid. We could choose <span class="math-container">\$A\$</span> but I will choose <span class="math-container">\$B\$</span> so that it is clear that it doesn't need to be <span class="math-container">\$A\$</span>.</p> <pre><code>A → (B → A) L.S.1 A → ((B → A) → A) L.S.1 (A → ((B → A) → A)) → ((A → (B → A)) → (A → A)) L.S.2 (A → (B → A)) → (A → A) M.P. A → A M.P. </code></pre> <p><a href="https://a-ta.co/mathjax/!XGJlZ2lue2dhdGhlcip9CihBXHJpZ2h0YXJyb3coQlxyaWdodGFycm93IEEpKQpcdGFnKntMLlMuMX1cXApBXHJpZ2h0YXJyb3coKEJccmlnaHRhcnJvdyBBKQpccmlnaHRhcnJvdyBBKVx0YWcqe0wuUy4xfVxcCihBXHJpZ2h0YXJyb3coKEJccmlnaHRhcnJvdyBBKQpccmlnaHRhcnJvdyBBKSlccmlnaHRhcnJvdygoQQpccmlnaHRhcnJvdyhCXHJpZ2h0YXJyb3cgQSkpClxyaWdodGFycm93KEEgXHJpZ2h0YXJyb3cgQSkpClx0YWcqe0wuUy4yfVxcCihBXHJpZ2h0YXJyb3coQlxyaWdodGFycm93IEEpKQpccmlnaHRhcnJvdwooQVxyaWdodGFycm93IEEpXHRhZyp7TS5QLn1cXApBXHJpZ2h0YXJyb3cgQVx0YWcqe00uUC59XFwKXGVuZHtnYXRoZXIqfQ==.svg" rel="nofollow noreferrer">TeX</a></p> <p><a href="https://tio.run/##hVVta9swEP7uX6EZRiR2NkvzrVsLzmB0kNEy94NLElxvURqDIxtbTTay/vbszrLrl7gZAUd67nnuRbqzszxN0ien2MfHY6TTLZ/f/L1fCuY412x@s4TDr3QlQ/0nk/wGoiTbROIFSuK9cK1K8R@@a1n7wjCWbr3kNrM/2QttC9gXyFCp5oHxYzs2YlDoSMutVDpEAzLiNQ/gwVA6NiLbznVf9ICi92@IHozo83Ck1r6sMBDGQbVx2wSTt7Gbdcdcxa8K42W4CiszEHaHHnSIp1USveF3vXc8t7zWTgccorOf0SpsqPP6KvGiepag6YsA7zlYXI0/vkCXRD1hJcW4DnkIrjAlj/IKwRPYOu2sXKRedKk1ewpfhIAamJZLj7ABF5MTF3QPngD6mxo306HoVi4LHabrMImVfK2MHfDJFlfscaEeX4C1Se6pxF4oupMsj/FUCy0z7uutBh9Xgl06LNvkUSF5E5nMApivc3xSR4U0MgWWV0L7PNaSst9GWRIXmpeA8QcqgXcYbBcl8coECyA0xZtTB0oHDq1sAmDzEZv549GSJnFYenFWenFOOjkrnQxI/d40Ng6U3oz5D7m71RvwzZXjaEENewrPFS8SEqme9Ib7MBOAXBYXbPZh7FRKpLUQEp0k9v2OjUgJI/wh4836BpI8cfZNlUpGkCkXuyFN17wqtFc8MGPFgfKX2IUdLs04RanBnrk7ba8ptbro9llDUHcRbqplojhWHSXrNN/KVVPWCIeiHytsXgGE7GROfZxLjL2OE3y5p1Us241V9qxdHac23JEW8P2BTZ1lUq24QWiK4Gv8W67KPZVvJqI6BRK0zBjz0jFRXet49Bh9Kqb09IRldvW2AvkQKgzWkRvMqzbWGaMJ5P0D" rel="nofollow noreferrer" title="Prolog (SWI) - Proof Verifier">Try it online!</a></p> <p>And that is a proof.</p> <h2>Resources</h2> <h3>Verification program</h3> <p><a href="https://tio.run/##hVVta9swEP7uX6EZRiR2NkvzrVsLzmB0kNEy94NLElxvURqDIxtbTTay/vbszrLrl7gZAUd67nnuRbqzszxN0ien2MfHY6TTLZ/f/L1fCuY412x@s4TDr3QlQ/0nk/wGoiTbROIFSuK9cK1K8R@@a1n7wjCWbr3kNrM/2QttC9gXyFCp5oHxYzs2YlDoSMutVDpEAzLiNQ/gwVA6NiLbznVf9ICi92@IHozo83Ck1r6sMBDGQbVx2wSTt7Gbdcdcxa8K42W4CiszEHaHHnSIp1USveF3vXc8t7zWTgccorOf0SpsqPP6KvGiepag6YsA7zlYXI0/vkCXRD1hJcW4DnkIrjAlj/IKwRPYOu2sXKRedKk1ewpfhIAamJZLj7ABF5MTF3QPngD6mxo306HoVi4LHabrMImVfK2MHfDJFlfscaEeX4C1Se6pxF4oupMsj/FUCy0z7uutBh9Xgl06LNvkUSF5E5nMApivc3xSR4U0MgWWV0L7PNaSst9GWRIXmpeA8QcqgXcYbBcl8coECyA0xZtTB0oHDq1sAmDzEZv549GSJnFYenFWenFOOjkrnQxI/d40Ng6U3oz5D7m71RvwzZXjaEENewrPFS8SEqme9Ib7MBOAXBYXbPZh7FRKpLUQEp0k9v2OjUgJI/wh4836BpI8cfZNlUpGkCkXuyFN17wqtFc8MGPFgfKX2IUdLs04RanBnrk7ba8ptbro9llDUHcRbqplojhWHSXrNN/KVVPWCIeiHytsXgGE7GROfZxLjL2OE3y5p1Us241V9qxdHac23JEW8P2BTZ1lUq24QWiK4Gv8W67KPZVvJqI6BRK0zBjz0jFRXet49Bh9Kqb09IRldvW2AvkQKgzWkRvMqzbWGaMJ5P0D" rel="nofollow noreferrer" title="Prolog (SWI) - Proof Verifier">Here</a> is a Prolog program you can use to verify that your proof is in fact valid. Each step should be placed on its own line. <code>-&gt;</code> should be used for implies and <code>-</code> should be used for not, atoms can be represented by any string of alphabetic characters.</p> <h3>Metamath</h3> <p><a href="http://us.metamath.org" rel="nofollow noreferrer">Metamath</a> uses the Łukasiewicz system for its proofs in propositional calculus, so you may want to poke around there a bit. They also have a proof of the theorem this challenge asks for which can be found <a href="http://us.metamath.org/mpeuni/con3.html" rel="nofollow noreferrer">here</a>. There is an explanation <a href="http://us.metamath.org/mpeuni/mmset.html#proofs" rel="nofollow noreferrer">here</a> of how to read the proofs.</p> <h3>The Incredible Proof Machine</h3> <p>@<a href="https://codegolf.stackexchange.com/users/71303/antony">Antony</a> made me aware of a tool called <a href="http://incredible.pm/" rel="nofollow noreferrer">The Incredible Proof machine</a> which allows you to construct proofs in a number of systems using a nice graphical proof system. If you scroll down you will find they support the Łukasiewicz system. So if you are a more visual oriented person you can work on your proof there. Your score will be the number of blocks used minus 1.</p> https://codegolf.stackexchange.com/q/143822 122 (-a) × (-a) = a × a Wheat Wizard https://codegolf.stackexchange.com/users/56656 2017-09-26T22:25:54Z 2019-07-02T14:30:31Z <p>We all know that <span class="math-container">\$(-a) \times (-a) = a \times a\$</span> (hopefully), but can you prove it?</p> <p>Your task is to prove this fact using the ring axioms. What are the ring axioms? The ring axioms are a list of rules that two binary operations on a set have to follow. The two operation are addition, <span class="math-container">\$+\$</span>, and multiplication, <span class="math-container">\$\times\$</span>. For this challenge here are the ring axioms where <span class="math-container">\$+\$</span> and <span class="math-container">\$\times\$</span> are closed binary operations on some set <span class="math-container">\$S\$</span>, <span class="math-container">\$-\$</span> is a closed unary operation on <span class="math-container">\$S\$</span>, and <span class="math-container">\$a\$</span>, <span class="math-container">\$b\$</span>, <span class="math-container">\$c\$</span> are members of <span class="math-container">\$S\$</span>:</p> <ol> <li><p><span class="math-container">\$a + (b + c) = (a + b) + c\$</span></p></li> <li><p><span class="math-container">\$a + 0 = a\$</span></p></li> <li><p><span class="math-container">\$a + (-a) = 0\$</span></p></li> <li><p><span class="math-container">\$a + b = b + a\$</span><sup>*</sup></p></li> <li><p><span class="math-container">\$a \times (b \times c) = (a \times b) \times c\$</span></p></li> <li><p><span class="math-container">\$a \times 1 = a\$</span><sup>†</sup></p></li> <li><p><span class="math-container">\$1 × a = a\$</span><sup>†</sup></p></li> <li><p><span class="math-container">\$a \times (b + c) = (a \times b) + (a × c)\$</span> </p></li> <li><p><span class="math-container">\$(b + c) \times a = (b \times a) + (c \times a)\$</span></p></li> </ol> <p>Your proof should be a string of equalities each being the application of one axiom.</p> <p>You may apply the axioms to either the entire expression or to some sub-expression. For example if we have <span class="math-container">\$(a + c) + (b + c)\$</span> we can apply Axiom 4 to just the <span class="math-container">\$(b + c)\$</span> term, the <span class="math-container">\$(a + c)\$</span> term or the entire expression as a whole. The variables can also stand in for arbitrarily complex expressions for instance we can apply axiom 4 to <span class="math-container">\$((a \times c) + b) + ((-a) + 1)\$</span> to get <span class="math-container">\$((-a) + 1) + ((a \times c) + b)\$</span>. In each step of the proof you can only apply <em>one</em> axiom to <em>one</em> expression. All axioms are bidirectional, meaning substitution can go in either direction. Things like the following are not allowed</p> <pre><code>(a + b) + (c + d) = (a + (b + c)) + d Ax. 1 </code></pre> <p>This should be done in two steps:</p> <pre><code>(a + b) + (c + d) = ((a + b) + c) + d Ax. 1 = (a + (b + c)) + d Ax. 1 </code></pre> <p>Facts you might normally take for granted but are not listed on the axioms list <em>cannot be assumed</em>, for example <span class="math-container">\$(-a) = (-1) \times a\$</span> is true but requires multiple steps to preform.</p> <p>User <a href="https://codegolf.stackexchange.com/users/71303/antony">Anthony</a> has kindly provided <a href="https://antony74.github.io/fol/" rel="noreferrer">a online proof validator</a> that can be used as a replacement for TIO.</p> <h2>Example proof</h2> <p>Here is an example proof that <span class="math-container">\$-(-a) = a\$</span> with the axioms used labeled on the right of each step.</p> <pre><code> -(-a) = (-(-a)) + 0 Ax. 2 = 0 + (-(-a)) Ax. 4 = (a + (-a)) + (-(-a)) Ax. 3 = a + ((-a) + (-(-a))) Ax. 1 = a + 0 Ax. 3 = a Ax. 2 </code></pre> <p><a href="https://antony74.github.io/fol/index.html?eJzT0NXQTdTU5NKA0NoGXAbaGjCxRG2IIEwAyAcxYHyQgAFXIgClkAyv" rel="noreferrer">Try it online!</a></p> <p>You will be tasked to prove <span class="math-container">\$(-a) \times (-a) = a \times a\$</span> using successive substitution like that shown above.</p> <h2>Scoring</h2> <p>This is <a href="/questions/tagged/proof-golf" class="post-tag" title="show questions tagged &#39;proof-golf&#39;" rel="tag">proof-golf</a> so your answers will be scored in number of steps taken to get from <span class="math-container">\$(-a) \times (-a)\$</span> to <span class="math-container">\$a \times a\$</span>, with a lower score being better.</p> <h3>Lemmas</h3> <p>Some answers have chosen to use Lemmas in their proofs, so I will describe how that should be scored to avoid any confusion. For the uninitiated, lemmas are proofs of facts that you use later in the proof. In real mathematics they can be helpful in organizing your thoughts or conveying information clearly to the reader. In this challenge using lemmas should not have an direct effect on your score. (Although proof organization may make it easier or harder to golf)</p> <p>If you choose to use lemmas it will cost as many steps as it took to prove that lemma in the first place each time you use it. For example the here is the score breakdown of a proof using lemmas.</p> <pre><code>Lemma: a × 0 = 0 Proof (7 steps): a × 0 = (a × 0) + 0 Ax. 2 (1) = (a × 0) + ((a × b) + (-(a × b))) Ax. 3 (1) = ((a × 0) + (a × b)) + (-(a × b)) Ax. 1 (1) = (a × (0 + b)) + (-(a × b)) Ax. 8 (1) = (a × (b + 0)) + (-(a × b)) Ax. 4 (1) = (a × b) + (-(a × b)) Ax. 2 (1) = 0 Ax. 3 (1) Theorem: (a × 0) + (b × 0) = 0 Proof (15 steps): (a × 0) + (b × 0) = 0 + (b × 0) Lemma (7) = (b × 0) + 0 Ax. 4 (1) = b × 0 Ax. 2 (1) = 0 Lemma (7) </code></pre> <hr> <p><sup>*: It has been pointed out that this axiom is not strictly necessary to prove this property, however you are still allowed to use it.</sup></p> <p><sup>†: Since <span class="math-container">\$1\$</span> does not appear in the desired equality any proof that uses these axioms is not minimal. That is these axioms cannot help with proving the desired fact. They have been included just for the sake of completeness.</sup></p> https://codegolf.stackexchange.com/q/96402 21 Prove DeMorgan's laws Wheat Wizard https://codegolf.stackexchange.com/users/56656 2016-10-16T08:13:41Z 2017-10-03T00:59:49Z <p>Using the the ten inferences of <a href="https://en.wikipedia.org/wiki/Natural_deduction" rel="noreferrer">the Natural Deduction System</a> prove <a href="https://en.wikipedia.org/wiki/De_Morgan%27s_laws" rel="noreferrer">DeMorgan's laws</a>.</p> <h2>The Rules of Natural Deduction</h2> <ul> <li><p>Negation Introduction: <code>{(P → Q), (P → ¬Q)} ⊢ ¬P</code></p></li> <li><p>Negation Elimination: <code>{(¬P → Q), (¬P → ¬Q)} ⊢ P</code></p></li> <li><p>And Introduction: <code>{P, Q} ⊢ P ʌ Q</code></p></li> <li><p>And Elimination: <code>P ʌ Q ⊢ {P, Q}</code></p></li> <li><p>Or Introduction: <code>P ⊢ {(P ∨ Q),(Q ∨ P)}</code></p></li> <li><p>Or Elimination: <code>{(P ∨ Q), (P → R), (Q → R)} ⊢ R</code></p></li> <li><p>Iff Introduction: <code>{(P → Q), (Q → P)} ⊢ (P ≡ Q)</code></p></li> <li><p>Iff Elimination: <code>(P ≡ Q) ⊢ {(P → Q), (Q → P)}</code></p></li> <li><p>If Introduction: <code>(P ⊢ Q) ⊢ (P → Q)</code></p></li> <li><p>If Elimination: <code>{(P → Q), P} ⊢ Q</code></p></li> </ul> <h2>Proof structure</h2> <p>Each statement in your proof must be the result of one of the ten rules applied to some previously derived propositions (no circular logic) or an assumption (described below). Each rule operates across some propositions on the left hand side of the <code>⊢</code> (logical consequence operator) and creates any number of propositions from the right hand side. The If Introduction works slightly differently from the rest of the operators (described in detail below). It operates across one statement that is the logical consequent of another.</p> <h3>Example 1</h3> <p>You have the following statements:</p> <p><code>{(P → R), Q}</code></p> <p>You may use And Introduction to make:</p> <p><code>(P → R) ʌ Q</code> </p> <h3>Example 2</h3> <p>You have the following statements:</p> <p><code>{(P → R), P}</code></p> <p>You may use If Elimination to make:</p> <p><code>R</code></p> <h3>Example 3</h3> <p>You have the following statements:</p> <p><code>(P ʌ Q)</code></p> <p>You may use And Elimination to make:</p> <p><code>P</code></p> <p>or to make:</p> <p><code>Q</code></p> <h2>Assumption Propagation</h2> <p>You may at any point assume any statement you wish. Any statement derived from these assumptions will be "reliant" on them. Statements will also be reliant on the assumptions their parent statements rely on. The only way to eliminate assumptions is by If Introduction. For If introduction you start with a Statement <code>Q</code> that is reliant on a statement <code>P</code> and end with <code>(P → Q)</code>. The new statement is reliant on every assumption <code>Q</code> relies on <em>except</em> for assumption <code>P</code>. Your final statement should rely on no assumptions.</p> <h2>Specifics and scoring</h2> <p>You will construct one proof for each of DeMorgan's two laws using only the 10 inferences of the Natural Deduction Calculus.</p> <p>The two rules are:</p> <pre><code>¬(P ∨ Q) ≡ ¬P ʌ ¬Q ¬(P ʌ Q) ≡ ¬P ∨ ¬Q </code></pre> <p>Your score is the number of inferences used plus the number of assumptions made. Your final statement should not rely on any assumptions (i.e. should be a theorem).</p> <p>You are free to format your proof as you see fit.</p> <p>You may carry over any Lemmas from one proof to another at no cost to score.</p> <h2>Example Proof</h2> <p>I will prove that <code>(P and not(P)) implies Q</code></p> <p>(Each bullet point is +1 point)</p> <ul> <li><p>Assume <code>not (Q)</code></p></li> <li><p>Assume <code>(P and not(P))</code></p></li> <li><p>Using And Elim on <code>(P and not(P))</code> derive <code>{P, not(P)}</code></p></li> <li><p>Use And Introduction on <code>P</code> and <code>not(Q)</code> to derive <code>(P and not(Q))</code></p></li> <li><p>Use And Elim on the statement just derived to make <code>P</code></p></li> </ul> <p>The new <code>P</code> proposition is different from the other one we derive earlier. Namely it is reliant on the assumptions <code>not(Q)</code> and <code>(P and not(P))</code>. Whereas the original statement was reliant only on <code>(P and not(P))</code>. This allows us to do:</p> <ul> <li><p>If Introduction on <code>P</code> introducing <code>not(Q) implies P</code> (still reliant on the <code>(P and not(P))</code> assumption)</p></li> <li><p>Use And Introduction on <code>not(P)</code> and <code>not(Q)</code> (from step 3) to derive <code>(not(P) and not(Q))</code></p></li> <li><p>Use And Elim on the statement just derived to make <code>not(P)</code> (now reliant on <code>not(Q)</code>)</p></li> <li><p>If Introduction on the new <code>not(P)</code> introducing <code>not(Q) implies not(P)</code></p></li> <li><p>We will now use negation elimination on <code>not(Q) implies not(P)</code> and <code>not(Q) implies P</code> to derive <code>Q</code></p></li> </ul> <p>This <code>Q</code> is reliant only on the assumption <code>(P and not(P))</code> so we can finish the proof with</p> <ul> <li>If Introduction on <code>Q</code> to derive <code>(P and not(P)) implies Q</code></li> </ul> <p>This proof scores a total of 11.</p>