Search All of the Math Forum:

Views expressed in these public forums are not endorsed by NCTM or The Math Forum.

Notice: We are no longer accepting new posts, but the forums will continue to be readable.

Topic: Very dumb question
Replies: 1   Last Post: Jun 18, 2013 1:57 AM

 Graham Cooper Posts: 4,495 Registered: 5/20/10
Re: Very dumb question
Posted: Jun 18, 2013 1:57 AM

On Jun 18, 1:26 pm, Newberry <newberr...@gmail.com> wrote:
> Let M(x) be a partially decidable predicate. Let Cm be a characteristic function of M(x). Assume that ~M(325) is true. We have computer program that computes Cm. And we want to find out if ~M(325). So we feed 325 to our program and wait. After six hours of staring at the blank screen and 14 quadrillion computer cycles, the brighter types will realize that we will never get there this way. We need to prove the theorem ~M(325).
>
> Does undecidability imply unprovability?
>

That is called BLACK BOX analysis.

You can then use WHITE BOX analysis and work out Why the Function is
not halting by tracing the program code, you may find some constraint
for it to halt that would violate a precondition and prove a result
from that.

You can also work within a bounded framework and say "~M within 14

This happens in PROLOG a lot because it tries to blindly solve queries
using all available options and can go into infinite loops.

---- USER QUERY I/O ----

prove THM true :-
prv THM [z[z[z[z 0]]]]

prove THM false :-
prv [ ! THM ] [z[z[z[z 0]]]]

NOTE: the 4 levels deep of inference searching
is arbitrary and for any logically solvable
problem there exists a finite level that
the solution will be found.

------------------------

prv R [ z Z ] :-
t R

prv R [ z Z ] :-
if L R
prv L Z

STANDARD MODUS PONENS (Depth Limited)

---------------------

By using a depth limit on how many inferences can be made for any
formula (1 less for each level of sub-formulas and so on..)

it is guaranteed to halt and try all possible branches wide.

That way the Theory can return True or False values.

-----------------

prove [ + 1 1 4 ] ANS ?

ANS = false

------------------

after trying 4 levels deep of

prove THM true :-
prv THM [z[z[z[z 0]]]]

and failing, it then tries to prove it false.

******************************

In this way you have a deterministic TRUE or FALSE predicate system,
although bounded by some predefined depth limit.

A BOUND COMPLEXITY SET THEORY is also possible.

set1 = { M | prove X true }

set2 = { M | prove X false }

then
[ e M set1 ] <-> [ not [ e M set2 ]]

---------------------------------------------

Herc

--

http://phpPROLOG.com

A.I. Software / Database on the Web!

FROM QUERY

DATABASE QUERY
id ref term ref term
---------------------- ----------------
6 1 test1
6 2 aaa
7 1 test1 <=> 1 test1
7 2 bbb <=> 2 bbb
---------------------- ----------------