Decidable
ภาวะตัดสินได้
คำจำกัดความภาษาไทย
ภาวะตัดสินได้
ทฤษฎีต่างๆ ในนัยที่ว่าเลขคณิตเป็นทฤษฎีหนึ่ง จะถือว่า “ตัดสินได้” (decidable) หากมีระบบรูปแบบนิยม (formalizations) สำหรับทฤษฎีเหล่านั้นที่มีความสมบูรณ์ (COMPLETE) ในระบบที่ไม่มีประพจน์แบบ ไม่แน่นอน (CONTINGENT) เช่น ระบบรูปแบบนิยมของเลขคณิต สูตรที่สร้างขึ้นอย่างถูกรูปแบบ (well-formed formula) จะตัดสินได้ก็ต่อเมื่อตัวมันเองหรือนิเสธของมันเป็นทฤษฎีบท ทว่าในกรณีที่มีประพจน์แบบไม่แน่นอนเข้ามาเกี่ยวข้อง สูตรที่สร้างขึ้นอย่างถูกรูปแบบจะตัดสินได้ก็ต่อเมื่อเราสามารถพิสูจน์ได้ว่ามันเป็นจริงทางตรรกะ เท็จทางตรรกะ หรือไม่เป็นทั้งสองอย่าง กระบวนการตัดสิน (decision procedure ซึ่งเป็นอัลกอริทึมประเภทหนึ่ง) ช่วยให้เราตัดสินเรื่องนี้ได้ด้วยวิธีการที่เป็นเครื่องจักรกล เพียงแค่ทำตามกฎในจำนวนขั้นตอนที่จำกัด กระบวนการตัดสินมีอยู่จริงสำหรับแคลคูลัสเชิงประพจน์และแคลคูลัสเชิงภาคแสดงเอกบท แต่โดยทั่วไปแล้วจะไม่มีในระบบที่ซับซ้อนกว่านั้น การพิสูจน์ว่ามีหรือไม่มีกระบวนการเช่นนี้ถูกเรียกว่าเป็น คำตอบเชิงบวกหรือเชิงลบต่อ “ปัญหาการตัดสิน” ตามลำดับ โดยคำตอบเชิงลบสำหรับแคลคูลัสเชิงภาคแสดงคือ ทฤษฎีบทของเชิร์ช (1936) [2]
English Definition
Theories, in the sense in which arithmetic is a theory, are decidable if formalizations exist for them which are COMPLETE. In systems without CONTINGENT propositions, such as formalizations of arithmetic, a well-formed formula (see AXIOM SYSTEM) is decidable if and only if it or its negation is a theorem. Where contingent propositions enter, as in formalizations of the propositional CALCULUS, a well-formed formula is decidable if and only if one can prove whether it is logically true, logically false, or neither. A decision procedure (one kind of ALGORITHM) lets one decide this mechanically by simply following a rule in finitely many steps. Decision procedures exist for the propositional and monadic predicate CALCULI, but not, in general, for more complex systems. Proof that such a procedure exists, or does not exist, for a given sphere is called a positive or negative solution, respectively, to the decision problem. The negative solution for the predicate calculus (beyond the monadic) is Church’s theorem (1936). See also RECURSIVE.
คำศัพท์และคำจำกัดความทั้งหมดได้รับการตรวจสอบและอนุมัติโดยผู้ดูแลระบบของ Dictionary of Philosophy.