Converting formal proofs to conform to sound deductive inference (Simple Essence)

[peteolcott]

In sound deductive inference there is:
[a connected sequence of valid deductions from true premises to a true conclusion].

It would seem that to convert formal proofs to conform to this model:
Axioms could be construed as expressions of language having the semantic
property of Boolean true. This would seem to anchor the syntax of formal
proofs within the semantics of Boolean values.

This would seem to cause the theorem consequences of formal proofs derive:
[a connected sequence of inference from axioms to a true consequence].

The key value of this transformation is that it seems to eliminate
undecidability, incompleteness and inconsistency from formal systems.

This defines the Prolog equivalent to sound deductive inference:
(1) Construing the Prolog database as the formal system.
(2) Construing queries that return "Yes" as True.
(3) Construing negated queries that return "Yes" as False.
(4) Construing ONLY queries that return Yes or return Yes to
their negation are sound deductive inference.

--
Copyright 2019 Pete Olcott All rights reserved

"Great spirits have always encountered violent
opposition from mediocre minds." Albert Einstein