Re: Mathematical incompleteness has always been a misconception --- Tarski

On 2025-02-21 23:22:23 +0000, olcott said:

On 2/20/2025 3:01 AM, Mikko wrote:

On 2025-02-18 13:50:22 +0000, olcott said:
 

On 2/18/2025 6:25 AM, Richard Damon wrote:

On 2/17/25 10:59 PM, olcott wrote:

On 2/12/2025 4:21 AM, Mikko wrote:

On 2025-02-11 14:07:11 +0000, olcott said:
 

On 2/11/2025 3:50 AM, Mikko wrote:

On 2025-02-10 11:48:16 +0000, olcott said:
 

On 2/10/2025 2:55 AM, Mikko wrote:

On 2025-02-09 13:10:37 +0000, Richard Damon said:
 

On 2/9/25 5:33 AM, Mikko wrote:

Of course, completness can be achieved if language is sufficiently
restricted so that sufficiently many arithemtic truths become inexpressible.
 It is far from clear that a theory of that kind can express all arithmetic
truths that Peano arithmetic can and avoid its incompletness.

 WHich, it seems, are the only type of logic system that Peter can understand.
 He can only think in primitive logic systems that can't reach the complexity needed for the proofs he talks about, but can't see the problem, as he just doesn't understand the needed concepts.

 That would be OK if he wouldn't try to solve problems that cannot even
exist in those systems.

 There are no problems than cannot be solved in a system
that can also reject semantically incorrect expressions.

 The topic of the discussion is completeness. Is there a complete system
that can solve all solvable problems?

 When the essence of the change is to simply reject expressions
that specify semantic nonsense there is no reduction in the
expressive power of such a system.

 The essence of the change is not sufficient to determine that.

 In the same way that 3 > 2 is stipulated the essence of the
change is that semantically incorrect expressions are rejected.
Disagreeing with this is the same as disagreeing that 3 > 2.

 But your logic needs to reject some of the results of your logic as semantically incorrect, and thus your logic is itself semantically incorrect.
 

 There is nothing like that in the following concrete example:
LP := ~True(LP)
 In other words you are saying the Prolog is incorrect
to reject the Liar Paradox.
 Above translated to Prolog
 ?- LP = not(true(LP)).
LP = not(true(LP)).

 According to Prolog rules LP = not(true(LP)) is permitted to fail.
If it succeeds the operations using LP may misbehave. A memory
leak is also possible.
 

?- unify_with_occurs_check(LP, not(true(LP))).
false

 This merely means that the result of unification would be that LP conains
itself. It could be a selmantically valid result but is not in the scope
of Prolog language.
 

 It does not mean that. You are wrong.

It does in the context where it was presented. More generally,
unify_with_occurs_check also fails if the arguments are not
unfiable. But this possibility is already excluded by their
successfull unification.

I am not going bother to quote Clocksin and Mellish
proving that you are wrong.

You are right, a quote that does not support your claim
is not a good idea.
--
Mikko