# Can you do without conditional proof if you have indirect proof? **URL:** \ **Category:** Factual Questions\ **Created:** [October 5, 2012, 4:17pm UTC](https://boards.straightdope.com/t/can-you-do-without-conditional-proof-if-you-have-indirect-proof/636820 "2012-10-05T16:17:28Z")\ **Posts on this page:** 20\ **Page:** 2
**Author:** ![Indistinguishable](https://avatars.discourse-cdn.com/v4/letter/i/90ced4/32.png) [@Indistinguishable](https://boards.straightdope.com/u/Indistinguishable)\ **Post date:** [October 8, 2012, 5:13pm UTC](https://boards.straightdope.com/t/can-you-do-without-conditional-proof-if-you-have-indirect-proof/636820/21 "2012-10-08T17:13:57Z")
Did post #19 suffice to answer your original question? ---
**Author:** ![Frylock](https://avatars.discourse-cdn.com/v4/letter/f/ce7236/32.png) [@Frylock](https://boards.straightdope.com/u/Frylock)\ **Post date:** [October 9, 2012, 2:22am UTC](https://boards.straightdope.com/t/can-you-do-without-conditional-proof-if-you-have-indirect-proof/636820/22 "2012-10-09T02:22:55Z")
Yes it did–thanks! -KR ---
**Author:** ![Jragon](https://avatars.discourse-cdn.com/v4/letter/j/e19b73/32.png) [@Jragon](https://boards.straightdope.com/u/Jragon)\ **Post date:** [October 9, 2012, 3:54am UTC](https://boards.straightdope.com/t/can-you-do-without-conditional-proof-if-you-have-indirect-proof/636820/23 "2012-10-09T03:54:27Z")
> [@chrisk](#): > > As stated, this makes no sense, so I’ve almost certainly got it wrong. The end is probably ‘Therefore ~A’ > > Crazily enough, I just spent a few minutes listing the symlog propositional logic rules I remember from university, and most of these match. You’ve got: > & introduction > & elimination > v introduction (you should also specify that you can derive A v B from B, to show that it’s symmetrical) > v elimination > -\> elimination > > - elimination > -\> introduction > > There are rules in the list for = introduction or elimination, but you probably don’t need to use that operator as it can be expressed in terms of -\> and & (or in other ways.) > > To get the double negation, one thing you’ll need is the - introduction: > Derive -A if you can derive a contradiction from A > > Other than that, it looks reasonably tight. If I understand right, your list includes conditional proof but not indirect proof, yes? You don’t even need all of those. Literally all you need for prop logic is DeMorgan’s law, double negation (A ^ B) = --(A^B) = -(-A v -B) and the rest can follow from resolution – i.e. A v -B -A v C Therefore, B v C All prop logic statements can be converted into a sequence of or statements, and all proofs can be done by resolution. (Technically this means all you need for logic is an or operator and a not operator, but and is so common we’ll be generous and grant it and DeMorgan’s at minimum) ---
**Author:** ![Jragon](https://avatars.discourse-cdn.com/v4/letter/j/e19b73/32.png) [@Jragon](https://boards.straightdope.com/u/Jragon)\ **Post date:** [October 9, 2012, 4:00am UTC](https://boards.straightdope.com/t/can-you-do-without-conditional-proof-if-you-have-indirect-proof/636820/24 "2012-10-09T04:00:08Z")
Forgot to mention: Proofs by resolution are proofs by contradiction. You assume the opposite is true and derive the empty set. ---
**Author:** ![Indistinguishable](https://avatars.discourse-cdn.com/v4/letter/i/90ced4/32.png) [@Indistinguishable](https://boards.straightdope.com/u/Indistinguishable)\ **Post date:** [October 9, 2012, 4:05am UTC](https://boards.straightdope.com/t/can-you-do-without-conditional-proof-if-you-have-indirect-proof/636820/25 "2012-10-09T04:05:16Z")
> [@Jragon](#): > > You don’t even need all of those. Literally all you need for prop logic is DeMorgan’s law, double negation (A ^ B) = --(A^B) = -(-A v -B) and the rest can follow from resolution – i.e. > > A v -B > -A v C > Therefore, B v C > > All prop logic statements can be converted into a sequence of or statements, and all proofs can be done by resolution. I think you mean A v B -A v C Therefore, B v C And you’ll also need a rule saying “If you can derive falsehood (i.e., the 0-ary disjunction) from the added assumption of A, then you can conclude -A”; otherwise, you’d never be able to get off the ground. And, for **Frylock** ’s purposes, with “-\>” in the language, you’ll also need a rule defining “-\>” in terms of &, v, and - (“A -\> B = -A v B”, say). But, yes, that’d be enough. On edit: Whoops, should have refreshed. You noted the proof by contradiction bit already. ---
**Author:** ![Jragon](https://avatars.discourse-cdn.com/v4/letter/j/e19b73/32.png) [@Jragon](https://boards.straightdope.com/u/Jragon)\ **Post date:** [October 9, 2012, 4:12am UTC](https://boards.straightdope.com/t/can-you-do-without-conditional-proof-if-you-have-indirect-proof/636820/26 "2012-10-09T04:12:04Z")
> [@Indistinguishable](#): > > I think you mean > > A v B > -A v C > Therefore, B v C Oops > [@](#): > > And, for **Frylock** ’s purposes, with “-\>” in the language, you’ll also need a rule defining “-\>” in terms of &, v But I was just mentioning all you need for prop logic, obviously you can define “-\>” if you really want (just like you can define xor if you really want, even though a lot of people don’t use it) – I was just pointing out that you don’t HAVE to. ---
**Author:** ![Indistinguishable](https://avatars.discourse-cdn.com/v4/letter/i/90ced4/32.png) [@Indistinguishable](https://boards.straightdope.com/u/Indistinguishable)\ **Post date:** [October 9, 2012, 4:35am UTC](https://boards.straightdope.com/t/can-you-do-without-conditional-proof-if-you-have-indirect-proof/636820/27 "2012-10-09T04:35:36Z")
Sure, sure. I mean, there’s nothing special about v, &, and - either; you don’t have to have them either. Your language could be just the 0-ary connectives true and false, and the 3-ary connective (a ? b : c) [i.e., \*if a, then b, else c\*], and your rules could be true ? b : c = b false ? b : c = c f(x) = x ? f(true) : f(false) with a derivation of a statement being a derivation of its equality to true. Indeed, as I see it, this is the soul of Boolean algebra. Then, of course, you could define all the other connectives out of these (-a = a ? false : true, a v b = a ? true : (b ? true : false), a -\> b = a ? b : true, and so on…). ---
**Author:** ![Indistinguishable](https://avatars.discourse-cdn.com/v4/letter/i/90ced4/32.png) [@Indistinguishable](https://boards.straightdope.com/u/Indistinguishable)\ **Post date:** [October 9, 2012, 5:01am UTC](https://boards.straightdope.com/t/can-you-do-without-conditional-proof-if-you-have-indirect-proof/636820/28 "2012-10-09T05:01:22Z")
> [@Indistinguishable](#): > > But, yes, that’d be enough. Whoops, come to think of it, you didn’t say enough: you need a distributivity rule to be able to rewrite things into conjunctive normal form. That is, your rules will not be enough to derive a contradiction from A v (B & C), -((A v B) & (A v C)) Proof: All your rules would still be valid if we interpreted negation standardly, but re-interpreted “A v B” as meaning “true, no matter what A and B are”, and “A & B” as meaning “false, no matter what A and B are”. However, under this re-interpretation, one cannot obtain a contradiction from the above two propositions, as both will amount to tautologies. ---
**Author:** ![Indistinguishable](https://avatars.discourse-cdn.com/v4/letter/i/90ced4/32.png) [@Indistinguishable](https://boards.straightdope.com/u/Indistinguishable)\ **Post date:** [October 9, 2012, 5:32am UTC](https://boards.straightdope.com/t/can-you-do-without-conditional-proof-if-you-have-indirect-proof/636820/29 "2012-10-09T05:32:41Z")
So all spelled out, the resolution rules are like so: The primitive operations are negation (-) and disjunction (v) Disjunctions are an abelian monoid; you can re-order and re-associate them at will. [Alternatively, you could reword the resolution rule to be agnostic to such issues] Negation is involutive; you may replace --X by X or vice versa anywhere at will. Disjunction distributes over its De Morgan dual [the operation defined by A & B = -(-A v -B)]; you may replace X v (Y & Z) by (X v Y) & (X v Z) anywhere at will. From A v B and -A v C, you may derive A v C If adding the assumption A lets you derive the empty disjunction, you may derive -A It’s alright, but it doesn’t seem so much more minimalistic to me than anything else. ---
**Author:** ![Indistinguishable](https://avatars.discourse-cdn.com/v4/letter/i/90ced4/32.png) [@Indistinguishable](https://boards.straightdope.com/u/Indistinguishable)\ **Post date:** [October 9, 2012, 5:40am UTC](https://boards.straightdope.com/t/can-you-do-without-conditional-proof-if-you-have-indirect-proof/636820/30 "2012-10-09T05:40:04Z")
Er, and also, toss “From A & B, you may derive A” on top of all that. ---
**Author:** ![Frylock](https://avatars.discourse-cdn.com/v4/letter/f/ce7236/32.png) [@Frylock](https://boards.straightdope.com/u/Frylock)\ **Post date:** [October 9, 2012, 11:22am UTC](https://boards.straightdope.com/t/can-you-do-without-conditional-proof-if-you-have-indirect-proof/636820/31 "2012-10-09T11:22:44Z")
> [@Jragon](#): > > Oops > > But I was just mentioning all you need for prop logic, obviously you can define “-\>” if you really want (just like you can define xor if you really want, even though a lot of people don’t use it) – I was just pointing out that you don’t HAVE to. If we’re talking about minimal sets of operators, you just need the sheffer stroke. But what I was working on was something intended (at least originally) to be more lay-intuitive. ---
**Author:** ![Frylock](https://avatars.discourse-cdn.com/v4/letter/f/ce7236/32.png) [@Frylock](https://boards.straightdope.com/u/Frylock)\ **Post date:** [October 9, 2012, 11:26am UTC](https://boards.straightdope.com/t/can-you-do-without-conditional-proof-if-you-have-indirect-proof/636820/32 "2012-10-09T11:26:04Z")
> [@Indistinguishable](#): > > Indeed, as I see it, this is the soul of Boolean algebra. I’m actually really surprised to hear you say that anything is the soul of anything. 😉 ---
**Author:** ![Frylock](https://avatars.discourse-cdn.com/v4/letter/f/ce7236/32.png) [@Frylock](https://boards.straightdope.com/u/Frylock)\ **Post date:** [October 9, 2012, 11:27am UTC](https://boards.straightdope.com/t/can-you-do-without-conditional-proof-if-you-have-indirect-proof/636820/33 "2012-10-09T11:27:14Z")
Can you say something, or point me to something, explaining in what sense false is the 0-ary case of v, and true the 0-ary case of &? ---
**Author:** ![chrisk](https://avatars.discourse-cdn.com/v4/letter/c/6de8d8/32.png) [@chrisk](https://boards.straightdope.com/u/chrisk)\ **Post date:** [October 9, 2012, 2:05pm UTC](https://boards.straightdope.com/t/can-you-do-without-conditional-proof-if-you-have-indirect-proof/636820/34 "2012-10-09T14:05:16Z")
> [@Frylock](#): > > Can you say something, or point me to something, explaining in what sense false is the 0-ary case of v, and true the 0-ary case of &? Well, try looking at it this way: (false v A) is logically equivalent to A - it evaluates to true if A is true, otherwise it is false. In the same way (false v A) v B is equivalent to A v B (true & A) is logically equivalent to A, in the same way. Therefore, if you were to ‘run the v program’ without supplying any inputs at all, it would default to false - it returns true iff at least one of the inputs is true. Similarly, if you had an & program that could take arbitrarily many inputs, the easiest way to describe its behavior is that it returns false iff at least one of the inputs is false. Saying that it ‘returns true iff all the inputs are true’ is logically equivalent, but when you put it in terms of ‘at least one’, it’s easier to see the logically consistent behaviour for 0 inputs. So without any input, the & program will return true. Does that make any sense? ---
**Author:** ![Frylock](https://avatars.discourse-cdn.com/v4/letter/f/ce7236/32.png) [@Frylock](https://boards.straightdope.com/u/Frylock)\ **Post date:** [October 9, 2012, 2:41pm UTC](https://boards.straightdope.com/t/can-you-do-without-conditional-proof-if-you-have-indirect-proof/636820/35 "2012-10-09T14:41:29Z")
> [@chrisk](#): > > Well, try looking at it this way: > > (false v A) is logically equivalent to A - it evaluates to true if A is true, otherwise it is false. In the same way (false v A) v B is equivalent to A v B > > (true & A) is logically equivalent to A, in the same way. > > Therefore, if you were to ‘run the v program’ without supplying any inputs at all, it would default to false - it returns true iff at least one of the inputs is true. Similarly, if you had an & program that could take arbitrarily many inputs, the easiest way to describe its behavior is that it returns false iff at least one of the inputs is false. Saying that it ‘returns true iff all the inputs are true’ is logically equivalent, but when you put it in terms of ‘at least one’, it’s easier to see the logically consistent behaviour for 0 inputs. So without any input, the & program will return true. > > Does that make any sense? It does make a kind of sense, but feels like fudging when you start talking about how to make it “easier to see” something or the “easiest way to describe” behavior. ---
**Author:** ![chrisk](https://avatars.discourse-cdn.com/v4/letter/c/6de8d8/32.png) [@chrisk](https://boards.straightdope.com/u/chrisk)\ **Post date:** [October 9, 2012, 2:51pm UTC](https://boards.straightdope.com/t/can-you-do-without-conditional-proof-if-you-have-indirect-proof/636820/36 "2012-10-09T14:51:33Z")
> [@Frylock](#): > > It does make a kind of sense, but feels like fudging when you start talking about how to make it “easier to see” something or the “easiest way to describe” behavior. Okay, then, consider this… A: All the barbers in this town are Chinese. B: You’re lying. I’ve met everybody in town, and I didn’t see any Chinese barbers. A: Did you see any barbers at all? B: Well, no, I guess not. But if there aren’t any barbers, then you can’t say anything about them. A: No, it’s true. All the barbers of this town are Chinese, and what’s more, they’re all missing a finger. Do you agree with B, or can you see from A’s (slightly whimsical) point of view? Speaking logically, ‘all of group A can be described by B’ is true if group A is empty - just like the empty set is a subset of every other set. ---
**Author:** ![Indistinguishable](https://avatars.discourse-cdn.com/v4/letter/i/90ced4/32.png) [@Indistinguishable](https://boards.straightdope.com/u/Indistinguishable)\ **Post date:** [October 9, 2012, 4:30pm UTC](https://boards.straightdope.com/t/can-you-do-without-conditional-proof-if-you-have-indirect-proof/636820/37 "2012-10-09T16:30:17Z")
> [@Frylock](#): > > Can you say something, or point me to something, explaining in what sense false is the 0-ary case of v, and true the 0-ary case of &? Sure. I can point you to [your own attempt](http://boards.straightdope.com/sdmb/showpost.php?p=10447405&postcount=5) to explain it, [slightly generalized](http://boards.straightdope.com/sdmb/showpost.php?p=10453873&postcount=27). Think of A & B & C & D & … as meaning “All of the conjuncts are true”. If there are no conjuncts, this is vacuously true. Think of A v B v C v D v … as meaning “There exists a conjunct which is true”. If there are no conjuncts, this is vacuously false. Also: Think of True as positive integers, and False as 0. Then & is multiplication, and v is addition. Empty multiplication is 1, empty addition is 0. In general, whenever one has a monoid (an associative operation with an identity element), one thinks of the identity element as the 0-ary case of the monoid operation. This lets one cleanly unify many analyses. [And also means monoids can alternatively be characterized by the description in the second link above.] ---
**Author:** ![Indistinguishable](https://avatars.discourse-cdn.com/v4/letter/i/90ced4/32.png) [@Indistinguishable](https://boards.straightdope.com/u/Indistinguishable)\ **Post date:** [October 9, 2012, 4:37pm UTC](https://boards.straightdope.com/t/can-you-do-without-conditional-proof-if-you-have-indirect-proof/636820/38 "2012-10-09T16:37:56Z")
We can also just look at the 0-ary case of the proof rules you gave: We can derive A\_1 & … & A\_n from the prerequisites of each of A\_1, …, A\_n. In the 0-ary case, there are no prerequisites; thus, we can derive 0-ary conjunction for free. This makes 0-ary conjunction as good as True. We can derive C from A1 v \_ … \_ A\_n, along with the further requirements of each of A\_1-\>C, …, A\_n -\> C. In the 0-ary case, there are no further requirements; thus, we can derive arbitrary C from 0-ary disjunction. This makes 0-ary disjunction as good as False. ---
**Author:** ![Indistinguishable](https://avatars.discourse-cdn.com/v4/letter/i/90ced4/32.png) [@Indistinguishable](https://boards.straightdope.com/u/Indistinguishable)\ **Post date:** [October 9, 2012, 5:05pm UTC](https://boards.straightdope.com/t/can-you-do-without-conditional-proof-if-you-have-indirect-proof/636820/39 "2012-10-09T17:05:48Z")
> [@Frylock](#): > > I’m actually really surprised to hear you say that anything is the soul of anything. 😉 Don’t worry. If anyone pressed me on it, I’d quickly concede that Boolean algebra is a multifarious subject which can be fruitfully understood from many disparate perspectives and via many disparate mathematical analogies, and also, that there’s no such thing as souls. 🙂 > [@Frylock](#): > > If we’re talking about minimal sets of operators, you just need the sheffer stroke. If I may continue my pedantry, the (2-ary) Sheffer stroke isn’t quite sufficient to axiomatize Boolean algebra. You can’t build any of the 0-ary operations from it (sure, you can get 1-ary operations which ignore their input, but that’s not the same thing. The empty set can be given a Sheffer stroke structure, but the empty set is not a Boolean algebra.). Easily patched, of course; a proper minimal set of operators would be the 2-ary Sheffer stroke along with the 0-ary operation False (that is, the negations of the 2-ary and 0-ary ANDs). ---
**Author:** ![Frylock](https://avatars.discourse-cdn.com/v4/letter/f/ce7236/32.png) [@Frylock](https://boards.straightdope.com/u/Frylock)\ **Post date:** [October 9, 2012, 6:46pm UTC](https://boards.straightdope.com/t/can-you-do-without-conditional-proof-if-you-have-indirect-proof/636820/40 "2012-10-09T18:46:12Z")
> [@Indistinguishable](#): > > Sure. I can point you to [your own attempt](http://boards.straightdope.com/sdmb/showpost.php?p=10447405&postcount=5) to explain it, [slightly generalized](http://boards.straightdope.com/sdmb/showpost.php?p=10453873&postcount=27). I have no recollection of writing that at all. But now that I’ve read it, and the rest of your post, I can see how the analogy works, and can understand the justification in terms of unified analyses. I will (apparently) not remember any of this four years hence I’m afraid. ☹ [Previous page](https://boards.straightdope.com/t/can-you-do-without-conditional-proof-if-you-have-indirect-proof/636820.md?page=1) [Next page](https://boards.straightdope.com/t/can-you-do-without-conditional-proof-if-you-have-indirect-proof/636820.md?page=3)