Talk:Entscheidungsproblem

“Entscheidungsproblem” is decidable

The following argument should be presumed wrong because it has not been published in a peer-reviewed scientific journal. Other editor(s) have commented that the proof appears wrong, but it is not their duty to prove it, as encyclopedias are not places for original research: see WP:NOR. Do not post other proofs here unless they have already been published in peer-reviewed scientific journals.

From Neil Immerman, “Computability and Complexity” in Stanford Encyclopedia of Philosophy @Internet:

In the 1930's, well before there were computers, various mathematicians from around the world invented precise, independent definitions of what it means to be computable. Alonzo Church defined the Lambda calculus, Kurt Gödel defined Recursive functions, Stephen Kleene defined Formal systems, Markov defined what became known as Markov algorithms, Emil Post and Alan Turing defined abstract machines now known as Post machines and Turing machines.

Surprisingly, all of these models are exactly equivalent: anything computable in the lambda calculus is computable by a Turing machine and similarly for any other pairs of the above computational systems. After this was proved, Church expressed the belief that the intuitive notion of "computable in principle" is identical to the above precise notions. This belief, now called the "Church-Turing Thesis", is uniformly accepted by mathematicians.

Part of the impetus for the drive to codify what is computable came from the mathematician David Hilbert. Hilbert believed that all of mathematics could be precisely axiomatized. He felt that once this was done, there would be an "effective procedure", i.e., an algorithm that would take as input any precise mathematical statement, and, after a finite number of steps, decide whether the statement was true or false. Hilbert was asking for what would now be called a decision procedure for all of mathematics.

As a special case of this decision problem, Hilbert considered the validity problem for first-order logic. First-order logic is a mathematical language in which most mathematical statements can be formulated. Every statement in first-order logic has a precise meaning in every appropriate logical structure, i. e., it is true or false in each such structure. Those statements that are true in every appropriate structure are called valid. Those statements that are true in some structure are called satisfiable. Notice that a formula, Φ, is valid if and only if its negation, ~Φ, is not satisfiable.

Hilbert called the validity problem for first-order logic, the entscheidungsproblem. In a textbook, Principles of Mathematical Logic by Hilbert and Ackermann, the authors wrote, "The Entscheidungsproblem is solved when we know a procedure that allows for any given logical expression to decide by finitely many operations its validity or satisfiability.… The entscheidungsproblem must be considered the main problem of mathematical logic."

From Angelo Margaris, First Order Mathematical Logic (New York: Dover Publications Inc., 1990) , pp. 99 – 100):

A formula whose distinct prime constituents are P1, P2, P3, . . ., Pn is in conjunctive normal form (CNF) if and only if it has the form

(P11 OR ... OR P1n) AND (P21 OR ... OR P2n) AND ... AND (Pm1 OR ... OR Pmn)

where each Pij is either Pj or ~Pj --- that is, a conjunction of disjunction clauses of prime constituents or their negations.

Theorem 9. Every formula that is not a tautology is equivalent to a formula in conjunctive normal form.

But this theorem is only true for sentential logic, not first-order predicate calculus. Therefore, your argument fails at this step. --greenrd 15:40, 25 December 2005 (UTC)

This discussion section, which by Wikipedia policy could be edited by anyone, is not the main article section --- that means, theories and proofs could be freely discussed here. Let us not stifle knowledge. Thank you for your rebuttal. Following the first-order mathematical logic concepts, terminology (in particular, "prime constituents"), formal symbols and axiom schemas provided by Margaris for the statement and first-order predicate calculus, what is it in Margaris' theorem that limits it to the statement calculus and does not apply to the predicate calculus? Could we not simply claim it true also to the no-quantifier formula of a predicate formula in prenex normal form and, hence, to the prenex normal form formula? [[email protected] 28 December 2005]

Please refer to Wikipedia article "Quantified Boolean Formula Problem" and its cited reference-link Vorlesung Letz. Efficient Decision Procedures for Quantified Boolean Formulas. TU München: Logikbasierte Entscheidungsverfahren. 2003.

A disjunction clause may have 1 or more (up to n) prime constituents or their negations. However, if C is a disjunction clause and P is a prime constituent then (C OR P) AND (C OR ~P) = C. Hence, each disjunction clause in a CNF formula could be lengthen so that all the n prime constituents are used in each disjunction clause. In this full CNF form, with n prime constituents and m disjunction clauses, a truth-value assignment solution <P1, P2, P3, …, Pn> (Pi is either True or False for each i, 1 <= i <= n) that satisfies each of the disjunction clauses of the formula (and so also their entire conjunction or the formula itself) could be easily found.

