# Mon, 29 Oct 2018

The allsome quantifier

For over 100 years formal logic has routinely represented ideas like “all Xs are Ys” using something called the “for all quantifier”, abbreviated as ∀. This lets people mathematically represent statements like “All Martians are green”. This is really important today, because these mathematical statements can be used to determine if systems work correctly; in some cases this can be used to save lives.

However, there is a problem. It is easy to mistranslate informal statements into formal logic, and these errors can cause serious problems. For example, in formal logic, the normal way to represent the statements “All Martians are green” and “All Martians are not green” can be simultaneously true (namely, when there are no Martians).

Informal statements with this format often embed the assumption that the situation occurs (that is, that there is at least one Martian). This mismatch between formal logic and informal statements could lead to problems, and conceivably to deaths.

I propose a small solution - 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. I hope that this new quantifier will reduce the risk of mistranslations of informal statements into formal expressions, and that others will eventually agree that allsome is awesome.