CISC/CMPE 204

20130121 - 20130128

Propositional Logic as a Formal Language

Unlike natural languages, formal languages have very little to do with information or communication. The central idea behind a formal language is determining whether or not a given sequence of symbols is a legal or well-formed expression within the language. The study of formal languages is central to computer science for both practical and theoretical reasons: on the practical side, a piece of software must conform to the syntax of the programming language in which it is written, and we need tools that will check this - on the theoretical side, many of the most fundamental concepts in the study of computational complexity (which tries to determine which problems can be solved quickly and which are inherently difficult) can be expressed in terms of formal languages.

So the purpose of describing propositional logic as a formal language is not to add any expressive power to it, but rather to put it into a format in which it is easy to determine if a string of symbols actually forms a proposition that we could evaluate. We use the following grammar to define propositional logic as a formal language:

1. All atomic propositions are well-formed formulae (wff).
2. ! : If PHI is a wff, then (!PHI) is a wff
3. ^: If PHI and PSI are wff, then (PHI ^ PSI) is a wff
4. V: If PHI and PSI are wff, then (PHI V PSI) is a wff
5. ->: If PHI and PSI are wff, then (PHI -> PSI) is a wff

The purpose of all the parentheses is to let us forget about precedence rules and binding orders. We can parse a fully parenthesized formula recursively and mechanically (i.e. we don't need to worry about the interpretation of the symbols). Parsing a wff lets us build a parse-tree for the formula, in which the root node corresponds to the final rule that was applied in the building of the formula, and the leaves are the atomic propositions in the formula.

The Semantics of Propositional Logic

We introduced the idea of considering whether a given atomic proposition is true or not in the real world or in some segment of it that we are modelling or imagining. (Note that in ND, we don't actually do this - ND is a purely syntactic system for manipulating symbols). We can examine the way that the truth or falseness of atomic propositions affect the truth or falseness of compound propositions.

For example, consider the formula (p V q) ^ r

We build a truth table with a column for each atomic proposition, each sub-formula of the overall formula, and finally the complete formula:

       p         q        r          (p V q)         (p V q) ^ r

        T      T       T                T                    T
        T        T       F                T                  F
        T        F       T            T                  T
        T         F      F                T                  F
        F         T      T                T                  T
        F         T      F                T                  F
        F         F      T                F                  F
        F         F      F                F                  F

Each line of a truth table is called a model or valuation.

Defining Truth Tables for the Fundamental Logic Operators

It is important to understand that the truth tables we create for the fundamental logical operators ^, V, ! and -> are definitions - logicians agree to use these definitions, and because the definitions are visual and tabular, there is very little risk of misinterpretation. However, it is essential to remember that we are defining a system of logic, not discovering intrinsic properties of reality.

For ^, V and ! the definitions are fairly obvious, but for -> there is some room for discussion.

p    q     p-> q

T    T       T
T    F       F
F    T       ?
F    F       ?

The first two lines of the truth table seem acceptable to most people. However, arguments can be made for replacing the ?s with T (which is what we will do) or F (which we won't). The "T" interpretation can be called the "benefit of the doubt interpretation" - we do not have hard evidence to refute the implication, so we accept it as true. The "F" interpretation can be called the "dubious interpretation" - we do not have hard evidence to support the implication, so we reject it and say it is false.

In our system of logic, we finish the table for -> like this

p    q     p-> q

T    T       T
T    F       F
F    T       T
F    F       T

The justification for this is a very pragmatic reason. We want the two systems of propositional logic (syntax, via Natural Deduction, and semantics, via truth tables) to be interchangeable, which means that propositions which are equivalent in one system should also be equivalent in the other. Since we know that p -> q -||- !p V q is a provable equivalence in the ND version of propositional logic, we also want these formulas to be equivalent in the semantic version of propositional logic. Since the truth table for !p V q is easily seen to be

p    q     !p V q

T    T       T
T    F       F
F    T       T
F    F       T

the decision to make this the truth table for p -> q is pretty much forced on us.

The Soundness of Propositional Logic

We are finally ready to prove that if PHI1, ...., PHIn |- PSI is a valid sequent, then PHI1, ...., PHIn |= PSI is a semantic entailment. The significance of this result is that we cannot build a proof of something which is not "true" in the semantic entailment representation of truth. To be more explicit, if there exists a proof for the sequent, then in the truth table all lines that have a T for each of PHI1 ... PHIn must also have a T for PSI.

As promised, we will use course-of-values induction in the proof, and we will apply the induction to the number of lines in a proof of the sequent. We will state the theorem as

Theorem: For all values of k, if PHI1, ..., PHIn |- PSI has a proof with k lines then PHI1, ..., PHIn |= PSI is a semantic entailment.

Proof:

We will use M(i) to represent the statement " if PHI1, ..., PHIn |- PSI has a proof with i lines then PHI1, ..., PHIn |= PSI is a semantic entailment."

Base Case: We cannot have a 0 line proof because one line is needed to write down the conclusion. However, we can have a 1 line proof, which would look like
       1.   PSI

There are only two possible justifications we could have for writing PSI on the first line: one is that PSI is a premise, and the other is that PSI is the result of applying a rule that requires no premises ... and the only rule we have that fits that bill is the LEM, which lets us introduce "p V !p" In the first case, PSI must be both premise and conclusion (since the last line of a proof always states the conclusion), so the sequent must be PSI |- PSI. In the second case, the sequent must be |- p V !p. In both cases, it is very easy to show that semantic entailment holds.

Inductive Step:

Inductive Hypothesis: Suppose M(i) is true for all values of i < k.

Assume PHI1, ..., PHIn |- PSI is a valid sequence, and has a proof with k lines. The proof looks like this
       1. PHI1
       2.
       ...
       n. PHIn
     ...
       k. PSI

We don't know which of the rules of ND was used to introduce PSI on the last line of the proof - but there really aren't that many of them. To complete the proof, all we need to do is consider each rule in turn and show how it leads to a semantic entailment. We won't do all of them in these notes, and it is a good exercise to do at least a few more for your self.

Suppose the rule that justifies adding PSI to the proof is ^i. Then PSI looks like PSI1 ^ PSI2, and each of these must occur as previous propositions in the proof, outside of assumption boxes. Suppose they occur on lines m1 and m2 respectively. Then the lines 1...m1 form a proof of the sequent PHI1, ..., PHIn |- PSI1
and the lines 1...m2 form a proof of the sequent if PHI1, ..., PHIn |- PSI2. Since both of these proofs have < k lines, the semantic entailments
    PHI1, ..., PHIn |= PSI1 and
    PHI1, ..., PHIn |= PSI2
must hold (by our Inductive Hypothesis).

It is now trivially easy to construct the truth table for PSI using the truth tables for PSI1 and PSI2, and to observe that PSI is true on every line where PHI1, ..., PHIn are all true. Thus PHI1, ..., PHIn |= PSI is a semantic entailment.

Now we do the same analysis to show that if any of the other possible rules were used to justify the final step of the proof of the sequent PHI1...PHIn |- PSI, semantic entailment also holds. In each case, the lines that form the requirements for the rule must occur above line k, and so the proof must contain proofs of them, and since these embedded proofs have < k lines, they must correspond to semantic entailments. It is easy to see that the truth tables for these semantic entailments can be combined to show that PHI1 ... PHIn |= PSI holds.

End of Proof

This is immediately useful to us. Suppose we are trying to prove a sequent, without success. If we can demonstrate that the corresponding semantic entailment does not hold, then there cannot be a proof of the sequent. To show that the semantic entailment does not hold, all we need to find is one line in the truth table on which all the premises are true but the conclusion is false.

For example, consider the sequent p -> q |- q -> p. This is obviously not valid but it may not be obvious how to prove that. We can demonstrate its invalidity by constructing the truth table

p      q      p-> q      q -> p
T      T         T            T
T      F         F            T
F      T         T            F         <--------- at this point we can stop. On this line, the premise has value T and the conclusion has value F.

Thus this is not a semantic entailment, and from the proof of soundness, we now know the sequent is unprovable.

The Completeness of Propositional Logic

We will outline a proof that if PHI1, ...., PHIn |= PSI is a semantic entailment, then PHI1, ...., PHIn |- PSI is a valid (i.e. provable) sequent. This is the second part of showing that the two systems of propositional logic (proof rules and truth tables) are exactly equivalent.

The proof consists of three main steps:

1. Prove that if PHI1, ... PHIn |= PSI holds, then |= PHI1 -> (PHI2 -> (..... (PHIn -> PSI))...) holds.

2. Prove that if |= PHI1 -> (PHI2 -> (..... (PHIn -> PSI))...) holds, then |- PHI1 -> (PHI2 -> (..... (PHIn -> PSI))...) is a valid sequent.

3. Prove that if |- PHI1 -> (PHI2 -> (..... (PHIn -> PSI))...) is a valid sequent, then PHI1, ... PHIn |- PSI is a valid sequent.

The proofs of Steps 1 and 3 are straightforward and we did them in class very much in the same way the text does them.

The proof of Step 2 is more difficult and the text's explanation is quite hard to follow. We can summarise the main points as follows:
    The proof is based on course-of-values induction applied to the height of the parse tree for the formula. The basic idea is that given any proposition RHO (just using a Greek letter different from PHI or PSI), we can take each line of the truth table for RHO and create a provable sequent which has the atoms in RHO (or their negations) as premises and either RHO or its negation as the conclusion. We do this by assuming it can be done for all formulas with parse trees that are smaller than RHO's parse tree, and then show how the the last operation in building RHO's parse tree lets us combine these to get a proof of the desired sequent.

Applying this method to the formula we have (i.e. PHI1 -> (PHI2 -> (..... (PHIn -> PSI))...) ) we get a separate proof for each line of the truth table of this proposition. We then use LEM over and over and over again to combine all of these special case proofs into a complete proof of |-PHI1 -> (PHI2 -> (..... (PHIn -> PSI))...).

Putting this result together with our previous proof of soundness, we can now state
PHI1, ... PHIn |- PSI is a valid sequent if and only if PHI1, ... PHIn |= PSI is a semantic entailment
We will explore the significance of this result over the next few lectures.