Logic I

Alternative textbook exercises (regular): 2.8, 2.10, 2.12, 2.21

Alternative textbook exercises (fast): 2.8, 2.10, 2.12, 2.21

Soundness (041)

definitions

Explains the notion of a sound argument.

Introduces the notion of identity used in studying first-order logic. Includes example argument and the two principles. Also demonstrates how to assign names in zoxiy, and using zoxiy to make identity statements true and false.

Reading: §2.2

Alternative textbook exercises (regular): 2.5, 2.6

Formalizing Arguments (135)

translation

Illustrates how for formalise simple arguments with the 'pigs' illustration.

Reading: §3.7

Sentence Letters (012)

definitions

Explains what sentence letters are and why we use them.

Truth Tables (071)

definitions

Introduces truth tables for conjunction, disjunction and negation. Truth tables give the meanings of connectives in our formal language awFOL.

Reading: §3.1, §3.2, §3.3

Alternative textbook exercises (regular): 3.1, 3.2, 3.5, 3.7

Alternative textbook exercises (fast): 3.1, 3.3, 3.5, 3.7

Complex Truth Tables (60)

truth-tables

Illustrates how to construct complex truth tables with an example, not(P and Q).

Contradictions, Logical Truths and Logical Possibilities (065)

definitions zoxiy ex-tt

Illustrates and defines the terms ‘contradiction’, ‘logical truth’ and ‘logical possibility’. Describes how to recognise these from truth tables. Demonstrates using zoxiy to construct truth-tables and answer questions about contradictions, logical truths and logical possibilities.

Reading: §2.2

Alternative textbook exercises (regular): 2.5, 2.6

Lecture 03

Date given: Tuesday 19th January 2016

Exercises for this lecture:

Logical Validity and Truth Tables (14)

truth-tables

Illustrates the use of truth tables to determine logical validity.

Reading: §4.3

Alternative textbook exercises (regular): 5.1-5.4

Formal Proof (211)

proof

Marks the transition from truth-tables, in which the notion of truth plays a central role, to fitch proofs which are purely formal entities.

Translating a Simple Argument (213)

translation

Illustrates how to translate an argument from English into our formal language awFOL.

Reading: §3.2

Formal Proof: ∧Elim and ∧Intro (21)

proof zoxiy ex-proof

Introduces and illustrates the use of rules of proof for conjunction. Explains how to create proofs using logic-ex.

Reading: §5.1, §6.1

Alternative textbook exercises (regular): 6.1

Alternative textbook exercises (fast): 5.3--5.6

Symbols and Words (022)

proof zoxiy ex-proof ex-trans

When you use zoxiy you can type words instead of using symbols. But which words stand for which symbols? Here’s a list.

Truth Tables Are Stipulations (073)

truth-tables semantics

Sometimes people think that one or other of the truth tables for a connective is wrong. These thoughts are always mistaken. The truth tables for the connectives are stipulations about their meanings.

Rules of Proof for Identity (110)

proof

Introduces and illustrates the rules of proof for identity, =Intro and =Elim.

Reading: §2.2

How to Write Proofs (130)

definitions

Describes how to write proofs.

Complex Truth Tables (09)

truth-tables

Illustrates how to construct complex truth-tables with an example, the truth-table for (P and Q) or R. Also describes how to order the reference columns.

Reading: §3.3, §3.5

Alternative textbook exercises (regular): 3.12, 3.13, 4.4-4.7, 4.12-14

Alternative textbook exercises (fast): 3.14, 3.15

Logic Makes Me Die Inside (161)

definition

Is the definition of logical validity flawed?

Reading: §2.1

Contradictions, Logical Truths and Logical Validity (160)

truth-tables

Continues exploring the use of truth-tables to establish whether sentences are contradictions or logical truths, and to demonstrate logical validity. Notes that logical validity is not what you think it is.

Reading: §4.1, §4.2, §5.4

Alternative textbook exercises (regular): 4.1, 4.2

Alternative textbook exercises (fast): 4.1, 4.2, 4.12--4.16

Lecture 04

Date given: Thursday 21st January 2016

Exercises for this lecture:

∨Intro (225)

proof

Introduces the rule of proof ∨Intro with some examples.

∧Intro and ∨Intro: Compare and Contrast (212)

proof

Contrasts two rules of proof and explores how their differences are related to truth-tables.

Reading: §6.1

