Transcript A ^ B

An Introduction to Classical Logic
(propositional and Predicate Logic)
Lecture Notes for ISA 780/SWE 623
by
Duminda Wijesekera
ISA 780/SWE 623Classical
Logic
Duminda Wijesekera
1
Propositional and Predicate Logic
• Propositional Logic
– The study of statements and their connectivity
structure.
• Predicate Logic
– The study of individuals and their properties.
• Study syntax and semantics for both.
• Propositional logic more abstract and hence less
detailed than predicate logic.
ISA 780/SWE 623Classical
Logic
Duminda Wijesekera
2
Propositional Logic: Syntax
• A collection of atomic propositional symbols.
– Say A = { ai : 0 < i }. A special atom _|_ for contradiction
• A collection of logical connectives.
– (and) ^, (or) v, ( not )  , (implies) =>
• Inductively define propositions as:
If X,Y are propositions, so are :–
X ^ Y, X v Y, X => Y,  X.
• Examples:
– a1^a2, (a =>a2)v(a3^( a4)) are propositions.
ISA 780/SWE 623Classical
Logic
Duminda Wijesekera
3
Propositional Logic: Semantics
• A model M of a propositional language consists
of
– a collection of atoms, say B = { bi : 0 < i }, where _|_
is excluded from B, and
– a partial mapping M from A = { ai : 0 < i } to B = {
bi : 0 < i }.
– If M(ai) e B, we say that ai is true in M. We write
“ai is true in M” as M |= ai. (Read M satisfies ai).
– ╞ is referred to as the satisfaction relation.
ISA 780/SWE 623Classical
Logic
Duminda Wijesekera
4
Propositional Semantics: Continued
• Extend M, and therefore the satisfaction
relation to all propositions using the
following inductive definition:
– M ╞ X ^ Y iff M ╞ X and M ╞ Y.
– M ╞ X v Y iff M ╞ X or M ╞ Y.
– M ╞ X => Y if M ╞ X then M ╞ Y.
– M ╞  X, if it is not the case that M ╞ X.
• Notice usage of truth tables
ISA 780/SWE 623Classical
Logic
Duminda Wijesekera
5
Propositional Logic: Example
• B = { a1, a3} where M given as M(a1) = a1 and M(a2) = a2
has the following properties.
–
–
–
–
M ╞ a1
M ╞ a1 ^ a3
M ╞  a2
M ╞ a2 => a4
• M does not satisfy the following propositions.
– M ╞ a4
– M ╞ a1 => a4
ISA 780/SWE 623Classical
Logic
Duminda Wijesekera
6
Propositional Logic: Proofs
• What formulas hold in all models ?
• I.e. can we check if a given proposition is
true in all models without going through all
possible models?
• Need proofs to answer this question.
• We use Natural Deduction proofs.
• Recommended: Read Ch 2 of Logic and
Computation by L.C. Paulson.
ISA 780/SWE 623Classical
Logic
Duminda Wijesekera
7
Natural Deduction for Prop. Logic
• Proofs are trees of formulae made by applying
inference rules.
• An inference rule is of the form:
A1 …… An
B
• Here A1 ….. An are said to be premises (or
antecedents) of the rule, and B is said to be the
conclusion (consequent) of the rule.
ISA 780/SWE 623Classical
Logic
Duminda Wijesekera
8
Natural Deduction for Prop. Logic
• Hence a proofs is a trees whose
– Root is the theorem to be proved,
– Branches are rules, and
– Leaves are the assumptions (axioms) of the proof.
• Example
 Assumptions
– A1 A2 A3C1 C2
B1
B2
D
 Applications of rules
 Theorem being proved
• There are introduction and elimination rules for each
connective in Natural Deduction proof systems.
ISA 780/SWE 623Classical
Logic
Duminda Wijesekera
9
Rules for Conjunction
• Introduction
A
B
A^B
• Elimination
A^B
A
ISA 780/SWE 623Classical
Logic
A^B
B
Duminda Wijesekera
10
Rules for Disjunction
• Introduction
A
AvB
B
AvB
• Elimination
[A]
C
AvB
[B]
C
C
• [X] denotes discharged assumption X.
ISA 780/SWE 623Classical
Logic
Duminda Wijesekera
11
Rules for Implication
• Introduction
[A]
B
A => B
• Elimination (Modus Ponens)
A => B
A
B
ISA 780/SWE 623Classical
Logic
Duminda Wijesekera
12
Rules for Negation
•  B interpreted as ( B => _|_). Hence we get the
following rules from those of implication.
•  Introduction
 Elimination
