Logical Connectives
We now tour the Metamath axioms and theorems.
Sentential Logic with SKI Combinator Calculus
The axioms begin with ax-mp and two other axioms which we call ax-k and ax-s. Here is how we phrase them in Metamath:
| Name | Statement |
|---|---|
| ax-k | ganai broda gi ganai brode gi broda |
| ax-s | ganai ganai broda gi ganai brode gi brodi gi ganai ganai broda gi brode gi ganai broda gi brodi |
| ax-mp | broda & ganai broda gi brode ⇒ brode |
Where do these axioms come from? These are the rules of SKI combinator calculus (WP, nLab, esolangs), a combinatory logic with some nice properties. A combinator is an abstract operation which takes some objects and arranges them into an applicative tree. Those other objects are usually also combinators, and application is ax-mp, so a combinator is ultimately some sequence of applications of ax-k and ax-s.
What are the nice properties of SKI combinators? Well, first, note that K and S are both tautologies (WP, nLab): if we test whether each bridi is true or false, and write out a truth table, then both K and S are always true. They're also admissible in intuitionistic logic, which means that if we imagine each bridi to refer to (classes of) things, then we always obtain more (classes of) things as a result of applying them.
Note that we don't have the identity combinator as an axiom. That's because it can be proved as a theorem, id. This is a nice example of the last nice property of K and S: they are complete for combinatory logic, which means that any other combinator can be built from them. Because of the way we set up Metamath, we can also prove the syllogism form of modus ponens, syl, as its own theorem.
The Five Connectives
We need to set up the five logical connectives in a specific order:
{ganai}{ge}{go}{ga}{gonai}
This is a sort of bootstrapping
process which allows us to define new valsi in terms of old
valsi. In general, once this is set up, a definition will be a {go} bridi
which uses the valsi being defined in its left-hand component but not its
right-hand component. For example, here are two definitions from this section
of the database:
| Name | Statement |
|---|---|
| df-se | go ko'e se bu'a ko'a gi ko'a bu'a ko'e |
| df-du | go ko'a du ko'e gi ro bu'a zo'u ko'a .o ko'e bu'a |
However, we can't use that for the connectives themselves. We don't define
{ganai} at all! It's part of the basis. We add the following axioms, as well
as a suspicious pseudo-definition df-go, in order to achieve our bootstrap:
| Name | Statement |
|---|---|
| ax-ge-le | ganai ge broda gi brode gi broda |
| ax-ge-re | ganai ge broda gi brode gi brode |
| ax-ge-in | ganai broda gi ganai brode gi ge broda gi brode |
| df-go | ge ganai go broda gi brode gi ge ganai broda gi brode gi ganai brode gi broda gi ganai ge ganai broda gi brode gi ganai brode gi broda gi go broda gi brode |
But once this is done, we can define our final two connectives:
| Name | Statement |
|---|---|
| df-ga | go ganai ga brode gi brodi gi broda gi ge ganai brode gi broda gi ganai brodi gi broda |
| df-gonai | go gonai broda gi brode gi ge ga broda gi brode gi naku zo'u ge broda gi brode |
Negation
It is convenient to define negation alongside {gonai}. We define experimental
valsi {cei'i} and {gai'o} for vacuous truth and falsehood respectively,
along with {naku} for negating entire bridi at once:
We also define two essential axioms of negation. ax-sdo defines self-defeating objects and ax-efq is the principle of explosion, also called ex falso quodlibet (WP, nLab).
| Name | Statement |
|---|---|
| ax-sdo | ganai ganai broda gi naku zo'u broda gi naku zo'u broda |
| ax-efq | ganai naku zo'u broda gi ganai broda gi brode |
And we also prove several classical tautologies:
Other Axioms
This section includes several axioms whose full potential is not yet unlocked, but whose inclusion couldn't be postponed to the discussion on non-logical connectives. There are axioms of first- and second-order universal quantification: