Multiply sequences and add alternatives or, the ubiquitous semiring

§ Formal logic

In formal logic, from propositions P and Q, you can make a new proposition P∨Q, just as meaningful as P or Q alone. The operation associates, so (P∨Q)∨R is equivalent to P∨(Q∨R), and has an identity, False, such that P∨False, or False∨P, is equivalent to P. Logical-AND, making P∧Q, follows similar rules, except that the identity is True instead of False. Between those operations, we also find that P∧(Q∨R) is just as true as (P∧Q)∨(P∧R). Also, P∧False is just as false as False.

§ Natural deduction

Natural deduction proofs give meaning to formal logic by associating proof-actions to operations. Any propositions P and Q can be combined into new propositions P∨Q and P∧Q, equally usable. Having both P and Q is more than needed for OR, but it's still valid.

OR of natural deduction associates. To expand an OR, split out lower-level cases, and accept their common conclusion. You consider the same cases, P, Q, and R, from (P∨Q)∨R and P∨(Q∨R). Either expression can arise in a proof from any one of P, Q, or R.

OR has the identity False. From P, you can derive P∨False. From P∨False, you can split out the case of P, where you prove something depending on P, and the case of False, where you can prove anything to match it. So splitting P∨False has the same consequences as using P alone.

AND, too, associates. You can equally well make (P∧Q)∧R or P∧(Q∧R) from P, Q, and R, by changing the order of steps. Expanding either three-way AND ends with the same statements, P, Q, and R, separated.

AND has the identity True. True can appear from the void in natural deduction, to combine with P for P∧True. P∧True splits into P and True, and True would've been provable anyway. That is, P∧True is equivalent to mere P.

Showing that P∧(Q∨R) and (P∧Q)∨(P∧R) are equivalent is less intuitive; this is what the proof-format is for (here, Fitch-style):

1. P∧(Q∨R)

2. P

3. Q∨R

   4. Q

   5. P∧Q

   6. (P∧Q)∨(P∧R)

   7. R

   8. P∧R

   9. (P∧Q)∨(P∧R)

4. (P∧Q)∨(P∧R)

Equivalence goes both ways.

1. (P∧Q)∨(P∧R)

   2. P∧Q

   3. P

   4. Q

   5. Q∨R

   6. P∧(Q∨R)

   7. P∧R

   8. P

   9. R

   10. Q∨R

   11. P∧(Q∨R)

2. P∧(Q∨R)

P∧False trivially implies P. Less trivially, False implies P∧False:

1. False

   2. ¬P
   3. False

2. ¬¬P

3. P

4. P∧False

§ Combinatorics

If there are x ways event A can play out, and y options for event B, then there are x + y options for the choice of either A or B. Likewise, A followed by B has x·y possibilities. Addition and multiplication of natural numbers follow the properties listed above:

• both closed
• both associate
• both have identities, 0 (impossible event) and 1 (predetermined event), respectively
• x·(y + z) = x·y + x·z
• 0·x = 0

§ QED

Quantum electrodynamics assigns a complex-number amplitude to each conceivable event, from which we derive probabilities. Events combine as in combinatorics — x + y for alternatives, x·y for a sequence — and those operations follow the same properties, here with complex numbers in place of natural numbers.

§ Logical NOT

Formal logic, natural deduction, combinatorics, and QED all share a similar mathematical structure: the semiring. Having that in common suggests they may have other, less obvious traits in common.

Formal logic has an extra operator NOT, defined with a few properties:

• ¬¬P = P
• ¬(P∧Q) = (¬P)∨(¬Q)
• P∨¬P is true for all P

The extra properties, that ¬(P∨Q) = (¬P)∧(¬Q) and that P∧¬P is false for all P, follow trivially from the others.

Natural deduction implements those properties on its own NOT:

• from ¬¬P, derive P
• if P leads to Q∧(¬Q), derive ¬P

Showing that the two forms of NOT are equivalent is a mere set of standard exercises in natural deduction.

In the language of combinatorics — which, so far, matches that of QED — the properties needed for an equivalent of NOT are:

• f(f(x)) = x
• f(x·y) = f(x) + f(y)
• x + f(x) = 1

The second suggests that f, isomorphic to NOT, is a logarithm. The first and third contradict that. NOT is an artifact of formal logic, maintained only in systems specifically designed to match it.

§ Exponents

If event A, with x paths (equivalently, quantum amplitude x), happens y times, there are x^y total paths (resp., final amplitude). 0 and 1 isomorph to False and True, respectively, so we can make a truth table for exponents.

Formal logic has an operation matching that: Q→P. Natural deduction implements it, too:

• if Q leads to P, derive Q→P
• given Q and Q→P, derive P

§ Derivatives

Taking algebraic expressions from combinatorics to define data types, the derivative of a type is the type of its one-hole contexts. Might derivatives take just as novel and meaningful a form in formal logic?

Take all derivatives "with respect to P". Insofar as OR is like addition, (P∨Q)' = P'∨Q' = True∨Q' = True. Further, as True is like 1, and False like 0, True' = False. Aliter, True' = (P∨True)' = True. Alas, the properties of the derivative contradict each other in formal logic.