HOUSE_OVERSIGHT_015939.jpg

Software 249

The final example is in prenex normal form. The symbol '∃' means
'there exists' and R stands for relationship in this equation. All logical
statements can be translated into this form using a purely mechanical
process. There is even a website that will do this for you. It’s useful but I
don’t recommend it as entertainment!

In the example above, something exists in relation to the existence
of something else: one person who loves another. Give me a name and I
can look up the person they love. This is simple. A computer can easily
solve such problems. Indeed there are hundreds of websites doing this
every day. Once you’ve solved one problem of this type, you have solved
them all.

We can rearrange Diophantine equations into many different
prenex forms. The simplest form might be, ‘there exists an x which solves
the following equation, x equals three.’ This would be written out as ∃x,
x=3 and is of the ∃ class – ‘there exists’. There are slightly more complex
classes than our simple ∃ relationship: ∀∃∀ ‘for all, there exists for all’ or
the class ∀²∃∀ ‘for all, for all, there exists, for all’. Each of these groups of
equation is called a ‘reduction class’.

One way to think about a reduction class is as a problem in topology,
‘knots’, to non-mathematicians. Imagine someone handed you a bunch
of tangled cables – the sort of mess you get when they are thrown
haphazardly into a drawer. You can tease them apart and rearrange
them but you must not cut them or break any connection. Once you
have done this you will be left with a series of cables on the desk. They
are all separate, looped or in someway knotted together. Each cable has
a fundamental topological arrangement: straight cables, granny knots,
figure eight, and so on. You have reduced them to their simplest form,
their logical classes. The same goes for logical statements. Once you
have rearranged logical statements into their simplest form you can lay
them out and group them together according to their complexity. Each
group makes up a reduction class and you can ask whether that class as a
whole is automatically decidable. It is a huge task to untangle and classify
mathematical problems, and it took Robinson and her colleagues nearly
forty years to succeed.

It turns out problems with a form as simple as ∀∃∀ (for all,
there exists, for all) have no general purpose algorithm. Each must be
examined individually and solved by something that is not a computer.
This is a remarkable result as the logic boundary is set quite low. An ∃∃,
(exists, exists), class of problem is automatically solvable by a general

HOUSE_OVERSIGHT_015939