Have you ever been in an argument where the other person "just wasn't being reasonable?" What were they doing that was "without reason?"
- Making "facts" up out of thin air?
- Forming connections between claims without appropriate evidence?
- Jumping between unrelated arguments?
- Not addressing the problem at hand?
How do you know that you were being reasonable and your partner was the unreasonable one? Is there an agreed-upon set of rules for what it means to operate "within reason" or is it simply a matter of perspective?
Mathematical logic is the study of formal logical reasoning. Coincidentally, logic itself is one of the foundations of both mathematics and computer science. Recall that mathematical prose contains propositions that assert relationships between definitions. These propositions are stated in terms of mathematical logic and thus form one of the cornerstones of the discipline.
As computer scientists, we care about logic for similar reasons. We care about the properties of the algorithms we design and implement, in particular, their correctness and complexity. Logic gives us a way of stating and reasoning about these properties in a precise manner.
Propositional Logic
Let us begin to formalize our intuition about propositions. First, how can we classify propositions? We can classify them into two buckets:
-
Atomic propositions that make elementary claims about the world. "It is beautiful today" and "it is rainy today" are both elementary claims about the weather.
-
Compound propositions that are composed of smaller propositions "It is either rainy today or it is beautiful today" is a single compound proposition made of up two atomic propositions.
This is not unlike arithmetic expressions that contain atomic parts---integers---and compound parts---operators. As you learned about arithmetic throughout grade school, you learned about each operator and how they transformed their inputs in different ways. Likewise, we will learn about the different logical operators---traditionally called connectives in mathematical logic---and how they operate over propositions.
We can formally define the syntax of a proposition similarly to arithmetic using a grammar:
A grammar defines for a sort (the proposition ) its set of allowable syntactic forms, each written between the pipes (). A proposition can take on one of the following forms:
-
Atomic propositions, elementary claims about whatever domain we are considering. When we don't care about the particular domain (e.g., we want to hold the domain abstract), we'll use capital letters such as as meta-variables for atomic propositions.
-
Top, (LaTeX:
\top), pronounced "top", the proposition which is always provable. -
Bot, (LaTeX:
\bot), pronounced "bottom" or "bot", the proposition which is never provable. -
Logical negation, (LaTeX:
\neg), pronounced "not", which stands for proposition , but negated. For example, the negation of = "It is beautiful today" is = "It is not beautiful today". -
Logical conjunction, (LaTeX:
\wedge), pronounced "and", which stands for the proposition where both and are provable. For example, the conjunction of = "It is beautiful today" and = "The sun is out" claims that it is both beautiful and the sun is out. -
Logical disjunction, (LaTeX:
\vee), pronounced "or", which stands for the proposition where at least one of or is provable. For example, the disjunction of = "It is beautiful today" and = "It is raining today" claims that it is either beautiful today or it is raining today (or both are true). -
Logical implication, (LaTeX:
\rightarrow), pronounced "implies", which stands for the proposition where is provable assuming is provable. For example, if = "It is cloudy" and = "It is raining", then claims that it is raining, assuming that it is cloudy.
Notably, logical implication are the conditional propositions we have seen previously of the form "if … then … ." For example, if we had the following program correctness claim:
We might write it concisely using the formal notation above as:
This form of logic is called propositional logic because it focuses on propositions and basic logic connectives between them. There exist more exotic logics that build upon propositional logic with additional connectives that capture richer sorts of propositions we might consider.
Modeling with Propositions
Recall that mathematics is the study of modeling the world. In the case of mathematical logic, we would like to model real-world propositions using the language of mathematical propositions we have defined so far. This amounts to translating our informal natural language descriptions into formal mathematical descriptions.
To do this, keep in mind that mathematical propositions are formed from atomic and compound propositions. We then need to:
-
Identify the atomic propositions in the statement.
-
Determine how the atomic propositions are related through various compound propositions.
As an example, let's consider a proposition more complicated than the previous ones that we have encountered:
"If it is either the case that the grocer delivers our food on time, or I get out to the store this morning, then the party will start on time and people will be happy.
First, we identify the domain under which we are making this proposition: preparing for a party. Thus, the atomic propositions are the statements that directly talk about preparing for a party. These propositions are:
- = "The grocer delivers our food on time."
- = "I get out to the store this morning."
- = "The party will start on time."
- = "People will be happy."
Now, we re-analyze the statement to determine how the propositions are related, translating those relations into logical connectives. You may find it helpful to replace every occurrence of the atomic propositions with variables to make the connecting language pop out:
"If it is either the case that or then and ."
From this reformulation of the statement, we can see that:
- and are related by the word "or" which implies disjunction.
- and are related by the word "and" which implies conjunction.
- These previous two compound conjunctions are related by the words "if" and "then" which implies implication.
Thus we arrive at our full formalization of the statement:
(Note that has lower precedence than or so the statement written as-is is not ambiguous.)
When translating statements in this manner, it is useful to keep in mind some key words that usually imply the given connective:
- : "not"
- : "and"
- : "or"
- : "implies", "if ...then"
Reasoning with Propositions
Recall that our goal is to formally model reasoning. While equivalences allow us to show that two propositions are equivalent, they do not tell us how to reason with propositions. That is, how do we prove propositions once they have been formally stated?
First, we must understand the reasoning process itself so that we can understand its parts. From there, we can state rules in terms of manipulating these parts. When we are trying to prove a proposition, whether it is in the context of a debate, an argument with a friend, or a mathematical proof, our proving process can be broken up into two parts:
- A set of assumptions, propositions that we are assuming are true.
- The proposition that we are currently trying to prove, our proof goal.
We call this pair of objects our proof state. Our ultimate goal when proving a proposition is to transform the proof goal into an "obviously" correct statement through valid applications of proof rules.
For example, if we are in the midst of a political debate, we might be tasked with proving the statement:
"80s-era Reaganomics is the solution to our current economic crisis."
Our proof goal is precisely this statement and our set of assumptions includes our knowledge of Reaganomics and the current economy. We might take a step of reasoning---unfolding the definition of Reaganomics, for example---to refine our goal:
"Economic policies associated with tax reduction and the promotion of the free-market are the solution to our current economic crisis."
We can then apply additional assumptions and logical rules to transform this statement further. Once our logical argument has transformed the statement into a self-evident form, for example:
"Everyone needs money to live."
Then, if everyone agrees this is a true statement, we're done! Because the current proof goal follows logically from assumptions and appropriate uses of logical rules, we know that if this proposition is true, then our original proposition is true. In a future reading, we will study these rules in detail in a system called natural deduction.
Propositional Logic Versus Boolean Algebra
Throughout this discussion, you might have noted similarities between propositions and a concept you have encountered previously in programming: booleans.
Values of boolean type take on one of two forms, true and false, and there are various operators between booleans, && and ||,logical-AND and logical-OR, respectively.
It seems like we can draw the following correspondence between propositions and booleans (using the boolean operators found in a C-like language):
- is
true. - is
false. - is
!. - is
&&. - is
||.
This correspondence is quite accurate! In particular, the equivalences we discussed in the previous section for propositions also work for boolean expressions. The only caveat is that there is no analog to implication for the usual boolean expressions, but the equivalence:
Allows us to translate an implication into an appropriate boolean expression.
So why do we talk about propositions when booleans exist? It turns out they serve subtle, yet distinct purposes!
- A proposition is a statement that may be proven.
- A boolean expression is an expression that evaluates to
trueorfalse.
Note that a proposition does not say anything about whether the claim is true or false. It also doesn't say anything computational in nature, unlike a boolean expression which carries with it an evaluation semantics for how to evaluate it in the context of a larger computer program.
Furthermore, the scope of a boolean expression is narrow: we care about booleans values insofar as they assist in controlling the flow of a program, e.g., with conditionals and loops. We don't need to complicate booleans any further! In contrast, propositions concern arbitrary statements, and our language of propositions may need to be richer than the corresponding language of booleans to capture the statements we have in mind.
Consider the following propositions
- = "The sky is cloudy."
- = "I will go running today."
- = "I'm going to eat a cheeseburger."
Write down English translations of these formal statements:
- .
- . (Note: implication is a right-associative operator! This means that this statement is equivalent to ).
- .
Recall that implication is right-associative. That is, sequences of operators parenthesize "to the right", i.e.,
Now, consider the abstract proposition where we instead parenthesize to the left:
Come up with concrete instantiations of , , and and write down the English translation of this proposition.