Linear logic has connectives not used in classical logic. The connectives ⊗and & are conjunctions, ⊕ and ⅋ are disjunctions, and ! and ? are analogous to the modal operators ◻ and ◇ (necessity and possibility).

Another way to classify the connectives is to say ⊕ and & are called additive, ⊗ and ⅋ are multiplicative, and ! and ? are called exponential.And still another classification says that ⊕, ⊗, and ! have positive polarity, while &, ⅋, and ? have negative polarity.

This post will show that these arithmetical names are justified by analogy.

For one thing, multiplication-like connectives distribute over addition-like connectives.
2

Also, the exponential-like operators behave analogously to the equation

with respect to the addition-like and multiplication-like connectives.

In both equations, if you apply an exponential-like operator to the result of applying an addition-like operator, you get a multiplication-like operator applied to the exponential-like operator applied to two addition-like arguments separately.

The term “polarity” is justified by the fact that linear negation flips the polarity of connectives.

In the following analogs of De Morgan’s laws, negation turns conjunctions into disjunctions and vice versa, and it reverses the polarity of connectives.

Negating exponential connectives also flips polarity.

These rules are analogous to the rules for negating quantifiers in classical logic.

More logic posts

• Minimizing Boolean expressions
• Rotating symbols in LaTeX
• Modal and temporal logic for security

Stanislaw Ulam once said

Using a term like nonlinear science is like referring to the bulk of zoology as the study of non-elephant animals.

There is only one way to be linear, but there are many ways to not be linear.

A similar observation applies to non-classical logic. There are many ways to not be classical.

Modal logic axioms

Modal logic extends classical logic by adding modal operators □ and ◇. The interpretation of these operators depends on the application, but a common interpretation is “necessarily” and “possibly.”

There are a bewildering number of possible axioms to choose from in order to create a system of modal logic, and these often have cryptic names like “K”, “G”, and “5”. Seldom is any reason given for the names, and after digging into this a little, I think I know why: There isn’t much reason. Or rather, the reasons are historical rather than mnemonic.

For example, Axiom T is so named because Kurt Gödel published a paper that called some set of axioms “System T.” Of course that raises the question of why Gödel called his system “T.”

Axiom 5 gets its name from C. I. Lewis’ classification of logic systems. But Lewis’ numbering of systems S1 through S5 was essentially arbitrary, other than larger numbers corresponding to more axioms.

Unless you’re interested in the history for its own sake, it’s probably not worth questioning why rules are called what they are.

Lemmon numbering

Although there’s not much logic behind the names of model logic axioms, there is a convenient way to catalog many of them. E. J. Lemmon [1] observed that many axioms for modal logic can be written in the form

Here’s a list of some common modal logic axioms, along with their names and Lemmon numbers.

[1] E. J. Lemmon, An Introduction to Modal Logic, American Philosophical Quarterly, Monograph 11. Oxford, 1977.

I got an email from Fr. John Rickert today, and with his permission I’ll share part of it here.

A sin of commission occurs when we do something we should not do. A system is consistent (or maybe I should say “sound”) if the results of proofs really are true. Gödel’s 2nd Incompleteness Theorem says that it is undecidable whether Peano Arithmetic commits any “sins of commission.”

A sin of omission occurs when we fail to do something that we should do. A system is complete if every true statement actually has a proof (in finitely many steps). Gödel’s 1st Incompleteness Theorem says that Peano Arithmetic does commit some “sins of omission”: There are truths that cannot be proved.

Finally, a conscience is perplexed if it does not know whether to do or refrain from a proposed action; the conscience is de facto in a state of invincible ignorance. Undecidability is invincible ignorance.

Of course a formal system isn’t under any moral obligations, and certainly not under obligation to do what it cannot do. These are just analogies. But they are interesting analogies. Sins of commission and omission, things done and things left undone, are more verbally parallel than completeness and soundness.

