ECS 20 – Fall 2021 – Logic I
Today: Logic
Propositional logic: Boolean values, digital circuits, logic-design problems, satisfiable and tautological formulas, provability
Wikipedia page on
Propositional calculus: https://en.wikipedia.org/wiki/Propositional_calculus and on Boolean algebra https://en.wikipedia.org/wiki/Boolean_algebra
1
Propositional Logic = Propositional Calculus
= Sentential Logic = Sentential Calculus ≈ Boolean algebra
Universe of two points 𝔹𝔹 = {0,1} or, alternatively, 𝔹𝔹={F,T} or 𝔹𝔹={False,True}
That is, I will interchangeably use 0, F, False and 1, T, True. I have even seen examples where the Boolean values are regarded as {-1, 1}.
(The font for 𝔹𝔹 is blackboard bold: \mathbb{…} in LaTeX)
The 𝔹𝔹 stands for Boolean, named after , a 19th century mathematician.
It is wonderful thing having a universe of only two points—a way simpler
universe than the natural numbers, the integers, or the reals, where most of
you have been told to live for all of your math classes. In fact, I can’t for the
positiveintegers,Z ,whichisaterriblycomplicatedthingcomparedto Maybe you can go back and teach all the young children in your life
life of me understand why school children start their studies with the +
propositional logic, and let them not worry about those nasty integers until
they are older.
𝔹𝔹. Here are some sets you should know:
𝔹𝔹 = {0,1} // Booleans. Symbol is uncommon. Also written Z2
N = {0,1,2,3,…} // The natural numbers. I always include 0 Z = {…,-2,-1,0,1,2,…} // The integers
Q = the rational numbers = {a/b: a, b ∈ Z, b ≠0}
R = the real numbers
Just like integers and reals have operations defined on them, like addition
(+) and multiplication (·), and so do Boolean values.
If P and Q are variables represent Boolean values, then we define a sort of
multiplication on them as
P·Q –lotsofalternativenotations: P∧Q PandQ PANDQ PQ
P && Q
I’m using infix notation, but don’t let that confuse you as to the nature of the thing: a function from AND: 𝔹𝔹 × 𝔹𝔹 → 𝔹𝔹. We could just as well have used the more familiar prefix notation for functions, like AND(P,Q)
P ∨ Q P or Q P OR Q P || Q
PQ|P∨Q ———————- FFF FTT TFT TTT
2
What does it mean??
PQ|P∧Q
———————-
FFF
F T F Atruthtable TFF
TTT
To make a truth table you really need to know how to count in binary. Do you all know? 0, 1, 10, 11, 100, 101, …
Or, with leading zero, then, for example, 000, 001, 010, 011, 100, 101, 110, 111. Everybody follows this convention; please don’t write a truth table any other way.
Similarly, for OR, with it’s various notations
3 (As an aside, why do our truth table rows in this order? Practice counting in
binary. 0, 1, 10, 11, 100, 101, 110, 111, 1000, …)
We need at least one more operator, a unary operator NOT
¬P not P
P|¬P ———————- FT TF
_
NOTP !P P
We can put them together and make longer formulas
P and not(Q) or not(P) and Q
That’s actually an interesting function, we call it XOR: P xor Q P ⊕ Q P + Q
PQ|P⊕Q ———————- FFF FTT TFT TTF
Here’s another functionality that’s very useful: implies. P IMPLIES Q, or
PQ|P→Q ———————- FFT FTF TFT TTT
Andyetanother. Biconditional: P↔Q PIFFQ PiffQ P≡Q
PQ|P↔Q ———————- FFT FTF TFF TTT
4
You can either think of operators like ⊕, → , ↔ as “basic” operators of sentential logic or, alternatively, you can think of them as “syntactic sugar” – convenient short hand for formulas that are “actually” made of ∧, ∨, ¬ . (But, for that matter, did we really need all of ∧, ∨, ¬ ? Exercise: write OR using only AND and NOT; write AND using only OR and NOT. In fact, this is more than an exercise: it is a way to introduce DeMorgan’s Laws.)
Warm about the use of the word formal having two different meanings: rigorous and symbolic. Now we are going to treat logic formally in the second sense:
Definition: A well-formed formula (WFF) (of propositional logic) over a nonempty set of variables 𝒫𝒫 (finite or countably infinite) is:
(the variables may not contain any of the symbols: ¬ ∨ ∧ ( ) F T )
Do a truth table involving more than two variables, like
if s then x else y
• IfX∈𝒫𝒫thenXisaWFF
• IfαandβareWFFsthensoare:(¬α), (α∨β),(α∧ β),
// stop here: let’s treat the other binary operators as “syntactic sugar”
(Nothing else is a WFF.)
This is an example of a recursive definition.
Formulas are just strings: sequences of symbols from an alphabet.
• FandTareWFF
There are alternative ways to give a recursive definition like the one we just gave for a WFF. Here is how you would write it using a context-free grammar:
W 𝒫𝒫 | T | F | ( W ∨ W) | (W ∧ W) | ( ¬ W) 𝒫𝒫L|L N
L P | Q | R
N0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | NN
TheT,F,∨, ∧, ¬,P,Q,R,0,1,…,0arecalledterminalswhilethe W, S, N, 𝒫𝒫 are called nonterminals or variables.
Def: Atruthassignmenttoveraset𝒫𝒫 isamapt: 𝒫𝒫→𝔹𝔹. A t.a. is also called a model.
A t.a. gives a formula φ whose variables are in 𝒫𝒫 a truth value in the natural way; formally, we extend t to a t.a. on WFFs by asserting that
t(T)=T
t(F)=F
t((α ∨ β)) = t(α) ∨ t(β) t((α ∧ β)) = t(α) ∧ t(β) t((¬α)) =¬ t(α)
Another recursive definition. In this way we have extended the definition of t from o this larger domain of WFFs.
5
A different notation that captures the same thing is called Backus-Naur Form (more frequently called Form, or BNF). It’s nice for more explicitly distinguishing terminals and nonterminals.
Don’t confuse strings of symbols with their semantics (e.g., the wedge on the LHS of the third formula has a very different meaning on the RHS; there is a big difference between a formal symbol and a logical operation.
In common usage we use a precedence order allows us to omit many parenthesis, adopting a convention:
¬
∧
∨
→
↔ (orsomewouldputatsamelevelas→)
and right-to-left within a level (or some would say left-to-right; or some would say ill-defined).
Design something, say a majority circuit – returns 1 if a majority of its inputs are on. Do for 3 wires.
How would you do it for 100 gates? –or an addition circuit using a full adder
6
Define: a set of operators being logically complete.
Show that the following sets of operators are logically complete: {∧, ∨, ¬} {∧, ¬}
⊼ (write NAND as a wedge with a bar over it). ⊽ (similarly for NOR)
Definitions:
• A formula φ is satisfiable if some t.a. makes it true: there is a t.a. t such
that t(φ)=T
• A set of formula Γ is satisfiable if some t.a. makes all of them true. • A formula φ is tautological (or valid) if it is true for every t.a.
• ⊨ φ means φ is a tautology
• φandψare(logically)equivalent,φ≡ψ,if φ↔ψ isatautology
• Γ⊨ φ Every t.a. that makes all formula in Γ true makes φ true.
7
Describe Disjunctive Normal Form (DNF).
Proposition: Each WFF is equivalent to one in DNF.
Give a proof, and give an upper bound on the number of two-input gates to realize any n-input functionality.
Proposition: There is an algorithm (=a precisely-describable procedure, mechanism, recipe)
that, given a WFF of sentential logic, decides
– if it is a tautology.
– if it is a satisfiable.
– if it equivalent to some given, second formula.
Proof: “Truth-table algorithm” Example:
Contrapositive: ⊨ (P→Q) ↔ (¬Q → ¬P) prove
Discuss the inefficiency of the truth-table algorithm.
Remarkable claim: no efficient means are known for any of these problems.
(P→Q) ↔ (¬Q → ¬P) // this is a statement, might be true or false ⊨ (P→Q) ↔ (¬Q → ¬P) // an assertion that it’s always true
Some simple tautologies Velleman, How to Prove It, p. 21, 23, 47, 49 . You can check any of these with a truth table.
Associative: P ∧ (Q ∧ R) ≡ (P ∧ Q) ∧R //Mention the similarities to arithmetic
P ∨ (Q ∨ R) ≡ (P ∨ Q) ∨ R DeMorgan’s: ¬(P∧Q) ≡ ¬P∨¬Q
¬(P∨Q) ≡ ¬P∧¬Q Idempotent: P ∧ P ≡ P
P∨P ≡P
Contradiction P → Q ≡ ¬P ∨ Q P→Q≡ ¬(P∧¬Q)
Discuss the difference in meaning between:
8
//laws with ∨ corresponding to addition //and ∧ corresponding to multiplication
Formal Proofs
Discuss conventional proofs vs. formal proofs.
I now discuss formal proofs, although what mathematicians – and you – will mostly be producing conventional (informal) ones.
Following from Wikipedia, Propositional Calculus. Following 14 rules φ
9
One of the reasons to have axioms like the list just given is to develop a notion of “what is provable”” We will write Γ ⊢ φ if statement φ follows from Γ. Read: φ is provable from Γ. Turnstyle is the name of the symbol. List of logical symbols: https://en.wikipedia.org/wiki/List_of_logic_symbols
Formal proofs are quite different from conventional proofs, but a thesis in mathematics is that conventional proofs can be recast as formal ones. What are formal proof? They are syntactic objects in some formalized system. There are many choices one has in how to do the formulation, but here is what we would typically have: that a formal proof is a sequence of formula: φ1,…,φn whereeachφi iseither
– an assumption or
– an axiom (it appear on a list like Axiom List W) or
– it follows from a previous set of lines in the proof by one of
a number of enumerated rules – indeed we can make do with one rule, modes ponens,
4. P
5. Q
6. P ∨ R 7. S
8. SQ 9. T
i) (A→B) …
j) A …
k) B
modes ponens
Example:
⊢ (PQ)(P ∨ R → S)(SQ → T) → T
1. PQ assumption 2. P∨R→S assumption 3. SQ → T assumption
“conjunction elimination” (P ∧ Q → P) applied to (1) “conjunction elimination” (P ∧ Q→Q) applied to (1)
“disjunction introduction” (P ∨ R → P) applied to (5)
modus ponens (A→B A gives B) applied to (2) and (6) “conjunction introduction” (S, Q → SQ) applied to (7) and (5)
modus ponens applied to (3) and (8) {PQ, P∨R→S, SQ→T} ⊢ T or
therefore
⊢ (PQ)(P ∨ R → S)(SQ → T) → T //The given statement is provable
⊢ φ can derive (prove) φ (from the ∅ — no assumptions) Γ⊢φ canderiveφ fromΓ
10
Theorems that we won’t prove in this class.
Soundness: If ⊢φ then ⊨φ (More generally, Γ ⊢ φ implies Γ ⊨ φ )
Completeness: If ⊨ φ then ⊢ φ (More generally, Γ ⊨ φ implies Γ ⊢ φ )
COMPACTNESS: Let Γ be a set of WFFs.
Suppose that every finite subset of Γ is satisfiable. Then Γ is satisfiable.
(Contrapositive:
Let Γ be a set of WFFs.
Suppose that Γ is not satisfiable.
Then some finite subset of Γ is already not satisfiable)
Let’s use this in a fun example: TILING (Dominos) Can you tile the with tiles of specified types (adjacent edges of the same color)
Eg:
Make an example where the plane is and is not tileable. Indicate that, in ecs120, common to prove that the TILING decision question is undecidable. But not our interest here. We are interested in whether the tileability of the plane for a given set of tile types is FALSIFIABLE — is there a proof of untileability? There will be if the following is true:
If the plane is untellable, it is already untileable on some finite subset of the plane.
11
Not an obvious claim — a priori possible that plane is untileable even though every finite rectangle in it is tileable.
To prove from compactness: Introduce a variable
P[i,j,k]: there is a tile of type k at position (i, j ) Write a Boolean formula to capture
∨ P[i,j,k] k
– At least one tile per square: for all i, j,
– At most one tile per square: for all i, j, P[i,j,k] → P[i,j,k’] for all k ≠ k’.
P[i,j,k] → ( ∨ P[i+1,j,k’] ) k’
– Horizontal direction is good: for all i and j,
if a tile of type k’ may be put to the right a tile of type k
– Columns are good. Fall i and j, P[i,j,k] → ( ∨ k’ P[i,j+1,k’] ) if a tile of type k’ may be put above a tile of type k
Now: connect it to compactness theorem. The set Γ is all the formulas above. If it is unsatisfiable, then some finite subset of Γ0 is unsatisfiable. Let n be the largest index used by a variable in Γ0. Then the [-n..n] × [-n..n] subset of the plane is already untileable. That is, you can prove to someone that the plane is untileable.
Γ is satisfiable iff every the plane can be tiled with tiles of the given types.
The plane can be tiled iff every n × n subset of it can be.
In the language you will learn in ecs120, the complement of tiling is recursively enumerable (r.e.)
A gap between Boolean expressions in modern programming languages and those in mathematics:
12
13 In most modern programming languages, like C, Java, and Python, short
”’Short-circuited evaluation in Python
”’
if (0<1 or 0/0==0): print("Hi")
if (0/0==0 or 0<1): print("there")
Hi
Traceback (most recent call last):
File "main.py", line 6, in
if (0/0==0 or 0<1): print("there")
ZeroDivisionError: division by zero
...Program finished with exit code 0
Hmm. Doesn’t this mean that if we can’t even reason about a program that B1 or B2 is the same as B2 or B1, then it’s hard to reason anything about real programs, right? Right!