I'm trying to work through something about rules of implication. So I can show, even if I have to use truth tables, that (if a then b) = (if a then a and b). And I know (if a then b) = (not a or b). So I seem to have (not a or b) = (not a or (a and b)). Then there is (if a then b else c). This is equivalent to ((if a then b) or (if not a then c)), because a can't be both true and false. Or should it be ((if a then b) and (if not a then c))?

The latter is correct; ((if a then b) and (if not a then c)). Expanding this out using the identities you gave above, ((if a then b) and (if not a then c)) = ((not a or b) and (not not a or c)) We can shuffle this around using the identity ((a or b) and (x or y)) = ((a and x) or (a and y) or (b and x) or (b and y)) which leaves ((not a or b) and (not not a or c)) = ((not a and a) or (not a and c) or (b and a) or (b and c)) = ((not a and c) or (a and b) or (b and c)) This actually reveals something about the condition that I missed on first reading: as written, b and c can both be true, in which case they tell us nothing about a. What implication problem are you trying to work through?

It's just how to rearrange if a then b else c, so you get an algebraic statement: (a and b) or (not a and c). I think I got the same answer you did in the following way. (if a then b) -> (a and b) or (not a and b) or (not a and not b). You can leave out not(a and not b) because it's logically equivalent to (not a or b) which is logically equivalent to (if a then b). Likewise (if not a then c) -> (not a and c) or (a and c) or (a and not c). So If I write: (if a then b) or if (not a then c) -> (a and b) or (not a and b) or (not a and not b) or (not a and c) or (a and c) or (a and not c), then rearranging, I get: (a and b) or (not a and c) or (b and c). Interesting how I use disjunction and your argument uses conjunction . . . It seems you can't avoid that b and c can both be true. However, in the context I'm using the logic, b and c are program branches, since both branches can't be taken (b and c) can be ignored.

One thing I tried was thinking about what's true after if a then b else c. a is true or false, which is also true before the if-then-else, and b or c is true. If you substitute b and c with P and Q, call them programs, then a has a different character, it's a test condition. So you seem to separate conditions from programs or program segments, since now a can be true or false, but P or Q represents a branch, one of P and Q is not taken so the logic statement (P and Q) is false in that context. I've noticed you can also start with (a and P) or (not a and Q). I get: ((a and P) or not a) and ((a and P) or Q) = (not a or a) and (not a or P) and (a or Q) and (P or Q) = (not a or P) and (a or Q) and (P or Q). So if I write code like: if a then P if not a then Q which is written in a shorter syntax with: if a then P else Q It means conjunction (meet), in the context of two if statements, but it's a join in the context of (a meet P) join (not a meet Q).

I think I see finally how to do what I've been trying to: I want to show: (If a then P)(If not a then Q) is equivalent to (not a or P) and (a or Q) which is equivalent to (a and P) or (not a and Q). Notice that the last statement implies P or Q is always true, and that they can't both be true, so P and Q is always false. In fact the exclusive or is implied.

That's a theorem: any syllogism formulated using "and" can be equivalently formulated using "or", and vice versa - not only within the premises and conclusion, but as the implied relationship between the premises (usually understood to be "and"). This is immediate from observing that a notation such as Bateson's in "Laws of Form", capable of embodying any instance of bivalued argument, can be transcribed into English either way.

I'm satisfied it shows there is nothing special about programs, P,Q are just a pair of logical objects which define the exclusive or relation, which seems to be what if-then-else is. On the other hand, program branching in this context (a logical 'program algebra') takes the state true to the state "the branch is taken". There should be a straightforward way to extend program branching into looping--returning to the same branch point.

There is another aspect to the logic: you assume that notation like (if a then P)(if not a then Q) = if a then P else Q, is sequential--a is either true or false, P or Q is the branch taken. Then P and Q doesn't appear, you can't take both paths. This is the standard deterministic picture of computations where the state of a is only needed at some branch point (i.e. is a local variable). But what if you switch the idea of sequentiality with concurrence, and what if a can be simultaneously true and false (pointing up and down, say), with P and Q also true or false (a situation where two distinct physical paths are taken)? Is a program logic still in there?