B
B
_|_
[B]
_|_
________
 B
• Special Contradiction Rule:
ISA 780/SWE 623Classical
Logic
Duminda Wijesekera
B
_|_
__________
B
13
Propositional Proofs: Examples
• Prove: ( A ^ B ) => (A v B)
• Notice:
– The outermost connective is =>. Hence, the last step of
the proof must be an implication introduction.
– That means, we must assume ( A ^ B ) and prove (A
v B), and then discharge the assumption by using =>
introduction rule.
– In order to prove (A v B) from ( A ^ B ), we must use
v –introduction, and hence must prove either A or B
from ( A ^ B ).
– This plan forms a skeleton of a proof.
ISA 780/SWE 623Classical
Logic
Duminda Wijesekera
14
Prop. Proof: Example Continued
• Prove: ( A ^ B ) => (A v B)
[A ^ B ]
A
^ elimination
AvB
v introduction
( A ^ B ) => (A v B)
=> introduction
• Proofs are analyzed backwards, I.e. start unraveling the
logical structure of the conclusion and work backwards to
the assumptions. Draw out a plan based on your analysis
and write down the formal proof.
ISA 780/SWE 623Classical
Logic
Duminda Wijesekera
15
Derived Rules
• These are rules derived from other rules.
• Example:
A^B
B^A
• Here is the derivation:
A^B B^A
B
A
^ elimination
B^ A
^ introduction
ISA 780/SWE 623Classical
Logic
Duminda Wijesekera
16
Soundness and Completeness
• A rule A1 …… An is said to be sound if for every
B
model in which all of A1 …… An are true, then so is
B. I.e. if M ╞ A1 , …… , M |= An, then M ╞ B.
• A collection of rules are sound if all rules in the
collection is sound.
• A collection of rules is complete if M ╞ A for all
models M, then A is provable. I.e. there is a proof of A
using the given set of rules. (Denoted |R-- A ) where R
is the set of rules.
ISA 780/SWE 623Classical
Logic
Duminda Wijesekera
17
Predicate Logic
• Language to describe properties of individuals.
• Thus, syntax is able to describe individuals, their
properties (relationships) and functions.
– These are to be thought of as names of individuals,
properties (relationships) and functions.
– Models are “incarnations” of these individuals,
properties (relationships) and functions.
• More detailed than propositional logic.
ISA 780/SWE 623Classical
Logic
Duminda Wijesekera
18
Predicate Logic: Syntax
• A collection of constants– say { ci : i >= 0 }.
– Constants are names for individuals. E.g.: 0, 1.
– Note: not all individuals in a model have names.
• A collection of variables– say { xi : i >= 0 }.
– Needed to generically refer to individuals.
– Think of them as standing in place of pronouns like it, she.
• A collection of function symbols- say { fi : i >= 0 }.
– May be of different arities, and may be typed. E.g.: +(x,y)
• A collection of predicate symbols- say { pi : i >= 0 }.
– May be of different arities.
– Encodes properties of individuals. E.g.: prime(x).
ISA 780/SWE 623Classical
Logic
Duminda Wijesekera
19
Predicate Logic
Recursive Definition of Terms
• Every variable is a term.
• Every constant is a term.
• If fi is an n-ary function symbol and t1, .., tn are terms,
then fi(t1, .., tn) is a term.
• We use {ti : i <=0 } for the collection of terms.
• Examples:
– f(x, g(2, y)) is a term, where f, g are function symbols and x, y
are variables.
– +( x, *(3,y)) is a term in arithmetic usually written as
x + (3*y)
ISA 780/SWE 623Classical
Logic
Duminda Wijesekera
20
Recursive Definition of Formulas
• If pi is an n-ary predicate symbol and t1, .., tn are terms,
then pi(t1, .., tn ) is an atomic formula.
• If A and B are formulas, then so are:
– A ^ B, A v B,  A, A => B.
–  xi A(xi),  xi A(xi), where xi is a variable.
• ,  are referred to as the universal and existential
quantifier, respectively.
• A formula that does not have either quantifier is said to
be a quantifier free.
ISA 780/SWE 623Classical
Logic
Duminda Wijesekera
21
Free and bound Variables
• In  x A(x), the variable x is said to be bound; meaning
the name x plays no significant role. (compare with he,
she, it)
• A variable x occurs bound in a formula if x or x is a
part of it. More precisely, x occurs bound in:
– y A(y) or y A(y) if x and y are the same variable.
–  A if x occurs bound in A.
– A ^ B, A v B, A => B if x occurs bound in either A
or B.
ISA 780/SWE 623Classical
Logic
Duminda Wijesekera
22
Substitutions
• If A is a formula, t is a term and x is a
variable, then A[t/x] is the formula obtained
by substituting t for x in A.
– A[t1/x1, … tn/xn] is the formula resulting in
simultaneously substituting x1, …xn by t1, …tn.
– Note: Simultaneous substitution Q(x,y)[x/y,y/x]
yields Q(y,x) but iterated substitution
Q(x,y)[x/y][y/x] yields Q(y,y).
ISA 780/SWE 623Classical
Logic
Duminda Wijesekera
23
Substituting Terms for Variables
• In A[t/x], the free variables of t stand the danger of
becoming bound in A. Hence, need a precise definition.
– If x is y then y A(y) [x/y] is y A(y). If not let z be a
fresh variable (I.e. not in t, x) then (y A(y) )[t/x] is
z (A(z/y) [t/x]).
– Similar definition for y A(y).
• Examples:
– y (y = 1) [y/y] is y (y = 1). Here x is y and t is x.
– y (y+1 > x) [2y+x/x] is z ((z+1>x)[2y+x/x] I.e.
z (z+1>2y+x). Here t is (2y+x).
ISA 780/SWE 623Classical
Logic
Duminda Wijesekera
24
Substituting Terms Continued
•
•
•
•
( A )[t/x] is  (A [t/x])
(A ^ B) [t/x] is (A[t/x] ^ B[t/x])
(A v B) [t/x] is (A[t/x] v B[t/x])
(A => B) [t/x] is (A[t/x] => B[t/x])
• Pi(t1, .. tn) [t/x] is Pi(t1[t/x], .. tn[t/x]) for
predicate symbol Pi.
ISA 780/SWE 623Classical
Logic
Duminda Wijesekera
25
Predicate Logic: Semantics
• A model consists of
– A set (of individuals), say A = { ai : i >= 0 }.
– A set of total functions Fn = { fni : i >= 0 } on A.
• I.e. fni(aj) is some ak for every aj.
– A set of predicates Pr = { pri : i >= 0 } over A.
• Do not have to be total.
• Can have many arities.
ISA 780/SWE 623Classical
Logic
Duminda Wijesekera
26
Interpreting Syntax
• Mapping from Syntax to Semantics:
– A mapping mCons : { ci : I >= 0 } to A={ai: i >= 0}.
• Need not be ONTO A. I.e. there could be unnamed individuals in the
semantic domain.
– A mapping mFun : { fi : I >= 0 } to Fn={fni: i >= 0}.
• Need not be onto. I.e. there could be unnamed functions in the
semantic domain.
– A mapping mPred: { pi : I >= 0 } to Pr={pri: i >= 0}.
• Need not be onto. I.e. there could be unnamed predicates in the
semantic domain.
ISA 780/SWE 623Classical
Logic
Duminda Wijesekera
27
Interpreting Formulas: naming
• We do not interpret formulas with free variables.
• In order to interpret quantified formulas, need to
expand the syntax by adding a constant in the syntax
for each unnamed individual in the model.
– I.e. for each ai for which there is no cj such that Fn(cj ) is ai,
add a new constant Cai to the syntax.
– Now expand the definition of terms to include these new
constants. Let newT = { Nti : i >= 0} be the collection of
new terms so defined.
ISA 780/SWE 623Classical
Logic
Duminda Wijesekera
28
Interpreting Formulas
• Let M be a model. We define M ╞ F for every
quantified formula as follows.
– For every n-ary predicate symbol pi , and every
sequence of new variable free terms Nt1, … Ntn
define M ╞ pi(Nt1, … Ntn ) if and only if
mPred(pi)(Nt1, … Ntn ).
– I.e. pi(Nt1, … Ntn ) is true in M if and only if its
image under the map mPred holds with parameters
Nt1, … Ntn .
ISA 780/SWE 623Classical
Logic
Duminda Wijesekera
29
Interpreting Formulas: Continued
– For every formula A , M ╞ y A(y) if and only if M
╞ A(Nti) for every Nti e newT.
– For every formula A , M ╞  y A(y) if and only if
there is some Nti e newT satisfying M ╞ A(Nti).
– M ╞ A ^ B if M ╞ A and M ╞ B .
– M ╞ A v B if M ╞ A or M ╞ B.
– M ╞ A => B if when M ╞ A then M ╞ B.
– M ╞  A if it is not the case that M ╞ A.
ISA 780/SWE 623Classical
Logic
Duminda Wijesekera
30
Proof Rules for Predicate Logic
• Proof rules of introduction and elimination
of ^, v, =>, and .
• New rules required for introduction and
elimination of  and  quantifiers.
ISA 780/SWE 623Classical
Logic
Duminda Wijesekera
31
Proof Rules for 
•  Introduction
A(x)
x A(x)
provided x is not free in the
assumptions of A
•  Elimination
x A(x)
A[t/x]
ISA 780/SWE 623Classical
Logic
Duminda Wijesekera
32
Proof Rules for 
•  Introduction
A[t/x]
xA(x)
•  Elimination
[A]
B
xA(x)
B
ISA 780/SWE 623Classical
Logic
provided x is not free
in B nor in the
assumptions of B
apart from A
Duminda Wijesekera
33
An Example Proof
• Prove ((x A(x)) ^ B) => (x (A(x)^ B))
provided that x is not free in B.
• Plan:
– Since outer connective is =>, need to use =>
introduction at the last step. Hence can use
(x A(x)) ^ B as an assumption for the steps above.
– Now in order to get x (A(x)^ B) using 
introduction, we need to get A[t/x] )^ B.
– Can use ^ elimination to (x A(x)) ^ B and obtain B
– Can use x elimination to get A[t/x].
ISA 780/SWE 623Classical
Logic
Duminda Wijesekera
34
Example Proof
x A(x) ^ B
x A(x)
[A(t/x)]
A(t/x) ^ B
x(A(x) ^ B
x A(x) ^ B
B
• The other direction of the proof appears in the handout
page 32.
ISA 780/SWE 623Classical
Logic
Duminda Wijesekera
35
Induction Rule
A[0/x]
[A(x)]
A[x+1/x]
A(x)
Proviso: x is not free in the assumptions of
A[x+1/x] apart from A(x).
ISA 780/SWE 623Classical
Logic
Duminda Wijesekera
36
Equality Reasoning
• Rules for equality
– Reflexivity axiom: t = t.
– Symmetry rule:
t= u.
u=t
– Transitivity rule: s = t
t=u.
s=u
• Congruence laws for each function and
predicate symbol, or substitution rules.
ISA 780/SWE 623Classical
Logic
Duminda Wijesekera
37
Equality Reasoning: Continued
• Congruence Law for functions:
t1 = u1 …. tn = un
f(t1, …., tn) = f(u1, ….,un)
• Congruence Law for Predicates:
t1 = u1 …. tn = un
p(t1, …., tn)  p(u1, ….,un)
• Substitution Rule:
t = u
S[t/x] = S[u/x]
ISA 780/SWE 623Classical
Logic
Duminda Wijesekera
38
Equality Reasoning: An Example
x f(x,x) = x
f(g(z), g(z)) = g(z)
p(f(g(z), g(z))  p(g(z))
 p(f(g(z), g(z))   p(g(z))
ISA 780/SWE 623Classical
Logic
Duminda Wijesekera
39
Many Sorted Logic
• Sorts can be introduced to first-order logic
– So what we learned is single-sorted first orderlogic
• x: Integer [ y: Real divides(x,y) ]
– Integer and Real are two different sorts.
• x,y: Point  z: Line [x ≠ y => isOn(x,y,z)]
– Point and Line are sorts
ISA 780/SWE 623Classical
Logic
Duminda Wijesekera
40
Translating many sorted Logic to
one-sorted logic
• Create a one-ary predicate for each sort and write
the statement as an implication.
• Many sorted:
– x: Integer [ y: Real divides(x,y) ]
• One Sorted:
– x y[isInteger(x) ^ isReal(y)=>divides(x,y)]
• x,y: Point  z: Line [x ≠ y => isOn(x,y,z)]
– x,y  z[ isPoint(x) ^isPoint(y) ^ x ≠ y => isLine(z)
isOn(x,y,z)]
ISA 780/SWE 623Classical
Logic
Duminda Wijesekera
41
Notations from Z
.
• In Z x f(x) is written as x f(x)
• Sometimes types are also used right after the
quantifier, for example:
• x :opera · isComposer(Beethovan,x)
.
• x: Integer · [ y: Real devides(x,y) ]
ISA 780/SWE 623Classical
Logic
Duminda Wijesekera
42
Typed Logics
• Sorts are expected to be disjoint sets
• That implies:
– Integers are NOT a subset of Real Numbers
• Introducing types are more complicated
– Requires that there be type constructors.
• Example: Integer  Real
– Ordered pairs, say ORD
• Example
– x: ORD,  z: Integer  z: Real x=(y,z)
– Here ( , ) is a type constructor.
ISA 780/SWE 623Classical
Logic
Duminda Wijesekera
43
Why is this an Issue?
•
•
•
•
•
How to prove: (x,y) = (a,b) iff x=a and y=b
Similar problems occur with sets, lists etc.
What is the problem?
The equality theory has to be built.
Sets create more problems:
– Set quantifiers are problematic
– Leads to FULL second order logic
• No complete Σ1 proof theory
ISA 780/SWE 623Classical
Logic
Duminda Wijesekera
44
Using Logic As a Programming
Language
• Prolog
• Datalog
• Basic Idea: Use them as Rules
– Can specify search
• Raises many issues with semantics
ISA 780/SWE 623Classical
Logic
Duminda Wijesekera
45
What Other Forms of Logics are
there?
• Can enrich 1st Order Logic by introducing
more connectives
• Example: Modal Logic:
– Adding two new constructors to reason about
possibility and nasality
– ◊ and 
– Syntax: If f is a formula so are ◊ f and f
ISA 780/SWE 623Classical
Logic
Duminda Wijesekera
46
Applications of Modal Logic
•
•
•
•
•
•
Dynamic Logic
Temporal Logics
Theories of Motion
Theories of Change
Theories of Knowledge
Applications in security
– Access control
– Delegation
• See separate transparency on Modal, Dynamic and
Temporal Logics
ISA 780/SWE 623Classical
Logic
Duminda Wijesekera
47
Other Forms to Enhance
1st Order Logic
• Add Richer Quantifier Structures:
– Quantify over subsets of structures and/or
relation symbols
– Add quantifiers such as there exists infinitely
many, or for infinitely many.
• Example:
– x  y factors(x,y)
–  y prime(y)
ISA 780/SWE 623Classical
Logic
Duminda Wijesekera
48
Apply existing connectives many
more times – infinitary logics
• If f1, … fn, .. are formulas so are
– ^ {i=1}  fi
– v {i=1}  fi
• Different from having infinitary quantifiers
ISA 780/SWE 623Classical
Logic
Duminda Wijesekera
49
Restrictions based on Semantics
• Can specify the size of models
• Infinitary but large models
– Such as only those beyond a given cardinal ‫א‬1
• Finite model theory
– Many applications in computer science
– Quantifiers take an entirely different meaning
ISA 780/SWE 623Classical
Logic
Duminda Wijesekera
50
Those that reject basic assumptions
of Classical Logic
• Intuitionism
• Why is (A → B) v (B → A) a tautology ?
– Pigenhole principle in classical truth values
• Similar argument for (A1 → A2) v (A2 → A3) …. (An →
An+1) v (An+1 → A1)
• Consequence: P v  P does not have to be true!
• Infinitely many truth values
• Leads to Kripke Semantics with worlds with
increasing truth values
• Used in the semantics of programming languages
and type theories
ISA 780/SWE 623Classical
Logic
Duminda Wijesekera
51