The Allsome Quantifier

David A. Wheeler

2018-11-14 (originally 2018-10-20)

It is easy to mistranslate informal statements into formal logic, and these errors can cause serious problems (potentially including property damage, maiming, and loss of life). For example, in formal logic, “All Martians are green” would often be represented as ∀x (φ→ψ), while “All Martians are not green” would often be represented as ∀x (φ→¬ψ). In formal logic both statements are simultaneously true if there are no Martians. However, informal statements with this format often embed the assumption that there is at least one case where the antecedent is true (that is, that there is at least one Martian). This essay proposes a new formal logic quantifier called “allsome” (aka “all some”) that is designed to make some of these mistranslations less likely. The allsome quantifier, abbreviated ∀!, simultaneously expresses for all (∀) and there exists (∃) in a way that models many informal statements. It has two syntactic forms, formally defined as follows: ∀! x (φ→ψ) ≡ ∀ x (φ→ψ) ∧ ∃ x φ and ∀! x∈A φ ≡ (∀ x∈A φ) ∧ ∃ x x∈A. We have implemented this construct in the Metamath proof system and formally proven that it counters this well-known problem. We also compare this approach to alternative countermeasures in PVS and SPARK. We hope that this new quantifier will help reduce the risk of mistranslations of informal statements into formal expressions, and that others will eventually agree that allsome is awesome.

The problem

Modern formal logic notation can represent many statements with great precision. This is very valuable, because formal logic can be verified by computers to ensure that certain claims can be proven from other claims, including those that can prevent loss of life. Unfortunately, it is easy to mistranslate informal statements into current formal logic notation, resulting in “proofs” that in fact do not prove anything important. That could be a disaster, because sometimes proofs are used to model systems to ensure that they do not damage property, maim, or kill. Even in pure mathematics we would like to ensure that what was proved is what we thought was proved. We should prefer notations that are unlikely to misunderstood, yet today some common constructs are easy to get wrong. This is especially true when material implication (→) is combined with the for-all quantifier (∀).

This is perhaps best explained using an example. The sentence “All Martians are green” would typically be represented formally using the expression ∀x (φ→ψ), which means for all x, if φ is true then ψ is true. In this example expression φ is true if and only if (iff) x is a Martian and ψ is true iff x is green. Similarly, “All Martians are not green” would typically be represented as ∀x (φ→¬ψ), that is, for all x, if φ is true then ψ is not true (we will use the traditional symbols ¬ for “not”, ∧ for “and”, and ∨ for “or”).

The problem happens if there are no Martians. In formal logic, this can be represented as ¬∃x φ (“it is not true that there exists an x that is a Martian”). If there are no Martians, then the statements “All Martians are green” and “All Martians are not green” are both true. That is surprising to the inexperienced, because the two expressions seem to be the opposite of each other. The reason this occurs in formal (classical) logic is because the implication (φ→ψ) is equivalent to ¬φ ∨ ψ. When φ is always false, ¬φ is always true, and an or with true is always true. You can see a detailed formal proof of this in the Metamath proof of alimp-surprise, and a proof of a similar problem at empty-surprise.

In short: expressions that use for-all and implication (such as ∀x (φ→ψ)) have surprising results to non-experts if the implication’s antecedent is never true. This also affects expressions that use for-all and a variable that ranges over a restricted set, since that is simply an abbreviation of a for-all with implication. Statements like this are sometimes called “vacuously true” statements.

(Brief aside: We use Martians in our examples due to a vague sense of convention and because at the time of this writing there are no known Martians. If it is widely known that there are Martians in the time you are reading this, use some other set that is not certain to be inhabited.)

A solution: the allsome quantifier

In this author’s experience, the problem stems from a disconnect between informal language and formal logic notation. In informal language, when we say that all X is Y, there is often an assumption that at least one X exists. This goes back to at least [Aristotle], who expressly and intentionally excluded empty sets from his logic system [Groarke]. It is possible to state that something exists in modern formal logic notation, in addition to saying that they all do it if they exist, but in typical formal logic notation this requires using two different quantifiers. There is no way to simply express this common informal statement in formal logic notation when using a single standard quantifier. This lack of a simple way to formally represent a common kind of informal statement can hide a lot of mischief.

Here we propose the “allsome” (aka “all some”) quantifier, a convenient shorthand that combines the “for all” quantifier (∀) with an “exists” quantifier (∃). This new quantifier directly represents the common informal statement pattern that simultaneously asserts that some assertion is true of all Xs and that there is at least one X. We have chosen “∀!” as the allsome symbol, with two syntactical patterns: a more general case that applies to a top-level implication, and a shorthand case that is applied to all members of a class. Here are their formal definitions:

  1. ∀! x (φ→ψ) ≡ ∀x (φ→ψ) ∧ ∃xφ   [df-alsi]
  2. ∀! xA φ ≡ (∀xA φ) ∧ ∃x xA   [df-alsc]

For example, if we now write “All Martians are green” as ∀! x (φ→ψ), we are simultaneously asserting that all Martians are green and that there is at least one Martian, which is almost certainly what the speaker actually meant.

The terminology and symbol are carefully chosen. The term “allsome” was chosen because it’s short, easy to say, and clearly hints at the two concepts it combines (∀ and ∃). The alternative “allexist” takes longer to say (three syllables instead of two) and is also more challenging to say due to the large sound shift between its vowels. We chose the term “allsome” instead of “someall” because we expect it to be used in cases where the human is focusing on the notion of “all” - so it made sense to emphasize that. The symbol ∀! was chosen since there is already a ∃! symbol that suggests that it is some variant of ∃ (so there is precedence for combining an explanation mark with a quantifier). In addition, this sequence when used as a symbol does not require that a new Unicode character be created and implemented before the symbol can be used. It might be useful to create a new Unicode character for it in the future, but it will be easier to make that argument once the symbol attains broader use.

This new quantifier does not eliminate the traditional for all (∀) quantifier, in fact, allsome is defined using for all. Instead, this new quantifier makes it easier to express a common circumstance, and perhaps more importantly, it reduces the risk of dangerous misstatements (which could lead to property destruction, maiming, or death if you are depending on the proofs to prevent that).

We have received a number of interesting comments from Yannick Moy; one was that this “might be overkill in some occasions, because it’s more difficult to prove than a simple ‘for all’ quantification, and it’s likely to be less automated because automatic provers are bad with exhibiting witnesses.” A “witness” is simply an example that shows that something exists. We agree that sometimes automatic provers are bad at finding them today, but we expect that they are going to get better at them over time. Humans are usually pretty good about providing them, or at least identifying an example that the prover can relatively easily prove, so we don’t think this is such a big problem. More importantly, if you care whether or not something is true, you should specify what you actually require; otherwise, the specification can be very misleading (you may think you’re proving something you aren’t). If you intend for something to exist, then you should specify it.

We have implemented the “allsome” quantifier in the Metamath Proof Explorer, including some formal proofs about its properties, and it works exactly as you would expect. For example, we can prove that ∀! x (xA→ψ) ↔ ∀! xA ψ [alsconv]. Perhaps even more importantly, we can prove that the “surprise” shown earlier cannot ever happen with allsome, specifically, we can prove that ¬(∀! x (φ→ψ) ∧ ∀! x (φ→¬ψ)) [alsi-no-surprise]. Thus, the “allsome” quantifier is already implemented and has been rigorously proven to have the properties it was designed to have.

Alternatives

Of course, we are not the first to notice this problem. Here we note two alternative approaches.

PVS TYPE+

Prototype Verification System (PVS) was developed for the development and analysis of formal specifications, and it has special abbreviations to declare non-empty types. An uninterpreted type or subtype declarations introduced with the keyword TYPE may be empty, while an uninterpreted type declarations introduced with the keyword NONEMPTY TYPE or simply TYPE+ are assumed to be nonempty. Uninterpreted subtype declarations introduced with the keyword NONEMPTY TYPE or TYPE+ are assumed to be nonempty, as long as the supertype is nonempty. This means that simply adding + after the word TYPE eliminates possibility of that type being empty. For more information, see [Owre 2001] section 3.1.5.

However, this PVS mechanism only works for that specific type, and if an expression does not use such a type for its antecedent, this approach does not help. So while it can deal with a few narrow situations, it is not as general an approach as allsome.

SPARK dead branch warning

SPARK is a programming language, verification toolset, and a design method which together “ensure that ultra-low defect software can be deployed in application domains where high-reliability must be assured, for example where safety and security are key requirements”. This is especially useful in embedded systems where performance is critical. Intro to SPARK is an interactive introduction to it. SPARK makes it possible to mathematically prove that a program will do certain things given certain assumptions. Of course, if the specification is wrong, then what it proves won’t be what was intended.

In 2018 SPARK implemented a warning that can often detect that a “branch” in a logical formula is “dead” - including when an implication in a for-all has an antecedent can never occur. This warning (when enabled) is implemented by calling SMT provers to detect the potential problem; they are given a 1 second timeout and only report when they can prove that that there is a dead branch.

Yannick Moy developed and sent me a little specification in November 2018 that specifies the Martian propositions in SPARK (see martians.ads). As expected, when sent the Martian propositions SPARK can easily prove them:

martians.ads:10:19: info: assertion proved
martians.ads:11:19: info: assertion proved

However, when SPARK is given the switch “--proof-warnings” to activate the warnings, SPARK also reports:

martians.ads:10:66: warning: unreachable branch
martians.ads:11:66: warning: unreachable branch

This warning mechanism has many advantages:

However, it also has disadvantages:

Working together

There isn’t any need to pick just one or the other. The allsome quantifier can provide guarantees for certain circumstances. PVS can expressly state that certain types exist. Warnings, such as those that can be provided by SPARK, can help detect problems in many other circumstances. Countering defects requires a range of approaches, not any one; all of these approaches can work together.

Conclusions

Specification errors can be a serious problem, so we think that systems should use a variety of mechanisms to reduce the likelihood of errors. Those include providing notation that more closely maps to common informal constructs and detecting constructs that are likely to be misstatements.

The new allsome quantifier does not eliminate all specification errors by itself, but it does help counter one common kind of mistake by providing notation that more directly represents a common informal construct. We expect that the allsome quantifier would be part of a larger suite of measures to counter common mistakes. Here are some examples of other mistakes and ways they can be countered:

We hope that this new allsome quantifier will help reduce the risk of creating formal expressions that appear to be correct but in fact are mistranslations. In addition, we hope that others will eventually agree that allsome is awesome.

References


Feel free to see my home page at https://dwheeler.com. You may also want to look at my paper Why OSS/FS? Look at the Numbers! and my book on how to develop secure programs.

(C) Copyright 2018 David A. Wheeler. Released under Creative Commons Attribution-ShareAlike version 3.0 or later (CC-BY-SA-3.0+).