Logic (PHIL 2080, COMP 2620, COMP 6262) Chapter: Introduction to Logic
Logic (PHIL 2080, COMP 2620, COMP 6262)
Chapter: Introduction to Logic
Pascal Bercher
Planning & Optimization
Yoshihiro Maruyama
Logic
Intelligent Agents
College of Engineering and Computer Science
the Australian National University (ANU)
23 & 25 February 2021
Organizational Matters Introduction to Logic Sequents Propositional Calculus Summary
Organizational Matters
Pascal Bercher and Yoshihiro Maruyama 1.34
Organizational Matters Introduction to Logic Sequents Propositional Calculus Summary
Team: The Lecturers, 1/3
Prof. Dr. John Slaney (2011 – 2020, now retired)
http://users.cecs.anu.edu.au/~jks/
We inherited his course; he produced:
Course structure and content
Most exercises (also for exams)
The Logic for Fun (L4F) platform
The online course notes
The plagiarism scanner
Pascal Bercher and Yoshihiro Maruyama 2.34
Organizational Matters Introduction to Logic Sequents Propositional Calculus Summary
Team: The Lecturers, 2/3
Dr. Pascal Bercher since 2021
https://cecs.anu.edu.au/people/pascal-bercher
Studies: Computer Science (with minor Cognitive Science)
PhD: Computer Science: Hierarchical Planning
Research:
• Hierarchical Task Network (HTN) Planning
• Heuristic Search
• Complexity Theory
→ Pascal will teach the first 50% of the course
Pascal Bercher and Yoshihiro Maruyama 3.34
http://users.cecs.anu.edu.au/~jks/
https://cecs.anu.edu.au/people/pascal-bercher
Organizational Matters Introduction to Logic Sequents Propositional Calculus Summary
Team: The Lecturers, 3/3
Dr. Yoshihiro Maruyama since 2021
https://cs.anu.edu.au/people/yoshihiro-maruyama
Studies: Mathematics, Philosophy, Computer Science
PhD: Computer Science: Category-theoretical Logic
Research: Mathematical and Philosophical Logic:
• category-theoretical logic
• categorical foundations of mathematics, CS, AI, physics
• philosophy of logic, mathematics, AI, science in general
→ Yoshi will teach the second 50% of the course
Pascal Bercher and Yoshihiro Maruyama 4.34
Organizational Matters Introduction to Logic Sequents Propositional Calculus Summary
Team: The Tutors
See Wattle for the complete list and contact info.
What do they do?
• Give the tutorials/workshops
• Answer your questions (via Wattle forum)
• (Co-)Mark the homework, assignments, and exam
Pascal Bercher and Yoshihiro Maruyama 5.34
Organizational Matters Introduction to Logic Sequents Propositional Calculus Summary
Various: Appointments/Dates
Lectures:
• Online live, recordings available via Wattle/Echo360
• 2 per week, (approx.) 50 minutes each, see Wattle for dates
Workshops/tutorials:
• Only online via Zoom: please activate video and bring a headset
• Once per week, 120 minutes each, see Wattle for dates
• We’ll do both tutorial-like “standard” exercises as well as
workshop-like modeling tasks
Appointments:
• Only in exceptional cases. If required ask for appointment via mail
• Otherwise ask all questions via the forum or your tutor
Pascal Bercher and Yoshihiro Maruyama 6.34
Organizational Matters Introduction to Logic Sequents Propositional Calculus Summary
Various: Exercises and Exam
Homework every two weeks:
• Standard exercises (do proofs) or modeling tasks
• Get corrected by tutors, marks are just FYI, they do not count
towards the exam/course mark
• Collaboration (up to 3 people) is strongly encouraged, but please
don’t hand in the same results several times
Three Assignments:
• 1 related to formal proofs, 1 via Logic for Fun (L4F) and 1 essay
• Each assignment counts 15% of the final mark
• Any form of cheating will be escalated and has serious
consequences
• Deadlines: Are strict, no exceptions (unless you have a serious
reason, backed up by medical certificates, for example)
Exam
• Will be online, 3 hours
• Counts 55% of final mark
Pascal Bercher and Yoshihiro Maruyama 7.34
https://cs.anu.edu.au/people/yoshihiro-maruyama
Organizational Matters Introduction to Logic Sequents Propositional Calculus Summary
Various: Course Material
Slides (see Wattle)
Online book “Logic Notes” (http://users.cecs.anu.edu.
au/~jks/LogicNotes/index.html)
Our modeling tool “Logic for Fun (L4F)”
(https://l4f.cecs.anu.edu.au/)
Online forum! (Set Wattle reminders accordingly!)
For further reading, see books:
• G. Restall. Logic: An Introduction. Ed. by J. Shand. Routledge,
2005 (Well-suited for Philosophy students)
• D. van Dalen. Logic and Structure. Springer, 2012 (Well-suited for
Computer Science and Mathematics students)
Pascal Bercher and Yoshihiro Maruyama 8.34
Organizational Matters Introduction to Logic Sequents Propositional Calculus Summary
Various: Feedback/Corrections
Nobody is perfect!
Did you find an error in the slides? (Even just a typeo!)
Do you have an idea on how to improve the slides?
• More content? Less content?
• Adding a specific example?
• Adding a specific explanation?
• Explaining a specific error many make?
→ Let us know! Drop us/the respective lecturer an email!
Pascal Bercher and Yoshihiro Maruyama 9.34
Organizational Matters Introduction to Logic Sequents Propositional Calculus Summary
Introduction to Logic
Pascal Bercher and Yoshihiro Maruyama 10.34
Organizational Matters Introduction to Logic Sequents Propositional Calculus Summary
Motivation: Motivations
See presentation by Yoshi!
Pascal Bercher and Yoshihiro Maruyama 11.34
http://users.cecs.anu.edu.au/~jks/LogicNotes/index.html
http://users.cecs.anu.edu.au/~jks/LogicNotes/index.html
https://l4f.cecs.anu.edu.au/
Organizational Matters Introduction to Logic Sequents Propositional Calculus Summary
Introduction: What is Logic?
Logic is a mathematical discipline, and the basis of many related
fields, most notably computer science.
Logic is the Science of Reasoning:
• Good/correct reasoning vs. bad/wrong reasoning
• Making (and reasoning about) valid arguments
⇒ See Monty Python sketch “argument clinic”
(e.g., https://www.dailymotion.com/video/x2hwqn9)
Pascal Bercher and Yoshihiro Maruyama 12.34
Organizational Matters Introduction to Logic Sequents Propositional Calculus Summary
Introduction: What’s an Argument?
Example:
All footballers are bipeds
Socrates it a footballer
}
premises
Thus, Socrates is a biped
}
conclusion
→ This is a valid argument
Arguments consist of premises and a conclusion.
Pascal Bercher and Yoshihiro Maruyama 13.34
Organizational Matters Introduction to Logic Sequents Propositional Calculus Summary
Introduction: What’s an Argument?
Another Example:
All cats are insects
Snoopy is a cat
premises
Thus, Snoopy is an insect
}
conclusion
→ This is also a valid argument!
• Although everything was wrong!
• All premises and the conclusion!
→ But we don’t care, since it has a valid form. We exploit this form,
and abstract from the content to reason about the conclusions.
Pascal Bercher and Yoshihiro Maruyama 14.34
Organizational Matters Introduction to Logic Sequents Propositional Calculus Summary
Introduction: What’s an Argument?
Our final Example:
All logicians are rational
Restall1 is rational
}
premises
Thus, Restall is a logician
}
conclusion
→ Interestingly, this is an invalid (wrong!) argument!
• Although everything was right!
• All premises and the conclusion!
→ Wrong form: The conclusion did not follow from the premises.
1Greg Restall, professor of logic at the University of Melbourne, author of the
best-known book on substructural logic and editor in chief of the Australasian Journal
of Logic, is presumably a logician if anyone is.
Pascal Bercher and Yoshihiro Maruyama 15.34
Organizational Matters Introduction to Logic Sequents Propositional Calculus Summary
Introduction: Forms of Arguments
Valid arguments have, e.g., the following form:
All As are Bs;
x is an A;
Therefore, x is a B.
The example with Restall did not work because it used a wrong form:
All As are Bs;
x is an B;
Therefore, x is an A.
Pascal Bercher and Yoshihiro Maruyama 16.34
Organizational Matters Introduction to Logic Sequents Propositional Calculus Summary
Introduction: Valid Arguments
An argument is considered valid, when ever the conclusion
logically follows from the premises.
“Logically follows” abstracts away from the number of
“intermediate steps” that are required so that the conclusion
becomes “obvious”.
For example, if we take all axioms of some mathematical system
as the premises and one of it’s (valid) theorems/propositions as
its conclusion, this forms a valid argument – no matter how
ingenious the theorem is!
Thus, showing that an argument is actually valid is hard!
We will break down arguments into a sequence of arguments, so
that every conclusion “follows in one step” from its premises.
This will be done via natural deduction (next chapter and couple
of weeks!), based on sequents, which represent arguments.
Pascal Bercher and Yoshihiro Maruyama 17.34
Organizational Matters Introduction to Logic Sequents Propositional Calculus Summary
Sequents
Pascal Bercher and Yoshihiro Maruyama 18.34
Organizational Matters Introduction to Logic Sequents Propositional Calculus Summary
Introduction to Sequents
Our convention:
Letters from the end of the alphabet: set
. . . beginning . . . : single object of the
kind that’s in the set
This represents sequent: X : A
X is a set of formulae
A is a single formula
This represents a “good” sequent: X ` A
Read it: A follows (logically) from X (later we will learn that it
actually means that A can be derived from X )
For example, “the query A follows from the data X ”
Pascal Bercher and Yoshihiro Maruyama 19.34
Organizational Matters Introduction to Logic Sequents Propositional Calculus Summary
Definition of Sequents
Since ` behaves like a relation (we are only allowed to write X ` A
under certain circumstances, cf. last slide), we can also ask which
properties the ` “relation” has that we consider (for propositional
natural deduction).
It satisfies the following properties:
If A is in X , then X ` A (reflexivity)
If X ` A, then X ∪ Y ` A for all Y (monotonicity)
If X ` A and Y ,A ` B, then X ,Y ` B (transitivity)
• X ,A ` B is short for X ∪ {A} ` B and (also called cut)
• X ,Y ` A is short for X ∪ Y ` A
When these criteria hold, we also say it’s a consequence relation.
Pascal Bercher and Yoshihiro Maruyama 20.34
Organizational Matters Introduction to Logic Sequents Propositional Calculus Summary
The Purpose of Sequents
Sequent are used to express valid arguments! (This will be
formally covered in week 4.)
Recall that an argument (in the sense of logic) is valid even if the
“step” from the premises to the conclusion is far from obvious.
To “prove” that a sequent is valid we will derive a sequence of
sequents, by only “slightly” manipulating the involved formulae.
More details will be given later when we study natural deduction.
Pascal Bercher and Yoshihiro Maruyama 21.34
Organizational Matters Introduction to Logic Sequents Propositional Calculus Summary
Propositional Calculus
Pascal Bercher and Yoshihiro Maruyama 22.34
Organizational Matters Introduction to Logic Sequents Propositional Calculus Summary
Introduction
Logic is about making statements:
(natural language) sentence︷ ︸︸ ︷
Socrates︸ ︷︷ ︸
constant
is a goat︸ ︷︷ ︸
predicate
What’s a predicate?
It will formally be defined later, when we deal with predicate logics
A predicate relates various objects (constants) to each other, e.g.:
• isGoat(Socrates) or isGoat(Goat)
• isFootballer(Socrates)
• Kicks(Socrates,Goat) or Kicks(Socrates,Ball)
Actually, predicates do not exist in propositional logics, where we
have propositions instead, e.g.,
• SocratesIsGoat or GoatIsGoat
• SocratesIsFootballer
• SocratesKicksGoat or SocratesKicksBall
→ Since this is way too long, we usually just write p, q, r , etc.
Pascal Bercher and Yoshihiro Maruyama 23.34
Organizational Matters Introduction to Logic Sequents Propositional Calculus Summary
Basic Definitions: Terminology
Atoms refer to any “atomic” truth statement:
true (denoted by >, T , or 1)
false (denoted by ⊥, F , or 0)
any propositional symbol (denoted by p, q, r , . . . )
What’s missing for non-atomic statements? Connectives!
Socrates is a goat, …
• because …
• although …
• until …
• and …
• or …
It is not true that …
• Socrates is a goat
• …
Pascal Bercher and Yoshihiro Maruyama 24.34
Organizational Matters Introduction to Logic Sequents Propositional Calculus Summary
Basic Definitions: Syntax of Connectives
Which connectives do exist in propositional logic?
… and …: ∧ e.g., (p ∧ >) or (p ∧ (q ∧ r))
… or …: ∨ e.g., (⊥ ∨>) or (p ∨ (q ∧ r))
if …, then …: → e.g., (p → q) or ((p ∧ q)→ (p ∨ q))
also: … implies …
… if and only if …: ↔ e.g., (p ↔ q) or ((p ∧ q)↔ (q ∧ p))
not …: ¬ e.g., ((¬p)→ q) or ¬(p → q)
Pascal Bercher and Yoshihiro Maruyama 25.34
Organizational Matters Introduction to Logic Sequents Propositional Calculus Summary
Basic Definitions: Semantics of Connectives
What do these connectives mean?
The semantics will be covered formally in a later section, so this
is just a “teaser” for some of the connectives.
Our connectives act like functions, assigning any input pattern a
new output (just like logical gates in “technical computer science”
/ “computer architecture”).
Examples:
• (¬p) inverts p’s truth value: > is switched to ⊥, and vice versa.
• (p ∧ q) is true if and only if both p and q are true.
• (p ∨ q) is true if and only if at least one of p and q are true.
Pascal Bercher and Yoshihiro Maruyama 26.34
Organizational Matters Introduction to Logic Sequents Propositional Calculus Summary
Basic Definitions: Semantics of Connectives
What do these connectives mean?
The semantics will be covered formally in a later section, so this
is just a “teaser” for some of the connectives.
Our connectives act like functions, assigning any input pattern a
new output (just like logical gates in “technical computer science”
/ “computer architecture”).
Examples: (expressed as truth tables)
p ¬
⊥ >
> ⊥
p q ∧
⊥ ⊥ ⊥
⊥ > ⊥
> ⊥ ⊥
> > >
p q ∨
⊥ ⊥ ⊥
⊥ > >
> ⊥ >
> > >
Pascal Bercher and Yoshihiro Maruyama 26.34
Organizational Matters Introduction to Logic Sequents Propositional Calculus Summary
Basic Definitions: Semantics of Connectives
What do these connectives mean?
The semantics will be covered formally in a later section, so this
is just a “teaser” for some of the connectives.
Our connectives act like functions, assigning any input pattern a
new output (just like logical gates in “technical computer science”
/ “computer architecture”).
Examples: (expressed as truth tables)
p ¬
0 1
1 0
p q ∧
0 0 0
0 1 0
1 0 0
1 1 1
p q ∨
0 0 0
0 1 1
1 0 1
1 1 1
Pascal Bercher and Yoshihiro Maruyama 26.34
Organizational Matters Introduction to Logic Sequents Propositional Calculus Summary
Basic Definitions: Semantics of Connectives in Natural Language
Note that natural language does not always translate 1-to-1 to logics:
“Jane and Jill went up the hill”:
says more than just WentUpHill(Jane) ∧WentUpHill(Jill),
because it means that they went there together.
“One false move and I will shoot!”
Does not mean Move(You) ∧ Shoot(I), but
Move(You)→ Shoot(I)
Funnily, “Don’t move or I shoot”:
Is not meant to mean ¬Move(You) ∨ Shoot(I), but also means
Move(You)→ Shoot(I), but both are equivalent.
Modeling “the real world” (based on natural language) is not easy,
and partially covered in some exercises of Logic For Fun.
Pascal Bercher and Yoshihiro Maruyama 27.34
Organizational Matters Introduction to Logic Sequents Propositional Calculus Summary
Basic Definitions: Precedence of Connectives (Syntax Simplification)
Our connectives use some precedence, which we exploit to eliminate
parentheses! Connectives, ordered by precedence:
Highest: ¬ e.g., ¬p → q ≡ (¬p)→ q
Second-highest: ∧ e.g., p ∧ q ∨ r ≡ (p ∧ q) ∨ r
Mid: ∨ e.g., p → q ∨ r ≡ p → (q ∨ r)
Second-Lowest: → e.g., p → ¬q ↔ r ≡ (p → (¬q))↔ r
Lowest: ↔ e.g., ¬p ∨ q ↔ q ∧ r ≡ ((¬p) ∨ q)↔ (q ∧ r)
We reduce parenthesis to simplify and avoid confusion by exploiting:
precedence, e.g., we write (p∧¬q∧ r)→ (p∨¬q∨ r) instead of
(((p ∧ (¬q)) ∧ r)→ (p ∨ ((¬q) ∨ r))), and
associativity, e.g., we write p ∧ q ∧ r instead of (p ∧ (q ∧ r))
Pascal Bercher and Yoshihiro Maruyama 28.34
Organizational Matters Introduction to Logic Sequents Propositional Calculus Summary
Connective Scopes and Main Connective: Connective Scopes
Every connective has a scope.
“[The scope of a connective] is defined to be the shortest formula
or subformula in which that occurrence lies.” (Logic Notes)
Examples: In the formula ¬(p ∧ q)→ ((p ∨ r)→ ¬s)
• … the scope of its first ¬ is (p ∧ q)
• … the scope of its second ¬ is s
Pascal Bercher and Yoshihiro Maruyama 29.34
Organizational Matters Introduction to Logic Sequents Propositional Calculus Summary
Connective Scopes and Main Connective: Main Connective
Every formula has a main connective:
“[T]he main connective of any formula […] is the one which is not
inside the scope of any other. […] The scope of the main
connective is the whole formula.” (Logic Notes)
Examples: The main connective of . . .
• ¬(p ∧ q)→ ((p ∨ r)→ ¬s) is: the first→
• (p ∧ q) ∨ r is: ∨
• What’s the main connective of (p ∧ q) ∨ r ∨ (q → r)?
Recall that “(p ∧ q) ∨ r ∨ (q → r)” is only syntactic sugar!
I It was either ((p ∧ q) ∨ r) ∨ (q → r) [then, it’s the right ∨],
I or it was (p ∧ q) ∨ (r ∨ (q → r)) [then, it’s the left ∨]
Why is it important to identify the main connective?
Because we will manipulate sequents based on their main
connective!
Pascal Bercher and Yoshihiro Maruyama 30.34
Organizational Matters Introduction to Logic Sequents Propositional Calculus Summary
Connective Scopes and Main Connective: Type of Formula
The main connective dictates the type of a formula:
if main connective is ¬, formula is a negation
… ∧, … conjunction
… ∨, … disjunction
… →, … implication
… ↔, … double-implication
Pascal Bercher and Yoshihiro Maruyama 31.34
Organizational Matters Introduction to Logic Sequents Propositional Calculus Summary
Substitution: Substitutions of Formulae
What is a substitution?
“Formula A is a substitution instance of formula B if and only if A
results from B by substitution of formulas for sentence letters.”
(Logic Notes) – (Definition is specific to propositional logic.)
Example:
“Original” formula: q ∨ p
One of its substitution instances is (p ∧ q) ∨ ¬r , because:
• q got substituted by (p ∧ q)
• p got substituted by ¬r
Pascal Bercher and Yoshihiro Maruyama 32.34
Organizational Matters Introduction to Logic Sequents Propositional Calculus Summary
Substitution: Substitutions of Formulae
What is a substitution?
“Formula A is a substitution instance of formula B if and only if A
results from B by substitution of formulas for sentence letters.”
(Logic Notes) – (Definition is specific to propositional logic.)
Non-Example:
“Original” formula: q ∨ q
The formula (p ∧ q) ∨ ¬r is not a substitution instance of it
(because the left part had to be the same as the right)
Pascal Bercher and Yoshihiro Maruyama 32.34
Organizational Matters Introduction to Logic Sequents Propositional Calculus Summary
Summary
Pascal Bercher and Yoshihiro Maruyama 33.34
Organizational Matters Introduction to Logic Sequents Propositional Calculus Summary
Content of this Lecture
Organizational Matters
Sequents, as a way to express valid arguments
Introduction to Propositional Logic
• Its syntax and (a preview to) its semantics
• What connectives exist (and which don’t)
• How to identify the type of a formula (e.g., negation, conjunction,
disjunction, implication, double-implication)
• What’s a substitution
→ The entire Logic Notes section “Introduction”
Pascal Bercher and Yoshihiro Maruyama 34.34
Organizational Matters
Team
Various
Introduction to Logic
Motivation
Introduction
Sequents
Propositional Calculus
Introduction
Basic Definitions
Connective Scopes and Main Connective
Substitution
Summary