|
lecture 9 part 1
Course Code
PHIL10086 Licence Type
Creative Commons - Attribution Date Created
November 14th, 2020
|
|
In this video we look at yet another pattern of implications, and apply our a method for counting the satisfying valuations.
Course Code
INFR08025 Licence Type
All rights reserved The University of Edinburgh Language
English
|
|
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…
Course Code
INFR08025 Licence Type
All rights reserved The University of Edinburgh Language
English
|
|
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…
Course Code
INFR08025 Licence Type
All rights reserved The University of Edinburgh Language
English
|
|
lecture 7 part 3
Course Code
PHIL10086 Licence Type
Creative Commons - Attribution Date Created
October 31st, 2020
|
|
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…
Course Code
INFR08025 Licence Type
All rights reserved The University of Edinburgh Language
English
|
|
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…
Course Code
INFR08025 Licence Type
All rights reserved The University of Edinburgh Language
English
|
|
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…
Course Code
INFR08025 Licence Type
All rights reserved The University of Edinburgh Language
English
|
|
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)…
Course Code
INFR08025 Licence Type
All rights reserved The University of Edinburgh Language
English
|
|
lecture 6 part 2
Course Code
PHIL10086 Licence Type
Creative Commons - Attribution Date Created
October 21st, 2020
|
|
We derive the implication rule using the rules introduced last week.
Course Code
INFR08025 Licence Type
All rights reserved The University of Edinburgh Language
English
|
|
We introduce sequents, where we have finite sets of predicates on both sides of the turnstile.
Course Code
INFR08025 Licence Type
All rights reserved The University of Edinburgh Language
English
|
|
Venn diagrams on a sphere.
Course Code
INFR08025 Licence Type
All rights reserved The University of Edinburgh Language
English
|
|
We show the intuition of contraposition using Venn diagrams.
Course Code
INFR08025 Licence Type
All rights reserved The University of Edinburgh Language
English
|
|
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…
Course Code
INFR08025 Licence Type
All rights reserved The University of Edinburgh Language
English
|