A problem is computable if it can be
solved by some algorithm; a problem
that is noncomputable cannot be
solved by any algorithm.
Halting Problem,
Alan Turing
The way to show that uncomputable
problems exist is to find one, similarly to the
way G¨odel showed unprovable true
statements exist by finding an unprovable
true statement.
A convincing proof requires a
formal model of computing. This
is why Alan Turing developed a
model of computation.
Perhaps there is a procedure in some more
powerful programming language in which it is
possible to implement a solution to the Halting
Problem. In fact, we will see that no more
powerful programming language exists.
Proved that
noncomputable problems
exist.
Mechanizing Reasoning
Aristotle’s Organon developed rules of
inference known as syllogisms to
codify syllogisms logical deductions in
approximately 350 BC.
Euclid -> axiomatic system, a
formal system consisting of a set
of axioms and a set of in-
axiomatic system ference rules to
codify knowledge in some domain.
five axioms (more commonly known
as postulates),five common notions,,
468 propositions
A proof of a proposition in an
axiomatic systemis a sequence
of steps that ends with the
proposition.
A consistent axiomatic
system is one that can
never derive
contradictory
statements by starting
from the axioms and
following the inference
rules.
A complete axiomatic
system can derive all true
statements by starting
from the axioms and following
the inference rules. This means
if a given proposition is true,
some proof for that proposition
can be found in the system.
Bertrand Russell discovered a problem with
Frege’s system, which is now known as Russell’s
paradox.
In 1913, Whitehead and Russell published
Principia Mathematica
Godel showed that no powerful axiomatic
system could be both complete and consistent:
no matter what the axiomatic
system is, if it is powerful enough
to express a notion of proof, it
must also be the case that there
exist statements that can be
expressed in the system but
cannot be proven either true or
false within the system.
Godel established that no interesting
and consistent axiomatic system is
capable of proving all true statements
in the system
are there problems for which no
procedure exists that produces the
correct output for every possible
problem instance in a finite amount
of time??
problem: A description of an
input and a desired output.
procedure: A specification of
a series of actions.
algorithm: A procedure that
is guaranteed to always
terminate.
a bold attempt to mechanize
mathematical reasoning