# Defining a decidability decider that consistently decides decidability? [closed]

Decision problem https://en.wikipedia.org/wiki/Decision_problem

Decidability (logic) https://en.wikipedia.org/wiki/Decidability_(logic)

Undecidable problem https://en.wikipedia.org/wiki/Undecidable_problem

Validity and Soundness https://www.iep.utm.edu/val-snd/

I am assuming that everyone reading this post is intimately familiar with all of the above topics. Within this assumption I cannot tell what is unclear about what I am saying without more feedback.

What I am saying is that it seems to me that if a finite string cannot be decided to be accepted and it cannot be decided to be rejected that this finite string is the consequence of deductively unsound inference. (see above).

Could a decidability decider be defined the conforms to the sound deductive inference model such that all decision problems are partitioned into: (1) Yes (2) No (3) Deductively unsound ?

I am going to explain this view in terms of the conventional notion of formal proofs of mathematical logic. Now that this is anchored as properties of finite strings it should be clear. The axioms that I refer to could be considered analogous to Prolog Facts.

A formal proof of mathematical logic is analogous to a Prolog query, yet generalized to function in higher order logic. When we define a decidability decider in terms of the sound deductive inference model any expression of language that is not provable from axioms is simply deductively unsound.

The notion of complete and consistent formal systems is exhaustively elaborated as conventional formal proofs to theorem consequences where axioms are stipulated to be finite strings with the semantic property of Boolean true.

Because valid deduction from true premises necessarily derives a true consequence we know that the following predicate pair consistently decides every deductively sound argument.

// LHS := RHS the LHS is defined as an alias for the RHS
∀x True(x) := ⊢x
∀x False(x) := ⊢¬x

Introduction to Mathematical logic Sixth edition Elliott Mendelson (2015) Pages 27-28 http://liarparadox.org/Provable_Mendelson.pdf

New contributor
PL_OLCOTT is a new contributor to this site. Take care in asking for clarification, commenting, and answering. Check out our Code of Conduct.

## closed as unclear what you're asking by Aryeh, Emil Jeřábek, Marzio De Biasi, Jan Johannsen, GamowMay 16 at 8:04

Please clarify your specific problem or add additional details to highlight exactly what you need. As it's currently written, it’s hard to tell exactly what you're asking. See the How to Ask page for help clarifying this question. If this question can be reworded to fit the rules in the help center, please edit the question.

• Is there a specific question here? The only question mark I see is in the title, but that alone doesn't appear to me to be an interpretable question. – mhum May 16 at 0:43