(Last edited May 11th, 2022 -JH)
Axioms
You have to start somewhere when dealing with a new area of math or logic. In the western tradition, this is often done with axioms (αξιώματα, classical Greek: worthy, later Greek: fitting). Axioms are, theoretically, statements about the topic that are so obvious that they need no proof. And (hopefully) they allow you to prove ANY valid statement in the system in question, and nothing that is not valid in the system.
Euclid (Εὐκλείδης) of Alexandria pioneered this with geometry around 300 BC, or so. He wrote a series of books on it that are still in print, and have been translated in quite a few languages. David Hilbert formalized axiomatic proofs for logic ("Hilbert style proofs"), and once you have logic you can define all mathematics subject to the usual arguments of exactly which axioms and definitions to use. [As shown by Russell and Whitehead in "Principia Mathmatica"] Computer theorem provers are usually working in axiomatic systems of one sort or another.
Basics:
Notation: I give axioms and theorems as axiom in Łukasiewicz notation, often called Polish Notation, a slash ("/"), and then the infix notation that I suspect more of my readers are more
used to. For example the axiom of Modus Ponens is:
CpCCpqq / p -> ((p->q) -> q)
An axiomatic basis for a system has a number of parts. There are rules of inference, and axioms.
The default rules of inference are usually Modus Ponens (MP), and Uniform Substitution (US). If you have those two, you provably also have a rule called Condensed Detachment (CD) that is easier to use for computers and almost subsumes both.
Modus Ponens says that if you have a theorem of the form
Cpq / p -> q
and you have p, then you also have q.
This is also called "Detachment".
Uniform Substitution says that you can substitute anything well formed in for a variable in a theorem as long as you substitute the exact same thing for each and every occurrence of it. (I'm really oversimplifying here, sometimes one set of rules and an axiom basis can be the same as another set of rules and other axioms.) There are also other rules used in specialized study of (usually unusual) systems.
As an example, using the usual rules, the axioms for the (implicational fragment of) positive propositional logic are often given as:
S: CCpCqrCCpqCpr / (p->(q->r))->((p->q)->(p->r)) K: CpCqp / p->(q->p)
There is, in general, no "one true axiomatic basis" of a logic system. A logic can have MANY different collections of axioms that describe exactly some given system, and nothing else. These collections are called an axiomatic bases for the logic systems. For example, the collection of everything the logic can prove is an axiomatic basis, albeit one with a countable infinity of axioms. A convention that cuts the universe of bases down quite a bit is to only worry about bases that have no "redundant" axioms.
A redundant axiom is one that can be proven by the other axioms. If it is redundant, why have it at all?
Removing it means one less case to worry about when doing proofs about the system.
*** EDITING NOTE. Some text has vanished here, probably an editing error.
*** I'm working to find the block of text that went here.*** -JH
CCCpqrCsCCqCrtCqt / ((p→q)→r)→(s→((q→(r→ t))→(q→t)))
(This is from Carew A. Meredith, and it is a shortest single axiom for HI (The implicational fragment of the intuitionist logic] system. (see below)
Another basis for this logic that is quite common is:
B: CCpqCCrpCrq / (p->q)->((r->p)->(r->q)) C: CCpCqrCqCpr / (p->(q->r))->(q->(p->r)) K: CpCqp / p->(q->p) W: CCpCpqCpq / (p->(p->q))->(p->q)
If there are two different axiomatic bases for the same logic, how do know that they are the same? First some terminology: If a logic A can be described without redundancy by some axiom set (B) that is the A set plus some axioms, that A is called a sub logic of B, and B is called an extension of A. If you have two axiom sets, A and B, that allegedly are axioms for the same logic, they each must be able to prove everything in the system. That means that each should be able to prove the other. If axiom set A can prove a set B, then B is at least a sublogic of A, or possibly is A. If B can prove A, A is at least a sublogic of B or possibly is B. If they can each prove the other, then we know that they are at least sub logics of each other, and therefor that must be the same logic. If there is a known basis for a system, another alleged basis is the same system if you can find proofs both ways between the bases. Note that this is easier said than done. Such proofs can be very difficult to find and there are lots of bases for some logics that are suspected to be an axiomatic basis for a specific logic but have not been proven or disproven for fifty or more years.
OK, now that all that is out of the way, we can go on to talk about properties of axiomatic bases. An obvious observation is that some axiomatic basis for the same logic have different numbers of axioms. And if one knows this, an obvious question to ask is whether or not a system has a basis that has only ONE axiom.
In a basis that has only one axiom the axiom is called a "Single Axiom". Like any other basis, it can prove all the theorems of the system, and nothing else.
And if you have a collection of single axioms, you can ask which is the shortest. This is called *a* shortest single axiom, since there may be many of that shortest size.
As an example, the system called BCI has 80 known shortest single axioms, and it is known that no shorter ones exist, and that there are a small number of candidates of that size that no one knows whether or not they are single axioms, and they've been around for around 40 or so years without anyone finding a proof or disproof of their status.
[TODO: Put in the citations to the actual articles and dates not from memory] A good question at this point is what it takes for a logic to have a single axiom. The first steps in answering that were taken by Tarski who discovered in 1925 or so, and published in 1930 or so, that there were two different sets of two theorems (one given in the text, one in a footnote) that insured that if your system had them, your system also had a single axiom. Although Tarski distributed the proof privately, it never made it to print. It was effectively lost until (1980?) when Adrian Rezus generated a proof based on Lambda Calculus and Combinators it also expanded the number of different logic systems that could proven to have single axioms. This was a constructive proof, and it produced famously long axioms. In (2008??) I produced a proof based on just the logic generally available in Tarski's time, of yet another set of theorems that insured your system had a single axiom. It was also a constructive proof, and while the axioms generated were smaller than Rezus' paper generated, they were HUGH. I was following an approach pioneered by Dr. Dolph Ulrich. He apparently proved the footnote pair of axioms from Tarski's paper... and presented it at a conference that never had the proceedings with his paper published. I was also able to weaken one of the axioms in the set (maintaining the property) Tarski had in the set in the footnotes of his paper. Over the past few years, I've generated several other such pairs of theorems. I have a growing collection of pairs of theorems that work. So far my crowning achievement has been proving that if your logic has the the pair of axioms K: (p -> (q -> p)) and C: ((p -> (q -> r)) -> (q -> (p -> r)) in your system insures that it has a single axiom. There are some other pairs whos presence that (constructively) insure that a single axiom exists.
But, alas, nobody has has been able to produce, with such constructions, anything as short as the known single axiom bases. For one popular logic, BCI, The shortest single axioms are of length 19 (in Polish notation). Rezus's single axiom is about 93 symbols long My constructions are some 50 symbols long. This is a very very large gap. Those of us working in the area would welcome some construction from the axioms that was in the ballpark of the size of known shortest single axioms for the system.
Navigation:
No comments:
Post a Comment