2026-07-13 (originally 2018-10-20)
Abstract: It is easy to mistranslate informal statements into formal logic. These errors can cause serious problems, potentially including property damage, maiming, and loss of life. For example, in formal logic, “All Martians are green” is typically represented by the pattern ∀x (φ→ψ), while “All Martians are not green” is typically represented as the pattern ∀x (φ→¬ψ). In formal logic both statements are simultaneously true if there are no Martians. However, informal statements of this form typically assume 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 these mistranslations less likely. The allsome quantifier, abbreviated ∀∃, simultaneously expresses for all (∀) and there exists (∃). It has two syntactic forms, formally defined as follows: ∀∃ x (φ→ψ) ≡ (∀x (φ→ψ)) ∧ ∃x φ and ∀∃ x∈A (φ→ψ) ≡ (∀x∈A (φ→ψ)) ∧ ∃x∈A φ. Now “All Martians are green and there is at least one Martian” is easily expressed as the first form, ∀∃ x (φ→ψ). 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. 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.
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 be 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” is usually formally represented using the pattern ∀x (φ→ψ), which means for all x, if φ is true then ψ is true. Here φ and ψ represent true-or-false formulas, each of which may depend on x. A specific representation could be ∀x (martian(x)→green(x)), where martian(x) is true if and only if (iff) x is a Martian and green(x) is true iff x is green. Similarly, “All Martians are not green” is usually formally represented using the pattern ∀x (φ→¬ψ), that is, for all x, if φ is true then ψ is not true. A specific representation could be ∀x (martian(x)→¬green(x)). Here we use the traditional symbol ¬ for “not”.
The problem happens if there are no Martians. In formal logic, non-existence in general can be represented as ¬∃x φ (“there does not exist…”). This specific situation can be represented as ¬∃x martian(x), that is, “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” as written above 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 ¬φ ∨ ψ, where ∨ is the traditional symbol for “or”. 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.
This is not a hypothetical concern; it has been measured. Beer and colleagues at IBM, reporting on several years of hardware verification, found that “during the first formal verification runs of a new hardware design, typically 20% of formulas are found to be trivially valid, and that trivial validity always points to a real problem in either the design or its specification or environment” [Beer 2001, p. 141]. The specific cause they name is an unsatisfiable antecedent, which earlier work called antecedent failure. Beatty and Bryant, who named it, put the danger memorably: “Formally, implications have an extensional meaning: they are also true if the antecedent condition is not true. Antecedent failure means that we can speak nonsense and not realize it.” [BeattyBryant, section “Observations”]. Their setting is temporal logic rather than first-order logic, and they include many issues not just this one. Still, their example is AG(request → AX ack) [Beer 2001, p. 142] (“in every state, if there is a request then an acknowledgement follows”). Their example domain is time not Martians, but this is the same shape as ∀x (φ→ψ) with an antecedent nothing satisfies, and it fails for exactly the same reason.
There is also evidence about the people, not just the formulas. Greenman and colleagues studied how well people understand linear temporal logic (LTL), and found that translating from English into formal notation was the most common source of errors. They found 47% of responses were incorrect from students (rounds 2 and 4), and a shockingly high 28% of responses were incorrect (round 3) from researchers with prior exposure to LTL [Greenman 2023, section 8]. As they put it, this is “the critical authoring direction in which a subtle mistake can lead to a faulty system”. This included BadProp, responses that “mis-use a logical operator or an atomic symbol”. They specifically recommend that designers “directly address misconceptions by changing the logic”, including adding new operations to correctly express common situations. That is exactly the approach allsome takes.
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.
In our experience, the problem is that formal logic notation lacks a simple way to notate a common informal expression. As noted by [Parsons], “Most English speakers tend to understand ‘Every S is P’ as requiring for its truth that there be some Ss... Every modern logic text must address the apparent implausibility of letting ‘Every S is P’ be true when there are no Ss.” This goes back to at least [Aristotle], who expressly and intentionally excluded empty sets from his logic system [Groarke].
Barwise and Etchemendy, in a widely-used textbook on translating informal language into formal logic, call these “vacuously true generalizations” and note that in everyday conversation we hardly ever encounter one: “when we do find either of these, we feel that the speaker has misled us” [BarwiseEtchemendy, section 9.6]. Their example is a professor who says “Every freshman who took the class got an A” when in fact no freshman took her class. She has not lied, exactly, but she has misled us, because her statement “typically carries the conversational implicature that there were freshmen in the class”.
Other textbooks on translating informal language into formal logic warn about the same trap. The open textbook forall x points out that ∀x (R(x)→M(x)), read as “every refrigerator is a monkey”, is true when the domain contains no refrigerators, and calls that result “counterintuitive”; it states the rule plainly, that “when F is an empty predicate, any sentence ∀x (F(x)→…) is vacuously true” [forallx, section 24.2]. Discussing a different example, it notes that the formal rendering “would be trivially true” if the antecedent had no instances, and adds the sentence we would underline if we could: “This is not what we want”.
There is no way to simply express this common informal statement in modern formal logic notation when using a single standard quantifier. The closest is repeatedly adding “and” and an extra “exists” statement every time, but this is absurdly complicated when dealing with real systems with many assertions and many long expressions within them. It’s also easy to forget. This lack of a simple way to formally represent a common kind of informal statement can lead to dangerous mistakes.
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 general case that applies to a top-level implication, and a bounded case that applies a top-level implication to the members of a class or set A. Here are their formal definitions, where ∧ is the traditional symbol for “and”:
For example, if we now write “All Martians are green” using the pattern ∀∃ x (φ→ψ), say as ∀∃ x (martian(x)→green(x)), we are simultaneously asserting that all Martians are green and that there is at least one Martian. Similarly, “among Martians, all tall ones are green” can be written as ∀∃ x∈martians (tall(x)→green(x)), and this can only be true if there is at least one tall Martian and all tall Martians are green. These are almost certainly what the speaker actually meant; it should be easy to say what is usually 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 because many readers can correctly guess its meaning without any explanation: it simply places the “for all” (∀) and “there exists” (∃) symbols next to each other, which is exactly what the quantifier combines. It also leaves room to append the modifiers that some systems add to “there exists”, which we look at in variants of “there exists”. We’re flexible about its exact typography; options include having the two traditional symbols adjacent to each other (∀∃), cuddling them together (∀∃), or using a merged symbol (∀∃). You can easily use it today in many cases just by writing the two symbols next to each other, but see below if you are interested in other options (including HTML, fonts, TeX, and so on).
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 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 the bounded form is simply the general form with membership folded into the antecedent, ∀∃ x∈A (φ→ψ) ↔ ∀∃ x ((x∈A ∧ φ)→ψ) [dfrals2]. Perhaps even more importantly, we can prove that the “surprise” shown earlier cannot ever happen with allsome, specifically, we can prove that ¬(∀∃ x (φ→ψ) ∧ ∀∃ x (φ→¬ψ)) [als-no-surprise]. The same holds for the bounded form, ¬(∀∃ x∈A (φ→ψ) ∧ ∀∃ x∈A (φ→¬ψ)) [rals-no-surprise], and note that this needs no assumption that A is nonempty; that is precisely the point.
Allsome also delivers something that the ordinary for-all does not. If all Martians are green and there is at least one Martian, then something is green: we can prove ∀∃ x (φ→ψ) → ∃x ψ [alsex], and likewise for the bounded form [ralsex]. From ∀x (φ→ψ) alone, nothing whatsoever follows about ψ. So the no-surprise property shows that allsome cannot say something contradictory, while this shows that it does say something useful. Thus, the “allsome” quantifier is already implemented and has been rigorously proven to have the properties it was designed to have.
You never need a special symbol or specialized typesetting to use allsome. You can put the widely-available “for all” and “there exists” symbols adjacent to each other: ∀∃. We’re flexible about its exact typography, but if you prefer, you can cuddle the two symbols together, or use a single merged allsome symbol. Here is what the three options look like, enlarged so that their differences are easy to see:
All three are acceptable, and they all mean the same thing. The adjacent form needs nothing at all, so if you just want to start using allsome quickly, you already can, and the rest of this section is optional. If you want one of the fancier forms, the subsections below explain how: you can cuddle the symbols using HTML and CSS, merge them using a font (which works in HTML, word processors, and many other tools), or merge them using TeX. All of these are workarounds for the fact that allsome currently has no character of its own, so we close by looking at the longer road: a Unicode assignment.
If you would like allsome to be the single cuddled symbol ∀∃ using simple HTML and CSS, without adding a font, you can nudge the second symbol slightly to the left with a negative CSS margin. Wrap the pair like this:
<span class="allsome">∀<span>∃</span></span>
and add this rule to your stylesheet:
.allsome span { margin-left: -0.18em; }
Adjust the value to taste. It is worth knowing what the value is actually cancelling. The gap you see between ∀ and ∃ is not spacing that CSS added, so no amount of zeroing margins or padding will remove it. It is built into the glyphs themselves: each one carries a little blank space on either side, called its side bearings, so that adjacent characters do not collide. The visible gap is the right bearing of ∀ plus the left bearing of ∃, and in common serif fonts that comes to roughly 0.06em to 0.11em. So a nudge of about -0.1em brings the two strokes to just touching, and larger values overlap them; this page uses -0.18em, which gives the cuddled form shown above.
Because the nudge is measured in em, it is proportional to the font
size, so one value stays right at every size; the enlarged samples above use
exactly the same rule as the running text.
Unfortunately, it is not proportional to the font’s design.
Fonts differ in how much bearing they give these two glyphs, and CSS offers no
unit that measures it, so the nudge is always cancelling a quantity it cannot
see.
A value tuned for one font may be slightly loose or slightly tight in another,
especially if the reader’s font lacks ∀ and ∃ and the browser substitutes
them from somewhere else.
If you want a join that is reliable no matter what font is in use, don’t nudge
at all; instead, use a single merged glyph, as described next.
There is a simpler variant: put both symbols in a single span and use
negative letter-spacing instead of a margin on a nested span.
<span class="allsome">∀∃</span>
.allsome { letter-spacing: -0.18em; }
We don’t suggest this, however.
letter-spacing applies its spacing after every
character, including the last one, so it also chops off the space to the
right of the “there exists” symbol and pulls whatever follows
(such as the variable) too close.
The negative-margin approach above closes only the gap between the two
symbols and leaves the trailing space intact.
If you want to use the merged symbol, the obvious solution is to use a font. This works in HTML, word processors, and many other tools. However, it requires that you download such a font and apply it where you use it.
We have implemented a special font (CC0 license) where if you have the character ∀ followed immediately by ∃ it will show ∀∃. The two characters must be immediately next to each other, and it is best to apply the font to just those two characters.
We provide the font in two formats, both released under CC0, so anyone may use them. They are small files; the font has only a few glyphs in it. Use allsome.woff2 on a web page; that is the format browsers want, and it is the more compact of the two. Use allsome.ttf to install the font in a word processor or in your operating system, since those want TrueType and cannot use a WOFF2 file. The two contain exactly the same glyphs.
We also provide the program that generates them, build_allsome_font.py. It draws every glyph from scratch, so the font contains no outlines taken from anyone else, which is what lets us release it under CC0 in the first place. It writes the TrueType file and then derives the WOFF2 from it, so the two can’t drift apart. You don’t need it to use the font, but it’s there if you want to check how the font was made or rebuild it yourself.
Using such a font in HTML takes three steps and needs no JavaScript.
First, put allsome.woff2 on your site.
Second, declare it in your CSS with an @font-face rule and
define a class that applies it:
@font-face {
font-family: Allsome;
src: url("allsome.woff2") format("woff2");
font-display: swap;
}
.allsome-font { font-family: Allsome, serif; }
Third, wrap an adjacent “for all” and “there exists” in a span that uses that class:
<span class="allsome-font">∀∃</span>
The font’s ligature then replaces that pair with the single merged glyph, so it displays as ∀∃. It is cleanest to apply the font only to the allsome pairs. Applying it more broadly is harmless in the sense that the font also contains ordinary ∀ and ∃ glyphs, so a lone ∀ or ∃ still renders as a normal symbol and only an immediately adjacent pair merges, but those lone symbols would then use this font’s glyphs instead of whatever font you would otherwise have chosen for them. If the font does not load for some reason, the two characters simply appear adjacent, which is a reasonable fallback.
We recommend including font-display: swap in the
@font-face rule, as shown above.
Without it browsers apply the default (font-display: auto,
which they implement as block), and while the font is still
loading they render text that uses it as
nothing at all for up to about three seconds.
A reader on a slow connection would see a blank space where the allsome
symbol should be.
With font-display: swap the browser immediately shows the
fallback, so the two symbols appear adjacent right away and are
replaced by the merged glyph as soon as the font arrives.
That also makes the loading case behave like the failure case described
above, which is what a reader would expect.
If you use TeX (including LaTeX), you can make ∀∃ appear as a single merged symbol, like this: ∀∃.
We have implemented
a robust, scale-aware \allsome command with the
TikZ package.
It draws a merged “for all” and “there exists”
symbol and sizes itself for display, inline, script, and script-script
math styles. It is CC0-licensed, so you can use it without licensing issues.
Download the TeX allsome command (CC0 license)
With this definition,
∀∃ x (φ→ψ)
can be written in TeX as
\allsome x\,(\phi \rightarrow \psi).
All of the approaches above are really workarounds. There is currently no Unicode code point for allsome, so we must either accept two adjacent characters or arrange for something (CSS, a font, or a TeX macro) to draw them as one. In the long term it’d be good to get a new Unicode assignment for this symbol, so that anyone could type and display it anywhere with no font, no stylesheet, and no macro.
That’s a longer road. Unicode generally wants evidence that a symbol is already being used before it will assign a code point to it. So the way to get there is to start using allsome now, using whichever of the approaches above suits you.
Some systems extend “there exists” by appending a character to it. If a system provides those extensions, it should provide them for allsome as well.
The common one is ∃!, “there exists exactly one” [BellMachover, Definition 10.1, p. 97; WhiteheadRussell, *14.02, p. 175; Metamath df-eu]. Some also have ∃*, “there exists at most one” [BellMachover, p. 460; Metamath df-mo]. Metamath provides forms of each restricted to a class as well (df-reu and df-rmo).
The natural way to extend allsome is to append the same character, and let it modify allsome’s existence conjunct. Nothing else changes. For example:
and likewise with ∃* in place of ∃!.
∀∃! is genuinely useful. Since exactly one x satisfies φ, saying that all φ are ψ says that that one thing is ψ. So ∀∃! x (martian(x)→green(x)) says: there is exactly one Martian, and it is green.
This is exactly what the English word “the” usually does. “The king is hungry” claims that a king exists, that there is only one, and that he is hungry. Russell analyzed such definite descriptions with exactly this apparatus [WhiteheadRussell, *14.02]. Now, however, we can succinctly describe it: ∀∃! x (king(x)→hungry(x)). The bounded form covers the restricted case: ∀∃! x∈martians (tall(x)→green(x)) says that exactly one Martian is tall and that it is green, which is to say “the tall Martian is green”.
The reason to care is the reason that motivates allsome, only more so. Write “the king is hungry” as ∀x (king(x)→hungry(x)) and you silently drop both claims: it is vacuously true when there is no king, and it says nothing about how many kings there are.
∀∃* says that there is at most one X, and that any X there may be is Y. In English that is the definite article without requiring existence: “the king, if there is one, is hungry”. That is less common, but it is a real thing to want to say. It is not the same as an ordinary for-all: ∀x (φ→ψ) says nothing about how many x satisfy φ, so ∀∃* is a stronger claim.
We do have a caution about ∀∃*. “At most one” is satisfied by having none, so ∀∃* deliberately permits there being none, and it is therefore true when nothing satisfies φ. If you want protection against vacuous truth, you want ∀∃ or ∀∃!.
This section defends the case for allsome instead of advancing it, so if you are already convinced, you can skip ahead without losing the thread. Each subsection takes up an objection or an alternative and answers it: how allsome fares in logics other than the classical one, whether one kind of quantifier could do the job of two, why we did not instead abandon material implication, and what allsome asks of automated provers.
We have even considered the case where someone uses intuitionistic logic instead of classical logic. Allsome works there too.
First, the problem is just as real in intuitionistic logic. The left-hand side of a material implication is often a predicate that checks for set membership. If that set is empty (e.g., there are no Martians), then we immediately have the problem we are describing.
The reason is not quite the one we gave earlier, though, so it is worth spelling out. Above we explained the surprise by noting that (φ→ψ) is equivalent to ¬φ ∨ ψ. That full equivalence is classical: the direction from (φ→ψ) to ¬φ ∨ ψ is not intuitionistically valid. The surprise, however, needs only the other direction, from ¬φ to (φ→ψ), and that direction does hold intuitionistically. To see why, recall what → means constructively: a proof of (φ→ψ) is a construction that converts any proof of φ into a proof of ψ. Suppose nothing satisfies φ, that is, suppose we have ¬φ, so a proof of φ would yield absurdity (written ⊥, and also called falsity or the absurd proposition). Then the required construction is trivially available. Given a supposed proof of φ, derive ⊥, and from ⊥ derive anything at all, including ψ. That last step is the principle called ex falso quodlibet (“from falsity, whatever you like”), which says that ⊥ → p for every proposition p. Intuitionistic logic accepts it. So (φ→ψ) holds for every x, and ∀x (φ→ψ) is provable. Both “All Martians are green” and “All Martians are not green” are therefore provable when there are no Martians, exactly as in classical logic. The surprise is not an artifact of classical truth tables. It follows from the meaning of implication together with ex falso quodlibet. That last principle is enough to get both halves of the surprise, though, as we will see next, it is not strictly needed for the “are not green” half.
What changes is the remedy. In classical logic you could instead assert that the set is not empty, as that has the same meaning in classical logic. In intuitionistic logic there is a subtle distinction: knowing a set is not empty is not the same as knowing that a set has an element (aka an “inhabited” set). Being inhabited implies being nonempty (see n0rf), but the converse does not hold constructively. Saying a set is “not empty” amounts to ¬¬∃x x∈A, and getting ∃x x∈A from that requires double negation elimination, which intuitionistic logic does not have.
Allsome asserts the stronger of the two. Its definition, (∀x (φ→ψ)) ∧ ∃x φ, uses only ∧, ∀, ∃, and →; it appeals to neither the law of the excluded middle nor double negation elimination. So the definition may be carried over to intuitionistic logic unchanged, and it retains its intended force there: its existence conjunct ∃x φ is the constructive existential, which demands an actual witness satisfying φ. It does not degrade into the weaker claim that no such witness can fail to exist. We intentionally chose the stronger “is inhabited” form as we believe it’s easier to work with and more consistent in practice with what is meant by informal statements.
Allsome’s central property is constructively provable as well. Here is a sketch: suppose both ∀∃ x (φ→ψ) and ∀∃ x (φ→¬ψ) hold. The first supplies a witness a satisfying φ. The two universals then yield ψ(a) and ¬ψ(a), hence ⊥. So the two cannot both hold: the surprise that allsome is meant to prevent cannot arise. Every step of that argument is intuitionistically valid.
The argument above raises a natural question: what about a logic that does not accept ex falso quodlibet? If we can show allsome works appropriately in this case, then that is an argument that it is a useful general quantifier.
Minimal logic is intuitionistic logic with exactly that principle removed. There, ⊥ is an ordinary proposition: ⊥ → p is simply not available, so from ⊥ you may not derive an arbitrary p. The derivation given earlier then breaks down. From ¬φ and φ we can still reach ⊥, but we can go no further, so ¬φ no longer yields (φ→ψ) for an arbitrary ψ. In minimal logic, “there are no Martians” no longer proves “All Martians are green”.
The vacuity does not disappear entirely, however, and the half that remains is easy to overlook. Proving (φ→¬ψ) never needed ex falso quodlibet in the first place. Recall that ¬ψ is simply (ψ→⊥). Assume φ; with ¬φ that gives ⊥. Now assume ψ; we already have ⊥, so we may discharge ψ and conclude (ψ→⊥), that is, ¬ψ. Discharging φ then gives (φ→¬ψ). Every step is ordinary implication and negation introduction: we derived ⊥, but we never derived anything from ⊥. So in minimal logic “there are no Martians” still proves “All Martians are not green”.
Minimal logic therefore removes the positive half of the surprise, but it leaves the negative half standing. The two statements can no longer both be derived from “there are no Martians”, so the paired surprise that opened this essay does not arise. But a vacuously true statement is still provable, and it still isn’t what the speaker meant. This also helps sharpen the diagnosis. The positive half of the surprise depends on ex falso quodlibet, while the negative half needs nothing beyond the meaning of implication and negation. Weakening the logic won’t remove it.
So in minimal logic, using allsome makes it easier to prevent a real defect. Written with allsome, “All Martians are not green” becomes ∀∃ x (martian(x)→¬green(x)), which by definition also requires ∃x martian(x). With no Martians it is simply not provable, vacuously or otherwise. That is exactly the protection we want, and it is the same protection allsome gives classically.
The abbreviation is available in minimal logic, too: our definition uses only ∧, ∀, ∃, and →, every one of which minimal logic provides. And the original motivation is untouched. It remains a common thing to mean both “all X are Y” and “there is at least one X”, and saying that easily still takes two quantifiers.
Finally, allsome’s no-surprise property still holds here, and its proof needs nothing that minimal logic lacks: a witness a satisfying φ yields ψ(a) and ¬ψ(a), hence ⊥, and discharging the assumption gives the negation directly. That last step is ordinary negation introduction, which minimal logic has. Once again the argument derives ⊥ but never derives anything from ⊥. So allsome’s guarantee doesn’t secretly depend on ex falso quodlibet, and it isn’t an artifact of the surrounding logic. It holds in the classical, intuitionistic, and minimal cases alike.
We should be clear about what is and is not machine-checked. Allsome is defined, and its properties are proven, in the classical Metamath Proof Explorer; we haven’t yet defined it in the Intuitionistic Logic Explorer. Both arguments above, for intuitionistic and for minimal logic, are therefore sketches rather than formal proofs. Formalizing allsome in those logics is future work, and we expect it to be straightforward.
We said earlier that expressing this common statement takes two different quantifiers, or other contortions. A pedant could object that in classical logic the two quantifiers are interdefinable: ∃x φ is equivalent to ¬∀x ¬φ. So we could write the general form of allsome using the for-all quantifier alone: ∀∃ x (φ→ψ) ≡ (∀x (φ→ψ)) ∧ ¬∀x ¬φ.
The objection is technically correct, but it doesn’t help in practice. That expression uses only one kind of quantifier, but it is harder to read, not easier: to recover the simple idea “some x satisfies φ” the reader must now decode a double negation, “it is not the case that every x fails to satisfy φ”. Our complaint was never that this meaning cannot be expressed at all. Our complaint is that it cannot be expressed simply, and this substitution makes matters worse, not better.
It is also worth noting that this rewrite is available only in classical logic. Intuitionistic logic does not equate ∃x φ with ¬∀x ¬φ; the latter is strictly weaker. In fact it is exactly the weaker notion we met earlier. Since ¬∃x φ and ∀x ¬φ are intuitionistically equivalent, negating both gives ¬∀x ¬φ ↔ ¬¬∃x φ, the double-negated existential. That is the “not empty” claim, not the “is inhabited” claim. So the one-quantifier rewrite would quietly replace allsome’s requirement that some x actually satisfies φ with the weaker claim that φ is not false of everything, and no witness need be produced. Outside classical logic, then, this rewrite doesn’t just cost readability; it changes the meaning, which is far worse.
A key part of the problem stems from how the logic operation material implication (→) sometimes differs from informal language. It is possible to drop the normal logic operation called material implication, but most people (including us) believe dropping material implication would not be an improvement.
[Suber 1997] notes that in English there are “many kinds of implication... the first step in becoming comfortable with material implication is to realize that, precisely because it’s just one kind of implication, it cannot capture every use of the English ‘if...then’ or ‘implies’... Material implication sometimes violates our intuition, but it is valuable because it creates a ‘truth-functional kind of implication’ which brings many substantial benefits.”
This debate about the meaning of implication is an old debate. Philo the Dialectician (who flourished around 300 BC) was a dialectic Greek philosopher of the Megarian school. (The Megarian school was a predecessor to and influencer of later Stoic logic; Zeno, who founded Stoicism, was a friend and admirer of Philo.) Philo interpreted the conditional (“if... then”) as material implication: “the conditional is true when it does not begin with a true proposition and finish with a false one, so that a conditional, according to him, is true in three ways and false in one way.” [Empiricus, 2.113]. Philo’s teacher, the Greek philosopher Diodorus (died c. 284 BC), disagreed with Philo. Diodorus said that “a conditional is true which neither was nor is able to begin with a true one and finish with a false one”. Thus, a statement like “If it is day, I am having a discussion” when it is day would be true for Philo but “false according to Diodorus. For it is able to begin with the true ‘It is day’ and finish with the false ‘I am having a discussion’ (when I have become quiet), and it was able to begin with a true one and finish with the false ‘I am having a discussion.’ ” [Empiricus, 2.115]. So even around 300 BC there was a debate about the meaning of implication. Sextus Empiricus could still point to this disagreement as an unresolved debate around the second century AD [Empiricus, 2.113-2.115].
Some logicians have been disturbed by material implication, so they “have developed so-called ‘relevance logics’ in which the antecedent and consequent of conditionals must somehow bear on the same subject.” However, while interesting, relevance logic has not widely caught on. As Suber notes, “(1) The perversity of material implication is deliberate, for it is the only way to get truth-functionality. (2) But the perversity violates only our ordinary expectations, not any logical principles. (3) For material implication, despite its perversity, suffices to capture the logically essential core of meaning in ordinary uses of implication. The nuances of English that it does not translate do not affect validity (in standard logic). (4) Hence, the price is worth paying, for the counter-intuitive material implication distorts nothing essential and, because it is truth-functional, allows us to test the validity of arguments that contain implication statements.” He also notes that this is not a defect peculiar to material implication: because English has so many kinds of implication, no other single version could express English statements precisely either.
There has been work to define and model causality (as opposed to material implication). This work is important in the real world, but also complex. The book Actual Causality [Halpern 2016] discusses (real-world) actual causality and proposes a family of definitions for actual causality. It is interesting, but the fact that it takes a whole book to deal with it suggests that there are good reasons mathematicians would choose something else.
As [Edgington] notes, “The truth-functional theory of the conditional was integral to Frege’s new logic (1879). It was taken up enthusiastically by Russell (who called it ‘material implication’), Wittgenstein in the Tractatus, and the logical positivists, and it is now found in every logic text. It is the first theory of conditionals which students encounter. Typically, it does not strike students as obviously correct. It is logic’s first surprise. Yet, as the textbooks testify, it does a creditable job in many circumstances. And it has many defenders. It is a strikingly simple theory: ‘If A, B’ is false when A is true and B is false. In all other cases, ‘If A, B’ is true.”
Thus, we don’t think we should drop material implication. Instead, we should try to find one or more ways to keep material implication while making it less likely to be misused.
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 automatic provers are sometimes bad at finding witnesses today, but we expect that they will get better at finding 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.
Of course, we are not the first to notice this problem. Here we note two other approaches that counter it while retaining material implication: declaring up front that a type is not empty, as PVS does, and detecting vacuity after the fact. If you suspect we are proposing a solution to a problem nobody has, note that tools to detect this have been built since at least 1994 [BeattyBryant], and that they exist in quite different kinds of tool. We look at vacuity detection as it grew up in model checking, and then at the same idea as it appears in SPARK, which proves programs a quite different way.
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 declaration introduced with the keyword TYPE may be empty, while an uninterpreted type declaration introduced with the keyword NONEMPTY TYPE or simply TYPE+ is 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 the 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.
Vacuity detection is a countermeasure that comes from model checking. As we noted earlier, Beatty and Bryant found in 1994 that a formula could be trivially valid because its antecedent was never satisfiable, and named that antecedent failure [BeattyBryant, section “Observations”]. Beer and colleagues generalized the idea to vacuity, covering other kinds of trivial validity as well, and showed how to detect it efficiently. Their definition is that a “formula φ is vacuous in model M if there is a sub-formula ψ of φ such that ψ does not affect φ in M” [Beer 2001, Definition 2]. Kupferman and Vardi gave a general method for detection of vacuity and generation of interesting witnesses for specifications in CTL*, which checks “whether all the subformulas of the specification affect its truth value in the system” [KupfermanVardi, section 1]. The technique rests on a precise notion of a subformula doing no work. A subformula ψ “affects” φ in a model if there is some replacement formula ψ′ for which φ and φ with ψ replaced by ψ′ have different truth values [Beer 2001, Definition 1]. So if ψ could be swapped for anything at all without changing the answer, it did no work, and the formula is vacuous. For a formula that is not vacuous, these tools can also produce an “interesting witness”, which Beer and colleagues define as “a non-trivial example of the validity of the formula” [Beer 2001, abstract].
The idea has been applied in industrial practice at more than one company. Beer and colleagues report on its use at IBM [Beer 2001], and Armoni and colleagues report using vacuity detection on real processor designs at Intel, where they apply such checks “on every specification” and check the important subformulas manually when a full check exceeds capacity [Armoni 2003, section 5.4].
We think this is valuable, and it is an endorsement of our thesis: people built tooling for finding specification defects, and the ones who did report that it kept turning up (recall the 20% figure quoted earlier). But it addresses a different moment in the process than allsome does, and the difference matters:
On the other hand, vacuity detection is more general than allsome in one important way. Its definition of vacuity turns on any subformula failing to affect the result [Beer 2001, Definition 2], not only on an antecedent that nothing satisfies. Allsome is a narrow fix for a specific mistake. Vacuity detection is a broad net for a whole family of them. Neither subsumes the other.
The idea is also not confined to model checking, as the next section shows.
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” (AdaCore has since reworded that page; the quotation is from a 2018 copy). 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.
SPARK has vacuity detection too, although it proves programs by a quite different route: its prover, GNATprove, hands each check to an SMT solver rather than exploring the states of a model. GNATprove will “issue warnings as part of proof, on preconditions or postconditions or pragma Assume that are always false, unreachable branches in complex Boolean expressions (typically in assertions and contracts), dead code at branching points in the program” [SPARKUG, section 7.3]. Read that alongside the definition of vacuity we quoted a moment ago, that a formula is vacuous when some subformula “does not affect” it. A precondition that is always false is an antecedent that nothing can satisfy, so the contract is trivially honored. An unreachable branch inside an assertion is a subformula that cannot affect the result. Same defect, same countermeasure, in a quite different kind of tool.
The part of this that concerns us most directly arrived in 2018, when 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 that 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 there is a dead branch.
Yannick Moy developed and sent us 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:
There isn’t any need to pick just one approach or the other. They fit together naturally, because they act at different moments:
Countering defects requires a range of approaches, not any one; all of these approaches can work together.
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. Here are some examples of other mistakes and ways they can be countered:
But again, the allsome quantifier does not need to solve all common mistakes. Instead, we hope that the allsome quantifier would be part of a larger suite of measures to counter common mistakes.
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.
Older versions of this essay instead used the symbol ∀!, by analogy with the existing ∃! symbol. However, that notation did not convey its meaning to readers who had not already learned it. Even worse, a reader who did know about ∃! might be misled, because there the “!” in that case means “exactly one” (see variants of “there exists”). We changed the symbol to ∀∃ so many could immediately intuit its meaning.
Those older versions that used the symbol ∀! also defined the bounded (second) form differently, as a bare formula applied to the members of a class: ∀! x∈A φ ≡ (∀x∈A φ) ∧ ∃x x∈A (defined in the Metamath token df-alsc). This asserted only that φ holds throughout A and that A has at least one member; it did not require any member of A to satisfy φ. We’ve since changed that second conjunct from ∃ x x∈A into ∃ x∈A φ, where φ is now the antecedent of the implication, so the corrected form requires a member of A that actually satisfies that antecedent. We believe that this older definition of the bounded form was a mistake, for two reasons:
The bare-formula meaning is not lost, only redundant. To say “all members of A satisfy φ, and A has at least one member”, you can still use ∀∃, just use the general form with membership as the antecedent: ∀∃ x (x∈A→φ). By definition that expands to (∀x (x∈A→φ)) ∧ ∃x x∈A, that is, every member of A satisfies φ and A has at least one member. That A is inhabited is not an extra condition we must remember to add; it is exactly what the existence conjunct of allsome already requires. This is precisely what the old bare-formula bounded form asserted, so no separate quantifier is needed for it. Of course, you can still write it the traditional way, using two quantifiers, (∀x∈A φ) ∧ ∃x x∈A, if you are more comfortable with that.
The opposite meaning also remains easy to express. If you want to say only that any members of A satisfy φ, without asserting that A has any members at all, that is the ordinary bounded for-all, ∀x∈A φ, which abbreviates ∀x (x∈A→φ). This is still vacuously true when A is empty. That is sometimes exactly what is meant, and the standard quantifier already says it.
So no option is lost and none is hard to write: use ∀ when you do not care whether A is inhabited, and use ∀∃ when you do. Allsome does not take away a choice; it makes the choice that requires an inhabited set just as easy to say.
Because we changed the symbol at the same time, it is easy to tell which definition an older document is using: ∀! always denotes the old definition, and ∀∃ always denotes the current one.
One more name, for the record: a conversion theorem called alsconv depended on that older df-alsc definition, relating the general form with a membership antecedent to the bare-formula bounded form (again in the older notation), ∀! x (x∈A→ψ) ↔ ∀! x∈A ψ. Both were replaced, and neither exists in the Metamath database any more.
The Metamath labels changed as well. The restricted (bounded) form is now prefixed with r, following the way Metamath names the restricted quantifiers that allsome is built from: ∀ gives df-ral and ∃ gives df-rex, so df-als gives df-rals. The older labels carried a trailing i, for implication, which no longer distinguishes anything now that both forms take an implication. Older references will use the names in the left column below. Those older names no longer exist in the Metamath database, so they are not linked here:
| Older name | Current name |
|---|---|
| df-alsi | df-als |
| df-alsc | df-rals (and corrected, as described above) |
| alsconv | dfrals2 (and corrected) |
| alsi-no-surprise | als-no-surprise |
Take care with the middle two rows. The general form and the no-surprise theorem were only renamed, and state exactly what they always did. The bounded form was not merely renamed: df-alsc and alsconv asserted the older, mistaken definition described above, so anything that relied on them should be re-examined rather than simply relabeled.
--proof-warnings=on switch.
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 David A. Wheeler. Released under Creative Commons Attribution-ShareAlike version 3.0 or later (CC-BY-SA-3.0+).