Lecture 2
Logic and Proof
The Story So Far
•	Syntax versus semantics
•	Formal Systems
>	language: alphabet  + grammar
>	inference system: axioms + rules of inference
>	theorem, proof, deduction
•	Semantics
>	interpretation
>	consistency (soundness), completeness
Basic Elements
Next Two Lectures
•	We will look at two specific formal systems:
>	Propositional logic
>	Predicate logic
•	We will also briefly examine some of the main proof styles used for these systems
>	Equational reasoning
>	Proof by contradiction
>	Proof by case analysis
>	Natural deduction
Propositions
•	A proposition is a statement that is either true or false (but not both).
•	Examples
>	Pittsburgh is the home of the Pirates
>	Pittsburgh is the capital of Pennsylvania
•	The same proposition can often be expressed in several ways.
•	Examples
>	five is bigger than four
>	four is less than five
>	5 > 4
Propositional Logic: Syntax
•	Alphabet: {P,Q,R, ..., Ÿ, ⁄, ~, ﬁ, €}
•	Grammar:
sentence = “P” | “Q” | “R” | ...
| “~”, sentence
| “(”, sentence, “⁄“, sentence, “)”
| “(”, sentence, “Ÿ“, sentence, “)”
| “(”, sentence, “ﬁ“, sentence, “)”
| “(”, sentence, “€“, sentence, “)”
we usually drop the parentheses when the resulting sentence is unambiguous
Propositional Logic: Semantics
•	The meaning of a propositional wff is given as follows:
>	each primitive symbol (P, Q, R, ...) is given an interpretation as a proposition (with an associated truth value)
example: P => today is Thursday, ...
>	the meaning (truth or falsity) of a compound wff is then determined by a set of standard tables:
example:
Semantic Turnstyle
•	If a sentence W is true whenever a list of sentences P are true, we write P |= W
•	We say W is a semantic consequence of P.
•	Example: PŸQ |= P ⁄ Q
•	Note this is all in the semantic domain
Terminology & Special Cases
•	A sentence of the form 
>	A Ÿ B is called a conjunction
»	A and B are conjuncts
>	A ⁄ B is called a disjunction
»	A and B are disjuncts
>	A ﬁ B is called an implication
»	A is the antecedant; B is the consequent
•	Some sentences always interpret to true.
>	these are called tautologies
>	example: a sentence of the form A ⁄ ~A, where A is any proposition
•	Some sentences always interpret to false.
>	these are contradictions, or inconsistencies
>	example: a sentence of the form A Ÿ ~A, where A is any proposition
Propositional Calculus
•	To complete our system we need a set of inference rules (called a calculus, here)
•	One way to represent these rules is in the form:
if we have proved these facts
we can conclude these facts
•	Examples
A Ÿ B	   A		A, A ﬁ B
    A	A ⁄ B		      B
•	These are given names (resp):
Ÿ-elimination, ⁄-introduction, ﬁ-elimination
Example
•	Prove:  (P Ÿ Q)  |-   (P ⁄ Q)
•	Derivation:
>	P Ÿ Q		premise
>	P			Ÿ-elimination
>	P ⁄ Q		⁄-introduction
About Proofs
•	There are many styles (or techniques) of proof. 
•	SEM presents a style called “natural deduction”
•	In this style a proof is constructed as a tree.
•	However there are a lot of other styles that we will use as needed.
•	Many of these center around the application a particular inference rule. 
Natural Deduction
•	Example of Derivation 2.4 and Theorem 2.1 done on board 
•	In practice, proof typically is constructed by working backwords, using the form of the goal as the guide to rule selection
>	Example: if have to prove P ﬁ Q, then reach for ﬁ -introduction
•	Use of indentation helps to keep assumption scopes clear
Some Other Proof Styles
•	Style 1: simple application of rules 
>	we have already seen this a couple of times
>	note for each step of proof write justification in terms of rule and lines on which it depends
•	Style 2: proof by contradiction
>	assume that the conclusion is not true and derive something that we know to be false
•	Style 3: proof by cases
>	break proof in to separate parts and then combine
•	Style 4: modus ponens
>	Show  P  and P ﬁ Q. Then conclude Q.
Relation to Natural Deduction
•	Many of the inference rules for Natural Deduction are better known by the proof technique with which they are associated
>	 ~-introduction = proof by contradiction
>	 ⁄-elimination = proof by cases
>	 ﬁ-elimination = modus ponens
Equivalence
•	We augment our formal system with a new symbol
•	Two sentences are equivalent (∫ ) iff their truth value is the same under every interpretation.
•	Example: (P ﬁ  Q) ∫ (~P ⁄ Q)
•	There is a collection of properties of equivalence, summarized on page 26 of SEM.
>	These can be used in an “equational” style to do proof.
>	Properties include usual associative, commutative, distributive properties of the connectors
Example
Prove: ~ (P Ÿ  ~Q) ∫  (Q  ⁄ ~P)
Proof:
~ (P Ÿ  ~Q)
        ∫  		DeMorgan
~ P ⁄ Q
        ∫  		⁄-Commutative
Q  ⁄ ~P
Relation Between Syntactic and Semantic Domain
•	Propositional Calculus is Consistent
>	That is, anything that can be proved it is valid
>	If  P |- W then P |= W
•	Propositional Calculus is Complete
>	That is, anything that can be is valid can be proven using the inference rules
>	If  P |= W then P |- W
•	This allows us to shift between the two worlds
•	In particular we can substitute € for ∫ 
To show |-  P ∫ Q we can demonstrate |=  P ∫ Q
Predicate Logic
Predicates (2) 
Predicates (3)
•	For the moment we will assume that the sets that are quantified over are understood by context
examples: " x  ∑  P(x),  $ x  ∑ Q(x)
•	You can think of a predicate as a boolean valued function: when applied to an argument it returns true or false.
•	Predicates may have n arguments
>	examples: >, is-pythagorian
Predicate Logic: Syntax
•	Alphabet: as with propositional logic, but includes quantifiers (", $) and  ∑
>	" is called a “universal” quantifier
>	$  is called an “existential” quantifier
•	Grammar: see SEM
>	but note every quantified expression has a  ∑
•	Can nest quantified expressions
>	" x  ∑  (" y ∑ ($ z  ∑  P(x,y,z)))
>	usually leave out the parens
>	combine adjacent variables with same quantifier.
>	so this becomes " x, y ∑ $ z  ∑  P(x,y,z)
Predicate Logic: Semantics
•	More involved than propositional logic
•	Basic idea is that sentence
" x  ∑  P(x) is true iff P is true of all values of x, and
$ x  ∑ Q(x) is true iff Q is true for some value of x
Predicate Calculus
•	As with Propositional Logic we introduce a set of deductive rules.
•	Similar to situation before
>	SEM uses natural deduction style
Equality
•	We now add one more symbol to Predicate Logic: = to represent that two entities are the same.
•	This is equivalent to having a special predicate “equals”, but we use the more common infix notation.
•	We also introduce several new rules to our deductive apparatus.
•	The most important of these is:
Substitution rule:
        m = n, S(n)
          S[m/n]
Theories
•	We can do a lot with just logic.
•	But sometimes we want to introduce special axioms to describe a specific phenomenon.
•	Then we are interested in the consequences of those axioms (given the other rules of deduction).
•	These consequences are called a theory.
Examples
•	Some general theories that we will encounter in this course
>	set theory
>	theory for sequences
>	theory for concurrent processes
•	Other theories we will make up on the spot to characterize a software system
>	example: theory of telephones for a switching system
>	example: theory of devices and event processing for real-time system
>	homework problems explore some of these