Truth-functional Connectives (072)

truth-tables semantics

Explains the notion of a truth-functional connective. Discussion of why 'because' could not have a truth table.

Reading: §7.0 (the text before §7.1)

Alternative textbook exercises (regular): 7.9

Alternative textbook exercises (fast): 7.9

The Storm Clouds on the Horizon Were Getting Nearly Directly Overhead (162)

truth-tables

Illustrates and defines the terms 'tautology' and 'contradiction' with some quotes from George Bush.

A ∧ B ∨ C (151)

proof syntax

Distinguishes lexical from structural ambiguity. Asks how we can know there is no structural ambiguity in our formal language awFOL.

Reading: §3.5

Alternative textbook exercises (regular): 3.20, 3.21, 3.22

A ∧ B ∨ C: the Truth-tables (153)

truth-tables

Illustrates how to construct complex truth tables for (A ∧ B) ∨ C and A ∧ (B ∨ C).

A ∧ B ∨ C: They Are Different (154)

truth-tables

Uses two arguments to show that (A ∧ B) ∨ C and A ∧ (B ∨ C) really are different.

Alternative textbook exercises (regular): 3.14, 3.15

Alternative textbook exercises (fast): 3.14, 3.15, 7.2, 7.5, 7.6

Lecture 05

Date given: Tuesday 26th January 2016

Exercises for this lecture:

¬, ⊥ (270)

proof

Quick introduction to two connectives, ¬ and ⊥, together with illustration of rules of proof for ⊥.

Reading: §6.3

→Intro, →Elim (390)

proof proof-example

Introduction to the rules of proof for →, →Intro and →Elim. This is the first time subproofs are used. Also illustrates a proof without any premises. The proof is from premises P→Q and Q→R to conclusion P→R.

Reading: §8.1, §8.2

Alternative textbook exercises (fast): 8.20--8.25

Subproofs with zoxiy (395)

proof proof-example zoxiy ex-proof

Reading: §8.1, §8.2

Ambiguity: Recap (170)

syntax

What is the source of ambiguity in natural languages?

I Shot an Elephant in My Pyjamas (171)

syntax

What is the source of ambiguity in natural languages? Depicts two structures for Groucho Marx' utterance 'I shot an elephant in my pyjamas'.

Lecture 06

Date given: Thursday 28th January 2016

Exercises for this lecture:

∨Intro and ∨Elim (222)

proof

States the rules of proof for ∨, ∨Intro and ∨Elim.

Reading: §6.2

∨Elim and Soundness (226)

proof

Introduces the rule of proof ∨Elim and links it to the truth table for ∨.

Reading: §5.2, §6.2

∨Elim: An Example (221)

proof proof-example

Illustrates the use of ∨Elim, a rule of proof. Uses the inference from A∨B to B∨A as an example.

Reading: §5.2, §6.2

Alternative textbook exercises (regular): 5.1--5.6, 6.2--6.6

Not Or (603)

translation

Negating disjunctions is tricky. This contrasts ¬(A ∨ B) with ¬A ∨ ¬B.

Reading: §3.7

Alternative textbook exercises (regular): 3.19, 5.18

→Intro: An Example (391)

proof proof-example

Discusses (but does not complete) a relatively hard proof involving the rule →Intro. The proof is from premise A∨B to conclusion ¬B→A.

¬Elim (280)

proof

Introduces the rule of proof ¬Elim with an illustration. Relates the rule to the truth table for ¬.

Reading: §6.3

¬Intro (281)

proof proof-example

Introduction to the rule of proof ¬Intro with an illustration. Discusses the proof from premise A∧B to conclusion ¬(¬A∨¬B).

Reading: §5.3, §6.3

Alternative textbook exercises (regular): 6.7--6.10, *6.11--6.12

Alternative textbook exercises (fast): 6.7--6.12, 6.18--6.20, 6.24--6.27, *6.40--6.42

¬Intro continued (282)

proof

Completes the proof used to illustrate ¬Intro.

∨Elim: Recap (223)

proof

Repeats an earlier illustration of the use of ∨Elim, a rule of proof. Uses the inference from A∨B to B∨A.

Subproofs Are Tricky (224)

proof

Offers what appears to be a proof of an argument that is not logically valid in order to illustrate a restriction on the use of subproofs.

Lecture 07

Date given: Tuesday 2nd February 2016

Exercises for this lecture:

