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]