lecture 9 part 1

In this video we look at yet another pattern of implications, and apply our a method for counting the satisfying valuations.

This video looks at the ordering of predicates. We first met thsis as the satisfaction ordering a ⊨ b.We look at the ordering of the 16 possible boolean functions of two variables. We can also view…

In this video we give an example showing how Haskell's types can help us to avoid confusions.We then discuss the types of the Boolean operations lifted to predicates, and show how…

lecture 7 part 3

This video includes a couple of points from a 2019 review lecture on Sequents.First we discuss how to use reduction to find an inhabited model in which Γ ⊨ Δ, which is equivalent to…

In logic, we call the things in the universal model valuations; they are Boolean-values functions defined on the set of predicates.In computer science we often call these states, because, as we will…

We begin by revisiting the idea of a universal model. If we have only n predicates then we can distinguish only 2n kinds of individual. So we only need to consider 2^{2n} universes. For example, for…

Gentzen's rules provide a complete system that does not require the cut rule. For many logical systems, cut elimination (showing that uses of the cut rule may be eliminated from any sound proof)…

lecture 6 part 2

We derive the implication rule using the rules introduced last week.

We introduce sequents, where we have finite sets of predicates on both sides of the turnstile.

Venn diagrams on a sphere.

We show the intuition of contraposition using Venn diagrams.

We use the rules to reduce a sequent to a conjunction of simpler sequents. In this example we find that the expression asserted by the sequent is a tautology — it is equivalent to the empty…