Recap: Structural Ambiguity in Natural Languages (231)

syntax

Reminder about the sources of structural ambiguity in natural language.

The Syntax of awFOL (230)

syntax

States the rules of syntax for awFOL. Illustrates these with tree diagrams. Links to truth tables.

Reading: §9.3

¬P ∨ ¬Q compared with ¬(P ∨ Q) (232)

syntax

Explains how the brackets make a different to the meanings of sentences. Illustrates by comparing ¬P ∨ ¬Q with ¬(P ∨ Q).

Reading: §3.5

Logically Entails (239)

definitions

One sentence logically entails another just if there’s no possible situation where the first is true and the second false.

Subproofs Are Tricky: The Answer (227)

proof

Explains that in doing a proof, it is not allowed to cite lines from a closed subproof, thereby answering a question asked earlier.

¬Intro Proof Example (283)

proof proof-example

Discusses an intermediate proof involving ¬Intro, from premises P→Q and ¬Q to conclusion ¬P.

Reading: §5.3, §6.3

Alternative textbook exercises (regular): 6.24--6.26

DeMorgan: ¬(A ∧ B) ⫤⊨ ¬A ∨ ¬B (235)

truth-tables

Introduces DeMorgan's Laws relating ¬, ∧ and ∨. The laws can be stated as A ∧ B ⫤⊨ ¬(¬A ∨ ¬B) and A ∨ B ⫤⊨ ¬(¬A ∧ ¬B). Also mentions that A → B ⫤⊨ ¬A ∨ B.

Reading: §3.6, §4.2

Alternative textbook exercises (regular): 3.19, 4.15--18, 7.1--7.2, *7.3--7.6

Alternative textbook exercises (fast): 3.19, 4.31

Get Some Quantifiers: Don't Economise (473)

quantification

We're going to be using quantifiers a lot. We understand them thanks to Frege and Taski. It's important to get a pair you like.

Reading: §9.1

Everything Is Broken (471)

quantification

Quantifiers are for talking about things without naming them.

Reading: §9.1, §9.2

Alternative textbook exercises (regular): 9.1 odd numbers only, 9.2 even numbers only

Alternative textbook exercises (fast): 9.8–-9.10

Lecture 08

Date given: Thursday 4th February 2016

Exercises for this lecture:

Get Some Quantifiers: Don't Economise (473)

quantification

We're going to be using quantifiers a lot. We understand them thanks to Frege and Taski. It's important to get a pair you like.

Reading: §9.1

Everything Is Broken (471)

quantification

Quantifiers are for talking about things without naming them.

Reading: §9.1, §9.2

Alternative textbook exercises (regular): 9.1 odd numbers only, 9.2 even numbers only

Alternative textbook exercises (fast): 9.8–-9.10

All Squares Are Blue (503)

quantification revision

Explains how to translate 'All squares and blue' and 'Some squares are blue' into awFOL using quantifiers.

Reading: §9.2, §9.3, §9.5

Alternative textbook exercises (regular): 9.4--9.5, 9.8--9.10

What does ∀ mean? (492)

semantics

Explains the meaning of ∀ with an example.

Reading: §9.4

Vegetarians Are Evil (502)

quantification

Practices translating an English argument involving quantifers into awFOL.

Reading: §9.2, §9.3, §9.5

Counterexamples with Quantifiers (502b)

quantification

Illustrates giving a counterexample to an argument involving quantifiers.

We knew that it was invalid ... (163)

definition

Some arguments are logically valid even though the conclusion is unrelated to the premises.

DeMorgan: ¬(A ∧ B) ⫤⊨ ¬A ∨ ¬B (235)

truth-tables

Introduces DeMorgan's Laws relating ¬, ∧ and ∨. The laws can be stated as A ∧ B ⫤⊨ ¬(¬A ∨ ¬B) and A ∨ B ⫤⊨ ¬(¬A ∧ ¬B). Also mentions that A → B ⫤⊨ ¬A ∨ B.

Reading: §3.6, §4.2

Alternative textbook exercises (regular): 3.19, 4.15--18, 7.1--7.2, *7.3--7.6

Alternative textbook exercises (fast): 3.19, 4.31

Lecture 09

Date given: Tuesday 9th February 2016

Exercises for this lecture:

Scope: A Mistaken Application of ¬Elim (291)

definition syntax

Describes a mistaken application of the rule ¬Elim. Asks why this application is mistaken.

