*
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.
*

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.)

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 *X*s
*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:

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* (*x*∈*A*→ψ)
↔
∀! *x*∈*A* ψ
[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.

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

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 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:

- It works with existing quantifiers.
- It can detect other kinds of problems where something is unreachable.
- It technically has no false positives. The warning “is only triggered if the prover can prove that a branch is dead. So you’ll still get false positives in the sense that people may not be interested in that specific warning (“OK it’s dead for that configuration but not another one” for example), but it will always point to an actual dead branch.” (Yannick Moy).

However, it also has disadvantages:

- There is no
*guarantee*that it will report a problem. The warning is only reported when it can guarantee that there is a dead branch, and in more complex circumstance this may not be detected. In short, there are no false positives (all reports are real), but there can be false negatives (some problems might not be reported). - Enabling these warnings takes a noticeable amount of time on larger programs, and thus is not the default. Yannick Moy reports, “there is a price to pay for such a proof-based warning: calling a prover. Right now we make this quite small, with 1 second timeout only for these special calls, but this is still noticeable on large programs with many branches to check (plus we already have in fact a few others of these proof-based warnings, on preconditions or postconditions that are always false and dead code after loops). This is why we’ve not made it the default but a separate switch. The customer who asked for this feature has made it the default configuration of the tool.”
- In general, the warning is not as powerful as allsome in cases where allsome is useful - there is no guarantee that the warning will show in dangerous cases, while allsome formally specifies that something must exist.

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.

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:

- Another common kind of error is using implication directly within an
exists quantifier (the form ∃
*x*(φ→¬ψ)). This is almost always a mistake (usually the implication → should be logical conjunction aka “and” aka ∧). Both Why3 and SPARK already have a built-in warning if there is an implication used directly within an exists quantifier. It does not even need to be built-in; a separate style checker could warn when this particular combination (∃ with →) occurs since it is practically never intended. - Paul E. Black noted that an implementation is typically checked against a specification by proving that the implementation implies the specification; this ensures that the implementation only has behaviors allowed by the specification, but it does not require the implementation to have any behavior at all. He suggests that correctness statements have two parts, corresponding to liveness and safety. Safety shows that the implementation implies an "allowed-behavior" specification, while liveness shows that a "required-behavior" specification implies the implementation. For more, see [Black 1999].

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.

- [Aristotle]
Aristotle,
*Posterior Analytics*, II.7.92b6-8 (translation by Mure), c. 300s BC. - [Black 1999] Black, Paul E., "Is 'Implementation Implies Specification' Enough?", presentation to 12th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'99), Nice, France, (September 1999).
- [Groarke]
Groarke,
"Aristotle: Logic",
*Internet Encyclopedia of Philosophy (IEP)*. - [Owre 2001]
S. Owre, S., N. Shankar, J.M. Rushby, and D.W.J. Stringer-Calvert,
*PVS Language Reference Manual*, Version 2.4, November 2001, section 3.1.5 (Empty versus Nonempty Types).

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+).