0:00

[MUSIC]

Â In this lecture, I will show you how you can use existential and

Â universal quantifiers in your data.

Â So you may recall from your lessons in logic that there is an existential

Â quantifier and a universal quantifier.

Â So the existential quantifier was written using this reversed E.

Â So this says there exists an x such that e(x) holds,

Â and this is valid if we can find a single x such that e holds.

Â And universal quantifier was written down using this upside-down A.

Â And this is true if, for all x, e(x) holds.

Â 0:53

So, typical examples are following the existing x is four.

Â And of course, this is true because we can find x is equal to two.

Â And that makes this true, and therefore, it's true.

Â Better excuse is x is larger than four.

Â Well we it can find an x for instance 5, and

Â therefore this whole expression is also true.

Â Positive x such that x is equal to zero and

Â notice that is a well timed expression because the positive

Â x is actually cast internally to a natural number x and

Â then x is zero is a correct expression.

Â But what we can see is that there is no positive x that is x is equal to zero.

Â So we cannot find a candidate to make x is zero true, and

Â therefore this expression is false.

Â 1:54

For the universal quantifier, we have this example.

Â For every x positive x, x is larger than 0.

Â Well this holds for all x.

Â And therefore this is true.

Â And for all x, x square is equal to four.

Â Well, this is only true for x is two, and not for any other natural number.

Â So obviously this is not true for all x, and

Â therefore this expression reduces to false.

Â 2:31

Okay, how can we use that?

Â Well, internally, it's for instance used to denote the equality of sets.

Â So if we have two sets over an arbitrary domain,

Â d, and we ask ourselves, when are they equal?

Â So when is s1 equal to s2?

Â 2:48

And this is defined as follows, maybe for all d, of type d.

Â D is in as one, if and only if this equals symbol is d if and

Â only if d is equal, is an element of s2.

Â So d is an element of s1 if and only if d is an element of s2.

Â And vice versa, b is an element of s2 if d is element of s1.

Â So this means the set s1 is equal to

Â set s2 and for all elements d,

Â d is in s1 if and only if it's in s2.

Â Another example, this set of prime numbers,

Â so you probably recall what a prime number was.

Â That was a number larger than one which could only be divided by itself or by 1.

Â And you can also express that very concisely.

Â Namely, a number n larger than one is a prime number if,

Â if you try to define it by a number m.

Â So for all positive numbers m between one and n,

Â n divided by m yields a remainder different from zero.

Â Or in other words, n model m is not equal to zero.

Â And if we have this expression to correct prime number,

Â we can also write down the set of all prime numbers.

Â Easily, so this is what it is.

Â The set of all positive numbers larger than one satisfying this expression,

Â saying that it cannot be defined by numbers in-between one and n.

Â And what you will find out is that if you write,

Â would write down this in your specification, then

Â you can do quite a lot with this set if it comes to behavioral analysis.

Â But this does not hold for all expressions with quantifiers, and

Â I will introduce here or show you Fermat's last theorem as a theorem that can very

Â concisely be expressed with quantifiers, but which is extremely hard to solve.

Â But in order to start with Fermat's theorem we should recall

Â the Theorem of Pythagoras, which you may know.

Â So if you have a triangle with one rectangular corner,

Â then you know that a square plus b square is equal to c square.

Â 5:23

And you probably recall the Pythagorean triples or Pythagorean numbers.

Â And these are positive numbers that you can fill in for

Â a, b, and c such that this equation holds.

Â So a typical example is are three, four, and five.

Â Three squared plus four squared is nine plus 16 is 25,

Â exactly the same as five squared.

Â So we can see three, four, and five fits this equation.

Â 5:55

Well, whenever you look at a to the power n,

Â plus b to the power n is c to the power n for larger numbers,

Â then n being equal to two, then we come to Fermat's last theorem.

Â And Fermat's last theorem says that there are no

Â Pythagorean triples when n is larger than two.

Â Or, expressed using quantifiers, we have that for every natural number n,

Â if n is larger than two, then there are no positive numbers a, b, and

Â c such that a to the power n plus b to the power n is c to the power n.

Â And this was his theorem that mathematicians took a few

Â hundred years to actually prove, and the whole proof consists of a whole book.

Â 6:42

What we can do, because we can denote quantifiers,

Â is write processors that look quite simple.

Â And that actually seem to be able to solve Fermat's last theorem.

Â So what we can have is this miracle process with two actions,

Â namely say that the theorem holds or

Â report that the theorem is invalid.

Â We can specify it as follows.

Â Namely, the process Fermat says that if Fermat's theorem holds, it reports that

Â the theorem holds and else, if it does not hold, it reports the theorem is invalid.

Â And what you can see here is that if you write this down you

Â cannot expect the tools to evaluate such an expression, and

Â you will find out that it quickly gets stuck.

Â And this situation most likely, will go on for the next decades.

Â Automated theorem proving is not capable of dealing with theorems of this kind for

Â a long time to come.

Â The big message of this is be careful

Â when using quantifiers if you want to do automatic analysis.

Â 8:51

You can also use them at many other places, but

Â then we cannot expect the tools to handle them properly anymore.

Â And probably when it comes to dealing with the tools and

Â more complex expressions, then you have to replace them with

Â more straightforward candidates suitable for the tools.

Â In the next lecture, I will apply everything you have seen up until now

Â to an example of a rather intricate data structure namely Knuth's dancing links.

Â Thank you for watching.

Â [MUSIC]

Â