Alternative textbook exercises (regular): 6.8

Scope (290)

definition syntax

Defines the notion of scope using trees; explains its application in constructing proofs and truth-tables.

Reading: §3.5

Alternative textbook exercises (regular): 3.14, 3.15

Scope and Negation (320)

semantics

Explores differences between the negation of a disjunction and a disjunction of negations. That is, between ¬(A∨B) and (¬A∨¬B)

Reading: §3.5, §3.6

Proof Example: ¬(P∨Q) therefore ¬P∧¬Q (821)

proof revision proof-example

Describes how to prove ¬(P∨Q) therefore ¬P∧¬Q.

Alternative textbook exercises (regular): 6.24--6.27

I Met a Philosopher (501)

quantification

Explains how to express propositions like 'I met a philosopher' by using the existential quantifier together with conjunction.

Reading: §9.2, §9.3, §9.5

Alternative textbook exercises (regular): 9.1 odd numbers only, 9.2 even numbers only, 9.4, 9.5, 9.8, 9.9, 9.10, 9.12

Alternative textbook exercises (fast): 9.8, 9.9, 9.10, 9.12, 9.13

Scope and Quantifiers (710)

semantics

Explores differences between ∃x(Square(x) ∧ Blue(x)), some squares are blue, and ∃x Square(x) ∧ ∃x Blue(x), something is square and something is blue.

Reading: §9.5, §9.6

Proof Example: ¬P∨R therefore P→R (820)

proof revision proof-example

Describes how to prove ¬P∨R therefore P→R.

∀Elim (800)

quantification proof

Explains the rule of proof ∀Elim with an example.

Reading: §13.1

Lecture 10

Date given: Thursday 11th February 2016

Exercises for this lecture:

∃Intro (801)

quantification proof

Explains the rule of proof ∃Intro.

Reading: §13.2

What does ‘→’ mean? (700)

semantics

Shows how to derive a truth table for → from the rules of proof for →, →Intro and →Elim.

Reading: §7.1

Alternative textbook exercises (regular): 7.1--7.6, 8.1 (yes/no answers are ok)

Alternative textbook exercises (fast): 7.2, 7.5, 7.6

Not If (604)

translation

Negating sentences whose main connective is the arrow is tricky. This contrasts ¬(A → B) with A → ¬B.

↔ : truth tables and rules (567)

translation

Mentions the truth-tables and rules of proof for the biconditional, ↔.

Fubar Rules (340)

meta

Introduces a fake rule of proof, ∧Fubar. The challenge is to explain what is wrong with ∧Fubar.

Reading: §8.3

What does ∃ mean? (491)

semantics

Explains the meaning of ∃ with a simple example.

Reading: §9.4

There Does Not Exist (605)

translation quantification

How can we translate sentences involving quantifiers and negation from English into our formal language awFOL? Discusses translating 'Something is not dead' and 'Nothing is dead'; also 'Everything is not broken' and 'Not everything is broken'. New: now includes discussion of first-order counterexamples.

Alternative textbook exercises (regular): 9.12

Alternative textbook exercises (fast): 9.18--9.19

Quantifier Equivalences: ¬∀x Created(x) ⫤⊨ ∃x ¬Created(x) (764)

translation quantifiers semantics

Introduces the logical equivalence that allows us to turn ∀ into ∃, and conversely. Explains how to prove informally that the equivalence holds using the truth-conditions for quantified statements.

Reading: §10.1, §10.3, §10.4

Lecture 11

Date given: Tuesday 23rd February 2016

Exercises for this lecture:

Revision: ∀Elim, ∃Intro (551)

proof

Summary of two rules of proof, ∀Elim and ∃Intro.

Reading: §12.1, §13.1, §13.2

∃Elim (550)

proof

Introduces the rule of proof ∃Elim with an example. The example proof is from premise ∃x( Blue(x) ∧ Square(x) ) to conclusion ∃x Blue(x).

Reading: §12.2, §13.2

Translation with Quantifiers (507)

translation

Discusses how to translate 'Some persuasive arguments are not valid' and 'All quadrumanous discordians weep and wail except Gillian Deleude' into first-order logic.

Reading: §9.5, §9.6

Alternative textbook exercises (regular): 9.4–-9.5, 9.8–-9.9

Alternative textbook exercises (fast): 9.12-–9.13

Don't use ∃ with → (245)

