This is an episode in a series on mathematical logic approached with some rigour. Here, we will (still) be closely following the book by Peter B. Andrews: An Introduction To Mathematical Logic and Type Theory. We will look at the axiomatic structure of a logistic system we’ve been working on. The previous blogpost can be found here: (S1E01): The Rules.
An axiom is a statement that is taken to be true. The system we’ve been building from (S1E01) (called ) consists of well-formed formulas having one of the following
(S1E02) (Sc0) axiomatic schemas:
We then also have just one primitive rule of inference:
- Modus Ponens
For some wff , if it is accepted and is of the form , then we can infer , given holds. are wffs.
Example: Let If it is an evergreen tree, then it doesn’t loose leaves in winter and its leaves are always green. Here we have It is an evergreen tree. And It doesn’t loose leaves throughout the year and its leaves are always green. Let us accept , and take a walk down the streets of some neighbourhood in South Africa with one of your friends who happens to be a botany major. We then come across these trees ( Cape Holly), and your friend exclaims: “It’s the evergreen Cape Holly trees!”.
What deduction can you make about the colour of its leaves throughout the year? They’re always green! Note that in this instance, if a tree’s leaves are always green and never fall off, it is true that it’s an evergreen, however, it’s not generally true that if one has a consequent: (), that can they assert anything about the antecedent (). i.e. the arrow goes from left to right (), not from right to left.
will denote a set containing wffs.
And then, we shall define what a proof is:
(S1E02) (Sc1) Defn: What is a Proof
A proof of a wff , where is a set of antecedents (or hypothesis), is a finite sequence where and for each
- is an axiom.
- is inferred (by Modus Ponens) from and where and .
Notation and Facts
- A theorem is then a wff with a proof.
- We can write which means is a theorem from the set , and is derivable from .
- In the place of we write .
- will mean .
- will mean is derivable from the empty set, and that therefore is theorem.
What it means for the set of antecedents to be empty is that we can always infer a wff from it. This reminds me of something known as vacuous truth. I encourage the reader to read the Wikipedia article on this, an excerpt:
“statements which can be characterized informally as vacuously true can be misleading. Such statements make reasonable assertions about qualified objects which do not actually exist. For example, a child might tell their parent “I ate every vegetable on my plate”, when there were no vegetables on the child’s plate to begin with.”
However, vacuous truth and , aren’t necessarily the same thing! The former refers to the idea of referring to elements involved in the statements as not existing, whereas the latter refers to the statements themselves not existing.
Testing if a finite sequence of wffs is a proof.
A proof is generally of this form:
Where each line is a consequence of That is, each line is either (1): an axiom, (2): A premise (antecedent), or (3): inferred from a line prior through Modus Ponens. In general though, we’ll see later on that there are many more rules of inference we can use which are a derivative of the information we already have about our system.
For the reader that’s not familiar with Groups And Rings, to put it shortly, a Group is a set that is closed under some binary operation. i.e. if is my set, and I have any , then . Example: are closed under addition.
Rings have this property too, but with an additional binary operation. Example: are closed under standard addition and multiplication.
There is much more to Rings and Groups than this, but this is about all we’ll need for this next section. Read more about them on Wikipedia (Rings), Wikipedia (Groups).
In Group theory, we have what is known as the group axioms, and likewise, for Ring theory, we have the Ring axioms. The Ring Axioms are an appendix to the group axioms and thus the set of antecedents for Group is a subset of the set of antecedents for the Ring . So, we have . Now, I’ll attempt to draw parallels between this fact and the theorems below.
It’s important to understand and know the following theorems.
Theorem (S1E02) (Sc2)
and then .
For example: if I have a theorem which states that the identity element of a group, e.g. in is unique for some binary operation (in this case ), then that exact theorem also exists in Ring Theory for some Ring: example .
Proof (S1E02) (Sc2)
has the same set of axioms and rules of inference to allow to be derived. Since it’s a superset of where is a proof in.
There is a direct consequence of this theorem (a corollary).
This result can be obtained by applying Modus Ponens on the first two statements in the antecedent on the set and this you can do because of (S1E02) (Sc2).
Theorem (S1E02) (Sc3) Rule Of Substitution (Sub)
If where a proof for is given be and if are distinct variables not found in any wff in , then is also a proof in . Where is a substitution.
Proof (S1E02) (Sc3) (Sub)
If is a sequence describing a theorem , it follows that is also a sequence describing a theorem in . So is also a theorem in .
For the next theorems, it’s important that one understands what Modus Ponens is. Modus ponens is a rule of inference that states that if I have a statement , and holds. Then I can infer from . That is to say that also holds. From here on, we will refer to Modus Ponens as MP. Also, we will abbreviate Axiom to Ax.
Theorem (S1E02) (Sc4)
If and then .
Proof (S1E02) (Sc4)
Suppose we have the proofs for and where these are respectively and respectively. So, we have…
Theorem (S1E02) (Sc4) is a derived rule of inference. Here we made use of MP and Axiom 3.
The following theorems are all written in the form . Where is some well-formed formula. Notice there is no set of antecedents in this case. What this means is that thees theorems are independent of any antecedent. They are then thus the theorems of logic and are true for any . These are important.
Theorem (S1E02) (Sc5)
Proof (S1E02) (Sc5)
Theorem (S1E02) (Sc6)
To be honest, this theorem’s proof (from the book) didn’t make any sense to me. After reading up on substitutions I realise that some books allow substitutions that we are here anyways trying to show, so that wasn’t too helpful. What was helpful though, was my previous post. Recall this excerpt from the book:
and also recall we wanted to prove . I will remind the user of the proof I used and some of the information I extracted from the proof:
Consider a wff with some substitution . If is a wff then we know it must have a formulation sequence (S1E01) (Climax 1). Consider a simultaneous substitution on all formulas in the formulation sequence to variables . Here, . So, and . So putting this together, we get . This then tells us that there must exist a substitution , such that gives us the empty formula.
This substitution does exist because we see in this post that .
Now for the proof:
In this proof, we’ll basically note that . And to both we apply . Which will give us . If either are theorems in some set , then so is the other (Sub). We already know from (S1E02) (Sc5) this should be the case so we summaries our proof as follows:
Proof (S1E02) (Sc6)
Note that here we assumed commutative of the disjunction. If this is actually not the case, then we’ll have to come back and fix this at a later stage or if we ever need this fact to prove such, then we’ll have to come back and reason this differently.
A similar idea is used for the theorem .
So we have
Which is basically what we’ve stated above.
We are starting to notice some algebraic behaviour here. cancels like .
Now, the proof for this is a bit long in the book. Instead, I’ll make use of for the sake of shortening this long-ass post.
Theorem (S1E02) (Sc7)
Proof (S1E02) (Sc7)
The next theorem (S1E02) (Sc8) says:
Proof (S1E02) (Sc8)
We can do the same for . And thus we have commutativety that we’ve been seeking. Here we relied on the result . Though trivial, our proof for it made use of another that relied on commutativity. So it’s circular. The assistance of the reader would greatly be appreciated, how would we rectify this?
I will stop this post here seeing as it’ll just be a collection of theorems from hereon. I will, however, make a post on those theorems next. But I think this is a good place to stop.
Any feedback is greatly appreciated. Next, we look at some other useful theorems and start to investigate what all this means (the semantics of our syntax).
The other theorems I have not discussed in this blogpost are mostly algebraic and for anyone who’s been proving theorems for quite some time, are really obvious. So for example the transitive property of implication, a deduction theorem, a theorem of antecedent independence (if a consequent follows whether the antecedent holds or not then that consequent must be a theorem of some theory), and also associativity of the disjunction (there’s a quick exercise to show it holds both ways in the book). If anyone is really reading this, and wants further details, drop a comment.