First, for n prime constituents, there are at most 2**n disjunction clauses that could be set up in a CNF formula and there are as many 2**n maximum number of possible truth-value assignment solutions <P1, P2, P3, …, Pn> that could be established. If the CNF formula involves the conjunction of all of the 2**n possible disjunction clauses, then the all-False truth-value assignment would clearly not satisfy it since one of the 2**n possible disjunction clauses evaluates to False. For each disjunction clause not included in the CNF formula, a valid truth-value assignment solution <P1, P2, P3, …, Pn> to the latter could be readily set up by simply assigning True to every prime constituents that is negated, and False if not negated, in the former. This is easily proved: for any possible truth-value assignment solution <P1, P2, P3, …, Pn>, P1 satisfies half [that is, 2**(n-1)] of all the 2**n possible disjunction clauses; P2 satisfies half [that is, 2**(n-2)] of all the 2**(n-1) possible disjunction clauses not satisfied by P1; P3 satisfies half [that is, 2**(n-3)] of all the 2**(n-2) possible disjunction clauses not satisfied by P1 and P2; . . . and so on . . .; Pn-1 satisfies half [that is, 2**1 = 2] of all the 2**2 = 4 possible disjunction clauses not satisfied by P1, P2, . . ., and Pn-2; Pn satisfies half [that is, 2**0 = 1] of all the 2**1 = 2 possible disjunction clauses not satisfied by P1, P2, . . ., and Pn-1; and the sole disjunction clause not satisfied by <P1, P2, P3, …, Pn> is the one wherein, for 1 <= i <= n, Pi is True if the ith prime constituent in the disjunction clause is negated otherwise Pi is False (that is, its self-contradiction disjunction clause).

The above argument unequivocally resolves the decidability, validity and computability issues of mathematical logic and theoretical computer science. What must be emphasized as affirmed in the preceding reasoning is that a self-contradictory formula is barred ab initio in truth-functional logic (that is, Boolean or 2-valued logic wherein the truth-value of a compound logical formula is determined by the truth-values of its prime constituents). Indeed, Aristotle’s 3 “laws of thought” [the first principles of identity (P --> P), excluded middle (P OR ~P), and non-contradiction (~(P AND ~P))] are embodied in the very definition of truth-functional logic. The imprudent relegation to mere “theorems” (that is, that they are derivable from “more primitive” axioms) of Aristotle’s 3 “laws of thought” [together with Georg Cantor’s “actual” or “completed” infinite set (this is also a self-contradiction!)] in Gottlob Frege’s logic with his material implication (adopted by Alfred North Whitehead and Bertrand Russell in their Principia Mathematica, and embraced by David Hilbert and Kurt Gödel in their respective logical or formal systems) is the root cause of the “modern crisis” in the foundations of mathematics. With material implication, both ~P --> Q and ~P --> ~Q are true [which is equivalent to P <--> ~P (self-contradiction!) by contraposition --- this is also a first principle since it is definitionally equivalent (check its truth-table) to material implication and it prevents infinite regress of reasoning] --- this makes Frege’s logic inherently inconsistent. Similarly with Set Theory, the empty or null set is an element of the power set of any given set (hence, as well as the power set of any set’s complement-set – this is also a self-contradiction!) --- this also makes Set Theory intrinsically inconsistent. As a matter of fact, our culture is littered with self-contradictions --- from logic’s “I am lying” to a graffito that says “Ban graffiti!” to “yin and yang”. What holds logic, and our culture together, is Aristotle’s first principle of non-contradiction (a proposition and its negation cannot be both true at the same time in the same respect) --- being definitionally equivalent to the first principle of identity, which simply declares that “something is what it is”, it is certainly a more primitive axiom than Principia Mathematica’s principle of tautology [(P OR P) --> P)]. Thus, Kurt Gödel’s theorem, which invokes “This assertion cannot be proved! (a self-contradiction) is not tenable. Georg Cantor’s diagonal argument is also a self-contradiction. (Please read my Wikipedia discussion notes on this article as well as on “Cantor’s theorem”, “Cantor’s first uncountability proof”, “Ackermann’s function”, and “Definable numbers”)

With regard to the computational complexity issue, it is admitted that the conversion to full length-n of all the disjunction clauses in a CNF propositional formula would require “exponential”-time (powers of 2) computations. However, concern for “polynomial” (variable base, constant exponent) against “exponential” (constant base, variable exponent) functions is indeed self-contradictory considering that, by the binomial theorem, 2**n = 1 + n + n(n-1)/2 + . . . + O([n/2]) + . . . + n(n-1)/2 + n + 1. A denial that the right-hand side of this equation is not really a “polynomial” expression [since it has a function of n (actually an arbitrary constant) exponent] does not discount the fact that the “exponential” left-hand side expression is bound by a “polynomial” function of degree m = [n/2] (here, [x] is the greatest integer less than or equal to x).

Please read my discussion notes (already archived) on the Wikipedia article “Boolean satisfiability problem” for details. I have 2 deterministic, polynomial-time algorithms for simply deciding (“One+-solution algorithm”) and for fully solving (“All-solutions algorithm”) 3-SAT decision problems --- they are implemented as Microsoft Visual FoxPro Relational Data Base Management System computer application programs.

[email protected] [09 December 2005]