translation

Stresses that ∀ works with → by examining sentences with ∀ and ∧, and ∃ with →.

Alternative textbook exercises (regular): 9.10, 9.15--9.17, *9.18--9

Alternative textbook exercises (fast): 9.10

Watch Out, Here Come Multiple Quantifiers (744)

revision quantification semantics translation

Preliminary to discussion of multiple quantifiers.

Reading: §11.1

Something Is Above Something (740)

quantification semantics

Introduces a simple sentence involving multiple quantifiers. Illustrates how to apply the procedure for determining the truth of sentences involving quantifiers to sentences containing multiple quantifiers.

Reading: §11.1

Alternative textbook exercises (fast): 11.2, 11.4

Multiple Quantifiers: Something Makes Someone Want to Die Inside (741)

quantification semantics translation

Introduces translation from English to awFOL using multiple existential quantifiers with an example.

Reading: §11.1

Multiple Quantifiers: Everyone Likes Puffins (742)

quantification semantics translation

Introduces translation from English to awFOL using multiple universal quantifiers with an example.

Reading: §11.1

Alternative textbook exercises (regular): 11.2

Quantifiers Bind Variables (711)

semantics

Illustrates how quantifiers bind variables (but does not define this). Contrast ∀x(Square(x) → Blue(x)), all squares are blue, with ∀x Square(x) → ∀x Blue(x), if everything is square then everything is blue.

Reading: §9.3

Summary of Quantifier Rules So Far (571)

proof

Summary of ∀Elim, ∃Intro and ∃Elim.

Reading: §12.1, §12.2, §12.3, §13.1, §13.2

∀Intro (570)

proof proof-example

Introduces the rule of proof ∀Intro with an example. The example proof is from premise ∀x(Square(x) → Blue(x)) to conclusion ∀x Square(x) → ∀x Blue(x).

Reading: §12.1, §12.3, §13.1

Alternative textbook exercises (regular): 12.4--12.5, *12.6--12.7, 12.9--12.10

∀Intro: An Incorrect Proof (572)

proof

Discussion of an incorrect proof which appears to apply ∀Intro to prove this invalid argument: (∀x Square(x)) → (∀x Blue(x)) therefore ∀x(Square(x) → Blue(x)).

Reading: §13.1, §13.2

Lecture 12

Date given: Thursday 25th February 2016

Exercises for this lecture:

Relations: Reflexive, Symmetric (120)

quantification relations counterexamples

Explains what it is for a relation to be reflexive, and what it is for a relation to be symmetric.

Reading: §15.1, §15.6

Relations: Transitivity (125)

quantification relations counterexamples

Explains what it is for a relation to be transitive. Describes how to show, using counterexamples, that the relation NotAdjacent (which holds between two objects just when the first is not adjacent to the second) is not transitive. Also describes how to express the counterexample formally.

Reading: §15.1, §15.6

Relations: Some Examples (128)

quantification relations

Practices identifying whether a given relation is reflexive, symmetric or transitive. Also practices finding relations with some given set of features (e.g. find a relation that is reflexive and symmetric but not transitive).

Reading: §15.1, §15.6

Defining Relations Using Dot-Arrow Diagrams (129)

relations

Describes how to use dot-arrow diagrams to define relations.

Expressing Relations with Quantifiers (581)

quantification relations

Describes how quantifiers can be used to express the claim that a particular relation is reflexive, symmetric or transitive. Also introduces dot-arrow diagrams to describe relations.

Reading: §15.1, §15.6

Alternative textbook exercises (regular): 15.33--15.40 (second edition)

Alternative textbook exercises (fast): 15.33, 15.37--15.39 (second edition)

Negating Identity (323)

semantics

Sometimes people think that ¬a=b and ¬(a=b) mean something different. They don't.

There Does Not Exist (605)

translation quantification

Alternative textbook exercises (regular): 9.12

Alternative textbook exercises (fast): 9.18--9.19

Expressing Counterexamples Formally (583)

counterexamples relations

Describes how quantifiers can be used to express the claim that a particular relation is reflexive, symmetric or transitive.

Reading: §15.1, §15.6

Summary of Relations (126)

relations

Quick summary definition of reflexive, symmetric and transitive.

Proof Example: A∧B therefore ¬(¬A∨¬B). (822)

proof revision proof-example

Describes how to prove A∧B therefore ¬(¬A∨¬B)..

