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 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:
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.
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 me) believe dropping material implication would not be an improvement.
[Suber1997] 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. 284BC), 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 this, and Sextus Empiricus could point to this disagreement as an unresolved debate around the second century AD [Empiricus, 2.113-2115].
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 in English there are “many kinds of implication... [so] no other specific version of implication can [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, I 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.
Of course, we are not the first to notice this problem. Here we note two alternative approaches to counter this problem while retaining material implication.
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:
However, it also has disadvantages:
There isn’t any need to pick just one approach or the other. The allsome quantifier can provide guarantees for certain circumstances. Techniques like the one used in PVS can expressly state that certain types exist. Warnings that try to detect common mistakes (without guaranteeing their detection), 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:
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.
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+).