Univalence wrote: ↑
Wed May 15, 2019 11:30 pm
Prolog is Turing-complete
PeteOlcott wrote: ↑
Wed May 15, 2019 11:29 pm
The Prolog inference engine already implements this for every level of logic that it can handle.
True is when a query returns: Yes.
Deductively unsound is when a query returns No.
and therefore subject to the halting problem.
Because Prolog implements the sound deductive inference model Godel's Incompleteness
can not be shown by Prolog because Prolog IS COMPLETE.
https://plato.stanford.edu/entries/goed ... mpleteness
The first incompleteness theorem states that in any consistent formal
system F within which a certain amount of arithmetic can be carried
out, there are statements of the language of F which can neither be
proved nor disproved in F. (Raatikainen 2018)
In Prolog an expression is either provable from facts and rules or it does not exist,
thus in Prolog there is no G in F that is unprovable, its provably true or not in F.
The sound deductive inference model works the same way. Expressions are either
provably true or deductively unsound.