Search All of the Math Forum:
Views expressed in these public forums are not endorsed by
NCTM or The Math Forum.



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 quadrillion cycles".
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 subformulas 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! Powered By SQL
SELECT HEADS.id FROM QUERY INNER JOIN HEADS ON QUERY.ref=HEADS.ref AND QUERY.term=HEADS.term
DATABASE QUERY id ref term ref term   6 1 test1 6 2 aaa 7 1 test1 <=> 1 test1 7 2 bbb <=> 2 bbb  