Here’s another post based on an email exchange with Fr. Rickert exactly one year ago: Unexpected square wave.

Formal verification of theorems takes a lot of work. And it takes more work where it is least needed. But the good news is that it takes less effort in contexts where it is needed most.

Years of effort have gone into formally verifying the proofs of theorems that no one doubted were correct. For example, a team worked for six years to formally verify the proof of the odd-order theorem in group theory.

Mathematical proofs are fallible, but it’s rare for a proof to be accepted that reaches a wrong conclusion. Flaws in proofs are much more likely to be gaps in reasoning than to be arguments in favor of false statements. And the more people who study a proof, the more likely it is that flaws will be found and fixed.

The return on investment for formal verification is highest for theorems that are the opposite of the odd-order theorem, theorems that are obscure and shallow rather than famous and deep.

For example, suppose you want to prove that a complex set of security protocols doesn’t have any gaps. Your problem is obscure in that only your company cares about it. You don’t have the assurance that would come from thousands of mathematicians around the world reviewing your work.

But on the plus side, your security rules are logically shallow. These rules may be too complicated to hold in your head, but they can be formally specified with far less effort than some mathematical object like a Möbius strip. In general, discrete things like if-then rules are much easier to formalize than continuous things like real numbers.

Mathematicians choose to study things they have some intuition for, and that intuition is often correct even when the reasoning around it is logically incomplete. But businesses are often faced with complex problems they did not chose and problems for which no one has much intuition, such as proving that a complex circuit does what it’s supposed to do, or that an encryption protocol didn’t neglect some edge case. That’s where the ROI on formal methods is greatest.

The previous post looked at all Boolean expressions on three or four variables and how much they can be simplified. The number of Boolean expressions on n variables is

and so the possibilities explode as n increases. We could do n = 3 and 4, but 5 would be a lot of work, and 6 is out of the question.

So we do what we always do when a space is too big to explore exhaustively: we explore at random.

The Python module we’ve been using, qm, specifies a function of n Boolean variables in terms of the set of product terms on which the function evaluates to 1. These product terms can be encoded as integers, and so a Boolean function of n variables corresponds to a subset of the integers 0 through 2ⁿ – 1.

We can generate a subset of these numbers by generating a random mask consisting of 0s and 1s, and keeping the numbers where the mask value is 1. We could do this with code like the following.

     N= 2**n
     x = np.arange(N)
     mask = np.random.randint(2, size=N)
     ones = set(mask*x)

There’s a small problem with this approach: the set ones always contains 0. We want it to contain 0 if and only if the 0th mask value is a 1.

The following code generates a Boolean expression on n variables, simplifies it, and returns the length of the simplified expression [1].

    def random_sample(n):
        N = 2**n
        x = np.arange(N)
        mask = np.random.randint(2, size=N)
        ones = set(mask*x)
        if mask[0] == 0:
            ones.remove(0)
        return len(qm(ones=ones, dc={}))

We can create several random samples and make a histogram with the following code.

    def histogram(n, reps):
        counts = np.zeros(2**n+1, dtype=int)
        for _ in range(reps):
            counts[random_sample(n)] += 1
        return counts

The data in the following graph comes from calling histogram(5, 1000).

Note that the length of the random expressions is distributed symmetrically around 16 (half of 2⁵). So minimization turns a distribution centered around 16 into a distribution centered around 8.

The code is slow because the Quine-McCluskey algorithm is slow, and our Python implementation of the algorithm isn’t as fast as it could be. But Boolean minimization is an NP problem, so no exact algorithm is going to scale well. To get faster results, we could switch to something like the Expresso Heuristic Logic Minimizer, which often gets close to a minimum expression.

***

[1] The code above will fail if the set of terms where the function is 1 is empty. However this is extremely unlikely: we’d expect it to happen once in every 2^(2^n) times and so when n = 5 this is less than one time in four billion. The fully correct approach would be to call qm with zeros=x when ones is empty.