Defining a decidability decider that consistently decides decidability

[peteolcott]

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

--
Copyright 2019 Pete Olcott
All rights reserved