Hilbert’s Entscheidungsproblem: To decide whether a sentence is TRUE or whether it is PROVABLE?
in [Math]
|
Prev: Trajectory branching in Liouville space as the source ofirreversibility
Next: Redshift and Microwave radiation favor Atom Totality and disfavor Big Bang #117; ATOM TOTALITY (Atom Universe) theory; replaces Big Bang theory
From: Charlie-Boo on 31 May 2010 12:11 Wikipedia: In mathematics, the Entscheidungsproblem is a challenge posed by David Hilbert in 1928. The Entscheidungsproblem asks for an algorithm that will take as input a description of a formal language and a mathematical statement in the language and produce as output either "True" or "False" according to whether the statement is true or false. Martin Davis 2000 (The Universal Computer a.k.a. Engines of Logic) p. 146: HILBERT'S ENTSCHEIDUNGSPROBLEM Hilbert had also sought explicit calculational procedures by means of which it would always be possible to determine, given some premises and a proposed conclusion written in the notation of what has come to be called first-order logic, whether Freges rules would enable that conclusion to be derived from those premises. The former reduces to the latter, but vice-versa? C-B
From: Rupert on 31 May 2010 18:39 On Jun 1, 2:11 am, Charlie-Boo <shymath...(a)gmail.com> wrote: > Wikipedia: > > In mathematics, the Entscheidungsproblem is a challenge posed by > David Hilbert in 1928. The Entscheidungsproblem asks for an algorithm > that will take as input a description of a formal language and a > mathematical statement in the language and produce as output either > "True" or "False" according to whether the statement is true or > false. > > Martin Davis 2000 (The Universal Computer a.k.a. Engines of Logic) p. > 146: > > HILBERT'S ENTSCHEIDUNGSPROBLEM Hilbert had also sought explicit > calculational procedures by means of which it would always be possible > to determine, given some premises and a proposed conclusion written in > the notation of what has come to be called first-order logic, whether > Freges rules would enable that conclusion to be derived from those > premises. > > The former reduces to the latter, but vice-versa? > > C-B Solving the Entscheidungsproblem in the latter sense we now know would be equivalent to solving the halting problem. The set of true sentences in the first-order language of arithmetic is more complex than the set of Turing machines that halt, of course, but it is pretty easy to give a proof that if we had solved the decision problem for the latter set we could also solve the decision problem for the former set, by induction on the complexity of sentences. But the point is moot, of course, because the halting problem is unsolvable.
From: Don Stockbauer on 31 May 2010 18:44 On May 31, 5:39 pm, Rupert <rupertmccal...(a)yahoo.com> wrote: > On Jun 1, 2:11 am, Charlie-Boo <shymath...(a)gmail.com> wrote: > > > > > > > Wikipedia: > > > In mathematics, the Entscheidungsproblem is a challenge posed by > > David Hilbert in 1928. The Entscheidungsproblem asks for an algorithm > > that will take as input a description of a formal language and a > > mathematical statement in the language and produce as output either > > "True" or "False" according to whether the statement is true or > > false. > > > Martin Davis 2000 (The Universal Computer a.k.a. Engines of Logic) p. > > 146: > > > HILBERT'S ENTSCHEIDUNGSPROBLEM Hilbert had also sought explicit > > calculational procedures by means of which it would always be possible > > to determine, given some premises and a proposed conclusion written in > > the notation of what has come to be called first-order logic, whether > > Freges rules would enable that conclusion to be derived from those > > premises. > > > The former reduces to the latter, but vice-versa? > > > C-B > > Solving the Entscheidungsproblem in the latter sense we now know would > be equivalent to solving the halting problem. The set of true > sentences in the first-order language of arithmetic is more complex > than the set of Turing machines that halt, of course, but it is pretty > easy to give a proof that if we had solved the decision problem for > the latter set we could also solve the decision problem for the former > set, by induction on the complexity of sentences. But the point is > moot, of course, because the halting problem is unsolvable. Well, the answer is for the machine to do what we all tell each other when working on a problem - "Never give up. Never give up."
From: Charlie-Boo on 3 Jun 2010 23:57
On May 31, 6:39 pm, Rupert <rupertmccal...(a)yahoo.com> wrote: > On Jun 1, 2:11 am, Charlie-Boo <shymath...(a)gmail.com> wrote: > > > > > > > Wikipedia: > > > In mathematics, the Entscheidungsproblem is a challenge posed by > > David Hilbert in 1928. The Entscheidungsproblem asks for an algorithm > > that will take as input a description of a formal language and a > > mathematical statement in the language and produce as output either > > "True" or "False" according to whether the statement is true or > > false. > > > Martin Davis 2000 (The Universal Computer a.k.a. Engines of Logic) p. > > 146: > > > HILBERT'S ENTSCHEIDUNGSPROBLEM Hilbert had also sought explicit > > calculational procedures by means of which it would always be possible > > to determine, given some premises and a proposed conclusion written in > > the notation of what has come to be called first-order logic, whether > > Freges rules would enable that conclusion to be derived from those > > premises. > > > The former reduces to the latter, but vice-versa? > > > C-B > > Solving the Entscheidungsproblem in the latter sense we now know would > be equivalent to solving the halting problem. The set of true > sentences in the first-order language of arithmetic is more complex > than the set of Turing machines that halt, of course, but it is pretty > easy to give a proof that if we had solved the decision problem for > the latter set we could also solve the decision problem for the former > set, by induction on the complexity of sentences. Ok, if it is so easy, then tell us. How would the inductive proof be structured? You first prove that if you can tell whether any single w is provable then you can tell whether any single w is true - is that it? I would think that it would be not so because the set of true sentences is neither r.e. nor co-r.e. That is not so of the set of theorems, their complement, the refutables, the decidables, their complements etc. > But the point is > moot, of course, because the halting problem is unsolvable. No. You cannot say two problems are equivalent because they are both unsolvable. It seems clear that somewhere in history the German got mistranslated. Has anyone else ever noticed this inconsistency? C-B - Hide quoted text - > > - Show quoted text - |