These notes follow closely notes originally developed by Alexander Kechris for the course Math 6c at Caltech.
Somewhat informally, a proposition is a statement which is either true or false. Whichever the case, we call this its truth value.
Example 1 “There are infinitely many primes”; “”; and “14 is a square number” are propositions. A statement like “ is odd,” (a “propositional function”) is not a proposition since its truth depends on the value of (but it becomes one when is substituted by a particular number).
Informally still, a propositional connective combines individual propositions into a compound one so that its truth or falsity depends only on the truth or falsity of the components. The most common connectives are:
- Not (negation),
- And (conjunction),
- Or (disjunction),
- Implies (implication),
- Iff (equivalence),
A word of warning is in order: The precise mathematical meaning of a connective (say, ) should not be confused with the somewhat ambiguous meaning of the word (say, “implies”) used to name it. The intended mathematical meanings of the connectives are as follows:
- “Not” () is a unary connective, i.e., it applies to only one proposition, and negates its truth value. There are other, less common, unary connectives: One that always returns a false value regardless of the truth or falsity of the proposition it is applied to, one that always returns a true value, and one that simply returns the same value of the proposition it is applied to. The other connectives mentioned above are binary, i.e., they bind two propositions:
- A proposition combining its components with “and” () is true when, and only when both of its components are true.
- A proposition combining its components with “or” () is true whenever either or both of its components are true. That is, is the so-called “inclusive or.”
- The “iff” (“if and only if”) or equivalence connective () is true precisely when both of its components have the same truth value, be it true or false.
- Unlike the previous connectives, the “implication” () is not symmetric: is not the same as When we use we intend to convey the meaning that whenever is true, must also be. So if is true, is true if and only if is also true. If, on the other hand, is false, then is also true (we say it is “vacuously” true). The statement that does not carry any “causal” connotation, unlike the English phrases we use (for lack of anything better) to pronounce it (such as “ implies ” or “if then ”).
We can summarize the meanings of these connectives using truth tables:
Of course, there are other binary connectives, and there are also ternary connectives, and connectives of even higher arity.
There are many different ways of expressing a compound statement, and corresponding to these there are different equivalent ways of combining propositions using these connectives: Their truth values are the same for any truth values of the original propositions. Here are some examples:
- The statements
are equivalent. This is one of what are known as De Morgan’s Laws.
- The law of the double negative says that and are equivalent. That is, if something is not false, it is true, and vice versa.
- The statements
are equivalent. The latter statement is called the contrapositive of the first. Note that because of the law of the double negative, the first statement is also equivalent to the contrapositive of the second.
- Yet another way to say that is
One consequence of this is that we could, if we wanted to, do without the connective altogether.
- Two more related statements which are not equivalent to are the converse, and the inverse, The converse and inverse are contrapositives of each other, however, so they have the same truth value.
We now proceed to develop the theory of propositions in a rigorous setting.
2. Syntax of propositional logic
In order to rigorously prove results about the structure and truth of propositions and their connectives, we begin by developing a formal language, the language of propositional logic. Later, just as in the example of the tree system presented before, we will assign a semantic to this language.
Definition 1 In the language of propositional logic we have the following list of symbols:
- Propositional variables. This is an infinite list of symbols. We often use to denote propositional variables.
- Symbols for the propositional connectives and
It does not matter what the propositional variables or the connectives actually are, for example, we can begin with any (countable) infinite set, and decide that its elements are the propostional variables. Our only requirement is that the symbols and are distinct from one another, and from the propositional variables.
We could also have symbols for and for additional connectives. In order to simplify the presentation, I will restrict myself to the language above.
As before, a string or word is any finite sequence of the symbols in the language, including the empty string. Its length is its domain, just as before. Unlike the example of the tree-system, now we are only interested in certain strings, those that “represent” formulas. There are several conventions we could follow; for example, we could state that or are formulas. To simplify the presentation, we restrict ourselves to only one of these options.
We will refer to the “grammatically correct” strings (those formed according to the conventions below) as well-formed formulas (wffs) or just formulas.
Definition 2 (Well-Formed Formulas)
- Every propositional variable is a wff.
- If is a wff, so is
- If are formulas, so is
Thus a string is a wff exactly when there is a finite sequence
(called a parsing sequence) such that and for each one of the following holds:
- is a propositional variable, or
- For some or
- For some
- is a wff with parsing sequence
is another parsing sequence, so parsing sequences are not unique.
- is a wff with parsing sequence
- and are not wff, but to prove this requires an argument.
Remark 1 Just as in the case of the tree system, we have not yet assigned any “meaning” to any of the symbols in our formal language. Eventually, we intend to interpret symbols such as in a way analogous to the propositional connective “implies,” at present they are simply symbols that we are manipulating formally.
We can prove properties of formulas by induction on the length of a formula. Suppose is a property of a formula For example, could mean “ has the same number of left and right parentheses.” If holds for all formulas of length 1 (i.e. the propositional variables) and whenever holds for all formulas of length then it holds for all formulas of length we may conclude, by induction, that holds for all formulas.
However, because of the way formulas are defined, it is most useful to use another form of induction, sometimes called induction on the construction of wff (or just induction on formulas):
Let be a property of formulas Suppose:
- Basis of the induction: holds, when is a propositional variable.
- Induction step: If hold for two formulas then
hold as well.
Then holds for all formulas We can prove the validity of this procedure using standard mathematical induction, and the existence of a parsing sequence for any wff.
Example 3 One can easily prove, using this form of induction, that every formula has the same number of left and right parentheses. This result can be used to show that certain strings, for example are not wffs, because they have unequal numbers of left and right parentheses.
Example 4 We can easily prove by induction on the construction of wff that a nonempty proper initial segment of a formula either consists of a string of ‘s or else has more left than right parentheses. Another easy induction shows that no formula can be empty or just a string of ‘s, so using also the previous example, no proper initial segment of a wff is a wff.
This can also be used to show certain strings, for example, are not wffs, as they contain proper initial segments that are wffs (in the example, ). Similar methods can be used for other non-wffs.
While parsing sequences are not unique, there is a sense in which all alternative parsing sequences offered for a given wff are “the same”: they break the wff down in the same way, to the same components, albeit in a different order. Using induction on formulas, we can prove that this will always be the case. This is called unique readability.
Theorem 3 (Unique Readability Theorem) Every wff is in exactly one of the forms:
- (i.e., a propositional variable);
- for a uniquely determined wff;
- for uniquely determined wff’s
Proof: By induction on the construction of formulas, it is straightforward that any formula must be of one of these forms. To prove uniqueness first notice that no wff can be in more than one of the forms (1), (2), (3). Obviously no two propositional variables are the same, and if then
So it is enough to show that in case (3), if then and First notice that, by eliminating the left parenthesis, we have that From this it follows that either is an initial segment of or vice versa. If then one of is a proper initial segment of the other, which is impossible, as they are both formulas. So we must have Thus and so
Remark 2 Similar arguments would have given the same result if we had followed a different convention when defining formulas. For example, if we had stated that whenever and are formulas, then so is However, not all conventions would work. For example, if we had used a formula such as would be “ambiguous.”
Definition 4 In form (2) we call the main connective and in (3) we call the connecting the formulas denoted above by and the main connective. Thus the main connective is the one applied last in a parsing sequence.
Example 5 In the main connective is the third “” (from left to right).
Given a formula it might be hard to recognize immediately which is the main connective. Consider for example the following formula:
(it turns out to be the 5th “”). There is however an easy algorithm for determining the main connective: In the formula the main connective is the first binary connective (from left to right) such that in the string preceding it the number of left parentheses is exactly one more than the number of right parentheses.
One can use the unique readability theorem to justify the following principle of definition by recursion on the construction of formulas:
Let be a set and let and be given functions. Then there is a unique function from the set of all formulas into such that
- for all propositional variables
- for any formula and
- for any formulas and
Without unique readability, the existence and uniqueness of would be called into question: If there were two different ways of breaking down a formula, then the corresponding compositions of the s might yield different values of for the same formula. But now that we know unique readibility, is well defined and unique.
- Let be defined according to the following clauses:
Then it is easy to see that the length of
Then the number of connectives in
- Let be a propositional variable and a formula. We define for each formula the formula according to the following clauses:
Then it is easy to see that is the formula obtained by substituting every occurence of in by
For example, if and then
- The parse tree of a formula is defined recursively as follows: The tree has a root with a unique immediate successor.
- In the parse tree of a propositional variable this successor is labelled and this is the whole tree.
- In the parse tree this successor is labelled and following it there is a copy of with the root removed.
- In the parse tree this successor is labelled and following it there are two immediate successors, to which we attach a copy of and a copy of with the roots removed.
Here is an example. For clarity, I use other connectives rather than just Say that Then its parse tree is
where, again for clarity, we have omitted the root, and labelled the nodes by formulas rather than connectives.
The parse tree, starting now from the bottom up, gives us various ways of constructing a parsing sequence for the formula; for example:
By unique readability, all parsing sequences can be obtained in this manner. Thus the parse tree extracts the “common part” referred to above, out of each parsing sequence.
- The formulas occurring in the parse tree of a formula are called the subformulasof These are the formulas that arise in the construction of If we let denote the set of subformulas of then can be defined by the following recursion:
We will next discuss an algorithm for verifying that a given string is a formula.
Given a string let be a propositional variable not occurring in and let the string we obtain from by substituting every propositional variable by
For any string containing only the variable let be the string obtained from as follows: If contains no substring (i.e. a string contained in as a consecutive sequence of symbols) of the form or then Otherwise substitute the leftmost occurence of any one of these forms by to obtain Notice that if then the length of is strictly smaller than that of
Now starting with an arbitrary string form first and then define recursively This process stops when we hit for which i.e., has no substring of the above form. This must necessarily happen since otherwise we would have an infinite decreasing sequence of lengths, which is impossible.
We then have that if then is a formula, and otherwise it is not.
- Let be Then we have:
So is not a wff.
- Now let be Then we have:
So is a wff.
Exercise 1 Prove the correctness of this algorithm.
Sometimes in practice, in order to avoid complicated notation, we adopt various abbreviations in writing wff, if they do not cause any confusion.
First of all, we write instead of instead of and instead of the formula abbreviated by
Also, we usually omit outside parentheses: We write instead of or instead of etc.
We adopt an order of preference between the binary connectives, namely
where connectives from left to right bind closer, i.e., binds closer than ; binds closer than ; and binds closer than So if we write we really mean and if we write we really mean etc.
Finally, when we have repeated connectives, we always associate parentheses to the left, so that if we write we really mean and if we write we really mean
All these are conventions that we follow (informally) in practice, although formally we have not introduced symbols to the language, or extended the notion of formula, and are just writing the unabbreviated forms each time.
8. A Hilbert-Type Proof System
We now describe a formal calculus of proofs. As in the example of the tree system, we start with axioms and use rules of inference to deduce consequences.
This style of arguing in formal logic, using axioms and rules, was introduced by David Hilbert and his school.
Hilbert was born in Königsberg, Prussia, in 1862, and died in Göttingen, Germany, in 1943. He is one of the most important mathematicians of the late 19-th and early 20-th century. A strong advocate of nonconstructive methods, this probably started with his work on “invariant theory,” where he proved a Basis Theorem without exhibiting an explicit basis. The paper appeared in Mathematische Annalen in 1888. (The result states that in any number of variables there is a finite set of generators for the invariants of quantics. A quantic is a symmetric tensor of a given degree constructed from tensor powers of a (finite dimensional) vector space. Invariance is measured under invertible operators of the space in itself.)
Gordon, the world expert in invariant theory, strongly opposed in vain to the publication of Hilbert’s result, due to its nonconstructive nature. On the other hand, Klein said of this result that “I do not doubt this is the most important work on general algebra that the Annalen has ever published.”
Hilbert’s work in number theory led to his book on the theory of algebraic number fields, recently translated into English. He started his work on logic with the publication in 1899 of the Grundlagen der Geometrie, where he advocates the axiomatic approach to mathematics.
In 1900 he delivered the invited address “Mathematical problems” to the Second International Congress of Mathematicians in Paris, where he listed 23 problems that in his opinion were essential for the progress of mathematics. From here comes his dictum “Here is the problem, seek the solution”. The inscription on his tombstone, “We must know, we will know” comes from a speech in Königsberg in 1938. His address can be found in the Bulletin of the AMS, vol 37, number 4 (2000).
His work on integral equations and calculus of variations led to functional analysis and the concept of Hilbert space. He also solved Waring’s problem, a well-known problem in number theory. His work in logic resulted in the development of proof systems and lead to the incompleteness theorems of K. Gödel.
A (logical) axiom is any formula of one of the following forms:
(for arbitrary formulas ).
We also have a rule of inference called modus ponens or MP: “From and derive ” In formal calculi, a rule such as this for deriving one formula from others given, is sometimes written as follows:
Modus ponens is short for latin “modus ponendo ponens” which means “proposing method.”.
Definition 5 Let be any set (finite or infinite) of formulas. A formal proof from is a finite sequence of formulas such that each is either a logical axiom, belongs to or comes by applying modus ponens to some with (i.e., is the formula ). We call this sequence a formal proof of from
Definition 6 If there is a formal proof of a formula from we say that is a formal theorem of and write
If we just write
and call a formal theorem.
Notice that and imply that Also notice that if and for all then since the formal proofs can simply be concatenated. Finally, implies that there is finite with since a formal proof can only be finitely long and hence can only use finitely many formulas of
Example 8 Let Here is a formal proof of from :
- (in ),
- (axiom (2)),
- (MP from 1, 2),
- (in ),
- (MP from 3, 4),
- (in ),
- (MP from 5, 6)
In the proof above, I have listed next to each formula the reason why it can be written down. Just as in the case of proofs in the tree system, formally, the proof is just the sequence of formulas, without the companion explanations:
Example 9 The following formal proof shows that :
- (Ax. (2)),
- (Ax. (1)),
- (MP 1, 2),
- (Ax. (1)),
- (MP 3, 4).
Typeset using LaTeX2WP. Here is a printable version of this post.