Proof Example: P therefore ¬¬P. (823)

proof revision proof-example

Describes how to prove P therefore ¬¬P.

Proof Example: S∨(Q∧R) therefore S∨Q. (824)

proof revision proof-example

Describes how to prove S∨(Q∧R) therefore S∨Q.

Lecture 13

Date given: Tuesday 1st March 2016

Exercises for this lecture:

There Is a Store for Everything (560)

quantification semantics translation

Explains how to translate English sentences involving a combination of universal and existential quantifiers into awFOL with an example.

Reading: §11.2, §11.3

Alternative textbook exercises (regular): 11.3, 11.4, 11.8, 11.9, 11.11, 11.13, *11.10

Alternative textbook exercises (fast): 11.8, 11.9, *11.11

How Big Is a Truth-Table? (431)

meta truth-tables

Explains how to determine how many rows a truth table for a sentence containing 2, 3 or 369 sentence letters would be.

Truth-functional completeness (430)

meta truth-tables

Explains what it is for a set of connectives to be truth-functionally complete. Proves that {¬, ∧, ∨} is truth-functionally complete. ‘A set of truth-functors is said to be expressively adequate (or sometimes functionally complete) iff, for every truth function whatever, there is a formula containing only those truthcfunctors which express that truthcfunction, i.e. which has as its truthctable the truthctable specifying that function.’ (Bostock, Intermediate Logic p. 45).

Reading: §7.4

Alternative textbook exercises (regular): 7.25, 7.26, *7.28, 7.29

Alternative textbook exercises (fast): 7.25, 7.26, *7.28, 7.29

Lecture 14

Date given: Thursday 3rd March 2016

Exercises for this lecture:

Two Things Are Broken (470)

quantification semantics

Explains how to translate sentences involving number into awFOL using quantifiers and identity.

Reading: §14.1

Loving and Being Loved (755)

quantifiers translation

Discusses translating English sentences about loving and being loved in order to illuminate the difference between ∃y∀x Loves(x,y) and ∃y∀x Loves(y,x).

Reading: §11.2, §11.3

Somebody Is Not Dead (607)

translation quantification

Continues discussion of how to translate sentences involving quantifiers and negation from English into our formal language awFOL? Discusses translating 'Some person is not dead' and 'No person is dead'; also 'Every person is not dead' and 'Not every person is dead'.

Quantifier Equivalences: ∀x(Square(x) → Broken(x)) ⫤⊨ ∀x(¬Broken(x) → ¬Square(x)) (760)

translation quantifiers

Describes how we can use knowledge of equivalences among propositional sentences to get quantifier equivalences with an example. The example is the inference from this: A → B ⫤⊨ ¬B → ¬A, to this: ∀x(Square(x) → Broken(x)) ⫤⊨ ∀x(¬Broken(x) → ¬Square(x)).

Reading: §10.3

Alternative textbook exercises (regular): 10.20, 10.22

Quantifier Equivalences: ∀x(Square(x) → Broken(x)) ⫤⊨ ∀x(¬Square(x) ∨ Broken(x)) (762)

translation quantifiers

A further example of how we can use knowledge of equivalences among propositional sentences to get quantifier equivalences.

Reading: §10.3

More Dead Horse (565)

quantification semantics translation

Continues the discussion of how to translate English sentences involving a combination of universal and existential quantifiers into awFOL with an example, 'There is a store for everything.' Also discusses structural ambiguities related to quantifier scope and how to use awFOL to pin down this sort of ambiguity.

Reading: §11.4, §11.5

Lecture 15

Date given: Tuesday 8th March 2016

Exercises for this lecture:

Soundness and Completeness: Statement of the Theorems (400)

meta

Explains what it is for a system of proof, such as Fitch, to be sound; and what it is for a system of proof to be complete.

Reading: §8.3, §13.4

The Soundness Property and the Fubar Rules (fast) (346)

meta

Identifies a property of the rules of proof in Fitch: no rule allows us to go from truths to a falsehood. Illustrates by contrasting ∧Elim with ∧Fubar.

Reading: §8.3

Alternative textbook exercises (regular): 7.32

Alternative textbook exercises (fast): 7.32

Proof of the Soundness Theorem (410)

meta

Sketches a proof of the soundness theorem for the propositional part of our formal system of proof, Fitch.

Reading: §8.3

Translation from awFOL to English (951)

