CS262 Logic and Verification Lecture 2: Basics of propositional logic
CS262 Logic and Verification 1 / 18
Propositional logic
Copyright By PowCoder代写 加微信 powcoder
A formal system for reasoning about propositions
Proposition = Formula = Statement
Which of the following are propositions? It is raining.
Every natural number has a successor.
Have a nice day.
You may have soup or melon for your starter. Will it never end?
Those for which it makes sense to ask: is it true or false?
CS262 Logic and Verification 2 / 18
Atomic vs. compound propositions
Consider the following propositions: It is raining.
Either it is raining or I will hang the washing outside, and if I hang the washing outside then it will dry more quickly.
If it is raining then I take my umbrella. I have not taken my umbrella. Therefore it is not raining.
CS262 Logic and Verification 3 / 18
The form of an argument
Consider the following two propositions:
If it is raining then I take my umbrella. I have not taken my umbrella. Therefore it is not raining.
If I get all the questions right then I get full marks. I have not got full marks. Therefore I have not got all the questions right.
It’s the form of the argument that matters rather than the meanings of the sentences.
CS262 Logic and Verification 4 / 18
Our propositional language
Atomic formulas are the most basic propositions (indecomposable) E.g: p =“It is raining”
q =“I take my umbrella”
Logical connectives/operators allow us to build more complicated
propositions
¬ negation “not p”
∧ conjunction “p and q”
∨ disjunction “p or q”
→ implication “p implies q” “If it is raining then I take my umbrella”
“It is not raining.”
“It is raining and I take my umbrella” “It is raining or I take my umbrella”
More binary connectives in the exercises. Will use ◦ ∈ {∧, ∨, →, . . .} as general notation.
CS262 Logic and Verification
Syntax of propositional formulas
Propositional formulas are exactly those that can be constructed by a finite number of applications of the following rules:
Propositional variables p, q, r , . . . and ⊤ and ⊥ are atomic formulas. If X is a formula then so is ¬X.
If X and Y are formulas then so is (X ◦Y), where ◦ is any binary connective (e.g., ◦ = {∧, ∨, →, . . .}).
((p ∨ ¬p) ∧ (¬p ∨ ⊥)) ¬¬¬⊤
Counterexamples:
CS262 Logic and Verification
Conventions
May leave out brackets where there is no ambiguity: p ∨ q = (p ∨ q)
p∧q∧r =(p∧q)∧r =p∧(q∧r) p∨q∨r =(p∨q)∨r =p∨(q∨r)
But the following is ambiguous:
p → q → r, because (p → q) → r ̸= p → (q → r)
CS262 Logic and Verification 7 / 18
Parse tree
We can inductively construct a parse tree for any propositional formula: For any atomic formula X, the parse tree has a single node labeled X.
The parse tree for ¬X has a node labeled ¬ as the root, and the parse tree for X as the unique subtree of the root.
The parse tree for (X ◦ Y ) has a node labeled ◦ as the root, and the parse trees for X and Y as its left and right subtree.
Example: ((p ∧ ¬q) → (r ∨ (q → ¬p))) Each subtree is a subformula.
CS262 Logic and Verification 8 / 18
Draw parse trees for the following formulas: (p ∧ (¬⊤ → r))
(p → ((q ∨ r) → ¬¬¬r))
CS262 Logic and Verification 9 / 18
Induction and recursion
Based on our inductive definition, we can define recursive functions on formulas.
deg(A) = 0 if A is an atomic formula, deg(¬X) = 1 + deg(X) if X is a formula,
deg(X◦Y)=deg(X)+deg(Y)+1ifX andY areformulas. We can also argue about formulas by induction.
Theorem: The degree of a formula equals the number of inner nodes of the parse tree.
CS262 Logic and Verification 10 / 18
Semantics of propositional logic
In propositional logic, formulas can have one of two possible values True=T or False=F
A truth table lists each possible combination of truth values for the variables of a Boolean function (=truth function)
f : {T,F}n → {T,F}, and specifies the function value in each case.
n variables; gives a table with 2n rows order of rows is irrelevant
CS262 Logic and Verification 11 / 18
Truth tables of connectives
Each connective is defined by its truth table:
Unary connective Binary connectives
X ¬X X Y X∧Y X∨Y X→Y … TFTTTTT FTTFFTF
FTFTT FFFFT
Nullary connectives ⊤=“top” and ⊥=“bottom” ⊤⊥
CS262 Logic and Verification
Valuations
A valuation is a mapping v from the set of propositional formulas to the set of truth values {T,F} satisfying the following conditions:
v(⊤) = T; v(⊥) = F, v(¬X) = ¬v(X),
v (X ◦ Y ) = v (X ) ◦ v (Y ).
To examine all interesting valuations for a given formula, it is enough to specify v for each variable. The value of all subformulas can then be deduced bottom-up (in the parse tree).
Example: if v is a valuation such that v(p) = T and v(q) = F, and X = ¬p ∨ (¬q → p)
then v(¬p) = F, v(¬q) = T, v(¬q → p) = T, and v(X) = T The truth table of a formula lists all possible valuations.
CS262 Logic and Verification
Truth table of compound formulas
Example 1: (p∧q)∨(¬p∧¬q)
p q (p∧q) ∨ (¬p ∧ ¬q) TTTTFFF TFFFFFT FTFFTFF FFFTTTT
CS262 Logic and Verification 14 / 18
Truth table of compound formulas
Example 2: p → (q ∧ r)
p q r p → (q∧r) TTTTT TTFFF TFTFF TFFFF FTTTT FTFTF FFTTF FFFTF
CS262 Logic and Verification 15 / 18
Tautologies, contradictions
A formula that evaluates to T under all valuations is called a tautology. A formula that evaluates to F under all valuations is called a
contradiction.
A formula that evaluates to T for some valuation is called satisfiable.
CS262 Logic and Verification 16 / 18
Propositional consequence
We say that a formula X is a consequence of a set S of formulas, denoted S |= X , provided that X maps to T under every valuation that maps every member of S to T.
X isatautologyifandonlyif∅|=X,whichwewriteas|=X.
{ p , p → q } |= q { p , q , r } |= p
|= (p ∨ ¬p)
Counterexamples:
p ∨ q |= q p → q |= p
CS262 Logic and Verification
Limitations of truth tables
Truth tables are great, but there are also disadvantages: Space requirements: 2n rows for n variables
Often wasteful; e.g.: p ∨ q ∨ r ∨ s ∨ t ∨ ¬p (look at binary decision diagrams)
Symmetry or structure of formulas is disguised; e.g.: f(x1,…,xn)=T iffandonlyifandoddnumberofxi =T
CS262 Logic and Verification 18 / 18
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com