⊤ | ¬ | ∧ | P_{n} for n = 0, 1, 2 etc. | |||
⊥ | ∨ | |||||
→ | ||||||
↔ |
The various types of sentences have names:
Consider the sentence:
( ∨ , ( ∧ , P_{0} , P_{1} ) , P_{2} )
Compare it with the string
∨ ∧ P_{0} P_{1} P_{2}
In other words, we have erased the parentheses. (Also the commas.) However, we have not introduced ambiguity because there is only one way to insert parentheses which ends up with a sentence. This is the beauty of what is called Polish notation. On the other hand, Polish notation is painful to read with or without parentheses!
Almost always in this course, we will prefer to use the traditional notation, in which our example is written
( P_{0} ∧ P_{1} ) ∨ P_{2}.
We still have parentheses but they are used differently and the sentence is much easier to read. Note that we would never write
P_{0} ∧ P_{1} ∨ P_{2}
without parentheses because we would not be able to tell whether we mean
( P_{0} ∧ P_{1} ) ∨ P_{2}
or
P_{0} ∧ ( P_{1} ∨ P_{2} ).
In other words, we would not be able to tell whether we mean
( ∨ , ( ∧ , P_{0} , P_{1} ) , P_{2} )
or
( ∧ , P_{0} , ( ∨ , P_{1} , P_{2} ) ).
Yet another way to write sentences is in tree notation. We could picture our example as the following downward growing finite tree.
∨ | |||
| | \ | ||
∧ | P_{2} | ||
| | \ | ||
P_{0} | P_{1} |
While we will not emphasize tree notation in this course, sometimes it is a useful image to have in mind.
Another useful way to analyze a sentence is to list its subsentences. In our example:
P_{0}
P_{1}
P_{2}
P_{0} ∧ P_{1}
( P_{0} ∧ P_{1} ) ∨ P_{2}
Notice that proper subsentences are shorter in length. Also observe that proper subsentences of sentences on the list occur earlier on the list. This is always possible and sometimes useful in logic.
First define a function S with dom ( S ) = ω by recursion as follows.
What is really going on here is that S ( n ) is the set of sentences of complexity ≤ n where complexity is defined by recursion as follows.
Assume the following.
Then Σ = { φ ∣ φ is a sentence }.
{ φ ∣ φ is a sentence } is countable.
By induction, we prove that S ( n ) is countable.
S ( 0 ) is the union of the countable set { P_{i} ∣ i ∈ ω } and the pair { ⊤ , ⊥ } , so S ( 0 ) is countable.
Assume S ( n ) is countable.
By definition, S ( n + 1 ) is the union of six sets:
S ( n )
{ ¬ φ_{i} ∣ i ∈ ω }
{ φ_{i} ∧ φ_{j} ∣ i , j ∈ ω }
{ φ_{i} ∨ φ_{j} ∣ i , j ∈ ω }
{ φ_{i} → φ_{j} ∣ i , j ∈ ω }
{ φ_{i} ↔ φ_{j} ∣ i , j ∈ ω }
Using the induction hypothesis, we see that each of these six sets is countable.
Since S ( n + 1 ) is a union of six countable sets, it is also countable.
That completes the induction.
Now { S ( n ) ∣ n ∈ ω } is a countable collection of countable sets.
Therefore, its union { φ ∣ φ is a sentence } is countable by Lemma 1.4.
QED
Each structure A has a corresponding truth function, Truth_{A}, which is a certain function from { φ ∣ φ is a sentence } to { 0 , 1 }.
Truth_{A} is recursively defined as follows.
(The members of a theory are called its axioms.)
(We also say A satisfies φ.)
(We also say A satisfies Σ.)
(That is, φ ⊨ ψ and ψ ⊨ φ.)
(That is, { } ⊨ φ. This may be abbreviated as just ⊨ φ.)
P_{0} | P_{1} | P_{2} | ( P_{0} → P_{1} ) ↔ P_{2} |
0 | 0 | 0 | 0 |
0 | 0 | 1 | 1 |
0 | 1 | 0 | 0 |
0 | 1 | 1 | 1 |
1 | 0 | 0 | 1 |
1 | 0 | 1 | 0 |
1 | 1 | 0 | 0 |
1 | 1 | 1 | 1 |
The first row of this table tells us that if A is any structure with
A ( P_{0} ) = A ( P_{1} ) = A ( P_{2} ) = 0,
then
Truth_{A} ( ( P_{0} → P_{1} ) ↔ P_{2} ) = 0.
The second row of the table tells us that if A is any structure with
A ( P_{0} ) = A ( P_{1} ) = 0 and A ( P_{2} ) = 1,
then
Truth_{A} ( ( P_{0} → P_{1} ) ↔ P_{2} ) = 1.
Notice how the values of A ( P_{n} ) for n > 2 are irrelevant to this example.
Our goal is to develop a formal proof system for propositional logic that mirrors what goes on in everyday mathematics. You can imagine that there are many legitimate ways to do this. In fact, we will present two versions. To keep the straight which is which, we will use different names. The words "proof" and "deduction" are synonyms in English but their formal versions will mean different things.
Returning to propositional logic, consider a theory Σ and a sentence ψ. We will explain what is meant that from Σ we may deduce ψ. In this case, we will write Σ ⊢ ψ. Before giving the general definition of Σ ⊢ ψ we list the deduction rules.
⊤-in | { } ⊢ ⊤ | ⊥-out | { ⊥ } ⊢ φ | |||||
¬-in | Σ ∪ { φ } ⊢ ψ and Σ ∪ { φ } ⊢ ¬ ψ implies Σ ⊢ ¬ φ | ¬-out | { ¬ ¬ φ } ⊢ φ | |||||
∧-in | { φ , ψ } ⊢ φ ∧ ψ | ∧-out | { φ ∧ ψ } ⊢ φ and { φ ∧ ψ } ⊢ ψ | |||||
∨-in | { φ } ⊢ φ ∨ ψ and { ψ } ⊢ φ ∨ ψ | ∨-out | Σ ∪ { φ } ⊢ χ and Σ ∪ { ψ } ⊢ χ implies Σ ∪ { φ ∨ ψ } ⊢ χ | |||||
→-in | Σ ∪ { φ } ⊢ ψ implies Σ ⊢ φ → ψ | →-out | { φ, φ → ψ } ⊢ ψ | |||||
↔-in | { ψ → φ , φ → ψ } ⊢ φ ↔ ψ | ↔-out | { φ ↔ ψ } ⊢ φ → ψ and { φ ↔ ψ } ⊢ ψ → φ | |||||
R1 | If Δ ⊆ Σ and Δ ⊢ φ, then Σ ⊢ φ. | |||||||
R2 | If Σ ⊢ φ_{i} for every i < n and { φ_{i} ∣ i < n } ⊢ ψ, then Σ ⊢ ψ. | |||||||
R3 | If φ belongs to Σ, then Σ ⊢ φ. |
Some of the deduction rules have popular alternative names:
Deductions are justified by applying the deduction rules finitely many times. Before stating the definitions of "deduction" and "justification", it is best to give a couple of illustrative examples.
Notice that the last line is rule R3. In other words, rule R3 can be justified by the other rules, so we do not really need to include it in our system. Officially, we keep it because it seems so basic and is used so often. But when it suits us, we may assume it was not used in a justification. Rule R3 corresponds to the idea that "every assumption is a theorem".
In general, a justification of length n is a finite sequence ( ( Γ_{0} , ψ_{0} ) , … , ( Γ_{n} , ψ_{n} ) ) such that, for every j ≤ n, Γ_{j} ⊢ ψ_{i} follows from Γ_{i} ⊢ ψ_{i} for i < j and a deduction rule. We define Σ ⊢ φ iff there is such a justification with Γ_{n} equal to Σ and ψ_{n} equal to φ. In this case, we say that φ is deducible from Σ and φ is theorem of Σ.
We remark that some of the names of the mathematical objects we are studying are words that we will continue to use in the usual way in English. This leads to slightly odd sentences such as, "Here is a deduction that there is a deduction from the theory Σ of the sentence φ." If we wanted to avoid using the same expressions in different ways, we could add the word "formal" in key places to obtain, "Here is a deduction that there is a formal deduction from the formal theory Σ of the formal sentence φ." Later, when we study other kinds of languages, we could also add the word "propositional" to keep things crystal clear.
QED
(You are asked to complete the proof of Theorem 2.3 in Exercise 2.9.)
Suppose Σ ⊢ φ.
Then there is a finite Δ ⊆ Σ such that Δ ⊢ φ.
Let Δ be the union of Δ_{i} for i < n.
Then Δ is a finite subset of Σ and Δ ⊢ φ_{i} for all i < n by rule R1.
By rule R2, Δ ⊢ ψ.
QED
(You are asked to complete the proof of Lemma 2.4 in Exercise 2.10.)
Here are especially important properties that a theory might have.
Let Σ be a theory. The following are equivalent.
Obviously, 2 implies 3.
Assume 3.
Then Σ ∪ { ¬ ⊥ } ⊢ φ and Σ ∪ { ¬ ⊥ } ⊢ ¬ φ by rule R1.
Hence, Σ ⊢ ¬ ¬ ⊥ by the ¬-in rule.
Thus, Σ ⊢ ⊥ by the ¬-out rule.
Therefore, 1 holds.
QED
Let Σ be a consistent theory and φ be a sentence.
Then either Σ ∪ { φ } is consistent or Σ ∪ { ¬ φ } is consistent (or both).
QED
Let Σ be a consistent theory.
Then there is a consistent theory Γ ⊇ Σ such that for every sentence φ, either φ belongs to Γ or ¬ φ belongs to Γ.
In particular, every consistent theory has a complete consistent extension.
Say { φ ∣ φ is a sentence } = { φ_{n} ∣ n = 0 , 1 , 2 , … }.
Using Lemma 2.6, recursively define an infinite sequence of consistent theories
Σ = Γ_{0} ⊆ Γ_{1} ⊆ ⋅ ⋅ ⋅ ⊆ Γ_{n} ⊆ ⋅ ⋅ ⋅
such that Γ_{n+1} is either Γ_{n} ∪ { φ_{n} } or Γ_{n} ∪ { ¬ φ_{n} }.
Let Γ be the union of these theories.
Clearly Γ is complete.
For contradiction, suppose that Γ is inconsistent.
That is, Γ ⊢ ⊥.
By Lemma 2.5, there is a finite Δ ⊆ Γ such that Δ ⊢ ⊥.
Pick a natural number n large enough that Δ ⊆ Γ_{n}.
By rule R1, Γ_{n} ⊢ ⊥.
Hence Γ_{n} is inconsistent, which is a contradiction.
QED
Assume Σ is a consistent theory. Then Σ has a model.
To prove Theorem 2.8, it suffices to show that Γ has a model because if A ⊨ Γ, then A ⊨ Σ.
Claim A. For every sentence φ, φ belongs to Γ iff ¬ φ does not belong to Γ.
Should Claim A fail, there would be a sentence φ such that both φ and ¬ φ belong to Γ. But then Γ would be inconsistent by Lemma 2.5.
Claim B. Every theorem of Γ belongs to Γ.
Should Claim B fail, there would be a sentence φ such that Γ ⊢ φ and ¬ φ belongs to Γ, hence Γ ⊢ ¬ φ. But then Γ would be inconsistent by Lemma 2.5.
Define a structure A by setting A ( P_{n} ) = 1 iff P_{n} belongs to Γ. The following claim completes the proof of Theorem 2.8.
Claim C. For every sentence φ, Truth_{A} ( φ ) = 1 iff φ belongs to Γ.
The proof of Claim C is by induction on the complexity of φ using Lemma 2.1. Here are the key points.
As the induction hypothesis, assume that Claim C holds for φ and ψ.
QED
The next result is the converse of Soundness Theorem 2.3. Intuitively, it says that the system of deduction rules is complete in the sense that every logical consequence of a theory can be deduced. (The word "complete" is used many different ways!)
Assume Σ ⊨ φ. Then Σ ⊢ φ.
We claim that Σ ∪ { ¬ φ } is consistent.
Otherwise, by Lemma 2.5, for some sentence ψ, Σ ∪ { ¬ φ } ⊢ ψ and Σ ∪ { ¬ φ } ⊢ ¬ ψ.
By the ¬-in rule, Σ ⊢ ¬ ¬ φ.
By the ¬-out and R1 rules, Σ ⊢ φ.
This contradiction proves the claim.
By Theorem 2.8, there is a model A of Σ ∪ { ¬ φ }.
Then A is a model of Σ but not a model of φ.
Therefore Σ ⊭ φ .
QED
There are useful principles in mathematics that say a certain kind of object has a certain property if all of its small subobjects have the property. Often, these are called "compactness" principles.
Let Σ be a theory. Assume that every finite subtheory of Σ has a model. Then Σ has a model.
Some parts of everyday mathematical proofs boil down to nothing more than checking truth tables. After enough practice, we end up considering such parts of proofs to be routine. Even a computer can verify validity using truth tables! So it is reasonable to offer an alternative to our deduction system that takes this idea into account. To keep things straight, we call it a proof system.
A proof from a theory Σ is a finite sequence of sentences ( φ_{0} , … , φ_{n} ) such that for every k ≤ n,
Σ ⊢_{p} φ iff Σ ⊢ φ
We prove by induction on n that if ( φ_{0} , … , φ_{n} ) is a proof from Σ, then Σ ⊢ φ_{n}.
If φ_{n} is valid, then { } ⊨ φ_{n}, so Σ ⊨ φ_{n}, hence Σ ⊢ φ_{n} by Theorem 2.9.
If φ_{n} belongs to Σ, then Σ ⊢ φ_{n} by deduction rule R3.
Finally, suppose there are i , j < n such that φ_{j} is the sentence φ_{i} → φ_{n}.
By the induction hypothesis, we know Σ ⊢ φ_{i} and Σ ⊢ φ_{i} → φ_{n}.
By the →-out deduction rule (modes ponens), { φ_{i} , φ_{i} → φ_{n} } ⊢ φ_{n}.
By deduction rule R2, Σ ⊢ φ_{n}.
Right-to-left
It is enough to show that each of the deduction rules remains true if we replace ⊢ by ⊢_{p}.
We do this for some of the rules and leave the rest as an exercise.
⊤-in
⊤ is valid so ( ⊤ ) is a proof from { } of ⊤.
⊥-out
( ⊥ , ⊥ → φ , φ ) is a proof from { ⊥ } of φ.
¬-out
(¬ ¬ φ , ¬ ¬ φ → φ , φ ) is a proof from { ¬ ¬ φ } of φ.
∧-in
( φ , ψ , φ → ( ψ → ( φ ∧ ψ ) ) , ψ → ( φ ∧ ψ ) , φ ∧ ψ ) is a proof from { φ , ψ } of φ ∧ ψ.
∧-out
Use ( φ ∧ ψ , ( φ ∧ ψ ) → φ , φ ) and ( φ ∧ ψ , ( φ ∧ ψ ) → ψ , ψ ).
∨-in
Use ( φ , φ → ( φ ∨ ψ ) , φ ∨ ψ ) and ( ψ , ψ → ( φ ∧ ψ ) , φ ∨ ψ ).
→-out
Use ( φ , φ → ψ , ψ ).
→-in
Let ( ψ_{0} , … , ψ_{m} ) be a proof from Σ ∪ { φ }.
We must find a proof from Σ of φ → ψ_{m}.
If ψ_{m} is either φ or valid, then φ → ψ_{m} is valid and ( φ → ψ_{m} ) is a proof from Σ of φ → ψ_{m}.
If ψ_{m} belongs to Σ, then ( ψ_{m} , ψ_{m} → ( φ → ψ_{m} ) , φ → ψ_{m} ) is a proof from Σ of φ → ψ_{m}.
Finally, suppose that there are i,j < m such that ψ_{j} is ψ_{i} → ψ_{m}.
By induction, there are proofs from Σ of φ → ψ_{i} and φ → ( ψ_{i} → ψ_{m} ).
Concatenate these two proofs (in either order) then concatenate by the following additional sentences:
QED