translation quantification revision

Revises translation from awFOL to English by considering some questions from an exam paper.

Alternative textbook exercises (regular): 14.1--14.3, (*14.4--14.5)

Numerical Quantifiers (620)

quantification translation

Explains how to translate sentences involving number, such as exactly two things are broken, into awFOL using quantifiers and identity.

Reading: §14.1

Alternative textbook exercises (fast): 14.2--14.3, 14.4--14.5, 14.10--14.11

Lecture 16

Date given: Thursday 10th March 2016

Exercises for this lecture:

There Is Exactly One (625)

translation

Mentions several ways of expressing the idea that there is exactly one creator in our formal language, awFOL.

Alternative textbook exercises (regular): 14.10--14.12, *14.13

Alternative textbook exercises (fast): 11.10, 11.13, 14.2

Every Time I Go to the Dentist Someone Dies (750)

quantifiers translation

Discusses translating English sentences involving obscured quantifiers into awFOL with an example.

Reading: §11.2

Could There Be Nothing? (805)

quantification proof

Our system of proof, Fitch, allows us to prove that something exists from no premises. So if Fitch is sound, there must not be a possible situation in which nothing exists. Here we look at what three proofs that somehing exists which indicate how Fitch would need to be restricted so that it does not allow us to prove that something exists from no premises.

Reading: §13.2

Proofs about Proofs (440)

meta

Explains how to prove proofs about proofs. Examples include: (i) if A ⊢ B then ⊢ A → B, (ii) if A ⊢ B then A ⊢ ¬¬B

Does ‘if’ mean what ‘→’ means? (640)

semantics quirk

Argues that ‘if’ must mean what ‘→’ means, and that it cannot.

Reading: §7.3

Lecture 17

Date given: Tuesday 15th March 2016

Exercises for this lecture:

Revison: Definitions (972)

definitions

Discusses the first part of many exam questions.

Revison: Truth tables (975)

quantification translation

Discusses an exam question.

Revison: Proofs (propositional) (977)

proof proof-example

Discusses an exam question.

Revison: Proofs (with quantifiers) (979)

proof proof-example

Discusses an exam question.

Revison: Translation from English to awFOL (971)

quantification translation

Discusses an exam question.

Proof Example: ∃x Dead(x) ⊢ ¬∀x¬ Dead(x). (825)

proof revision proof-example

Describes how to prove that not everything is not dead given that something is dead.

Alternative textbook exercises (fast): 13.43--13.45

Proof Example: ¬∀x Dead(x) ⊢ ∃x¬ Dead(x). (826)

proof revision proof-example

Describes how to prove that something is not dead from the premise that not everything is dead.

Alternative textbook exercises (fast): 13.49--13.50

The End Is Near (790)

quantification translation

Extremely brief introduction to definite descriptions. Hints at how sentences such as 'The winner is hungry' might be translated into awFOL.

Reading: §14.3

Alternative textbook exercises (regular): 14.26, 14.28

Alternative textbook exercises (fast): 14.2, 14.4, 14.5, 14.10, 14.11, 14.26, 14.28

Lecture 18

Date given: Thursday 13th March 2014

Exercises for this lecture:

Proofs about Proofs (440)

meta

Explains how to prove proofs about proofs. Examples include: (i) if A ⊢ B then ⊢ A → B, (ii) if A ⊢ B then A ⊢ ¬¬B

A ⊨ ⊥ (467)

meta

Explains what A ⊨ ⊥ means. (A ⊨ ⊥, i.e. the argument with premises A and conclusion ⊥ is logicallly valid.)

If (A ⊬ ⊥ entails A ⊭TT ⊥) then (A ⊨TT B entails A ⊢ B) (469)

meta

This is a step towards our proof of the completeness theorem. The completeness theorem says A ⊨TT B entails A ⊢ B. Here we prove that we can show this by showing that A ⊬ ⊥ entails A ⊭TT ⊥.

The Essence of the Completeness Theorem (450)

meta

Outlines how the completeness theorem for the propositional part of our formal proof system, Fitch, will work.

Reading: §8.3

Lemma for the Completeness Theorem (453)

meta

Proves the following claim, where Γ is a set of sentences of awFOL: if for every sentence letter P, either Γ⊢P or Γ⊢¬P, then for every sentence of awFOL φ, either Γ⊢φ or Γ⊢¬φ.

Reading: §8.3