Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]

Groups > comp.lang.c > #143462 > unrolled thread

Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this)

Back to article view | Back to comp.lang.c

Contents

  Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-04-26 09:58 -0500
    Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) Siri Cruise <chine.bleu@yahoo.com> - 2019-04-26 08:20 -0700
      Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-04-26 10:48 -0500
    Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-04-26 10:51 -0500
      Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) Kaz Kylheku <847-115-0292@kylheku.com> - 2019-04-26 17:48 +0000
        Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-04-26 17:22 -0500
          Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) Kaz Kylheku <847-115-0292@kylheku.com> - 2019-04-27 01:13 +0000
            Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-04-27 11:23 -0500
              Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) Kaz Kylheku <847-115-0292@kylheku.com> - 2019-04-27 18:26 +0000
                Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) Ike Naar <ike@iceland.freeshell.org> - 2019-04-27 21:56 +0000
                  Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-04-27 17:13 -0500
                Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-04-27 16:58 -0500
                Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-04-27 17:28 -0500
                Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-04-27 17:44 -0500
                Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-04-27 17:49 -0500
                Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-04-27 18:59 -0500
                Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-04-27 19:44 -0500
                Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-04-27 19:48 -0500
                Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-04-27 21:38 -0500
                  Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-04-29 21:53 -0500
                    Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-04-30 11:55 -0500
                    Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-04-30 12:02 -0500
                      Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) bert <bert.hutchings@btinternet.com> - 2019-04-30 11:06 -0700
                        Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-05-01 00:51 -0500
                          Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) bert <bert.hutchings@btinternet.com> - 2019-05-01 03:21 -0700
                            Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-05-01 07:50 -0500
                              Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-05-01 09:29 -0500
                                Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-05-01 13:53 -0500
                              Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) Keith Thompson <kst-u@mib.org> - 2019-05-01 10:48 -0700
                                Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) Bonita Montero <Bonita.Montero@gmail.com> - 2019-05-01 20:25 +0200
                                  Re: Eliminating Undecidability and Incompleteness in Formal Systems (HP Proof refutation) peteolcott <Here@Home> - 2019-05-01 15:01 -0500
                                Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-05-01 14:01 -0500
                                  Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) David Brown <david.brown@hesbynett.no> - 2019-05-01 23:28 +0200
                                    Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-05-01 16:44 -0500
                                      Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) David Brown <david.brown@hesbynett.no> - 2019-05-02 09:19 +0200
                                        Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) mark.bluemel@gmail.com - 2019-05-02 00:45 -0700
                                          Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) Tim Rentsch <tr.17687@z991.linuxsc.com> - 2019-05-02 09:56 -0700
                                        Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-05-02 09:58 -0500
                                Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-05-01 15:14 -0500
                Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-04-29 18:43 -0500
                  Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-04-29 22:06 -0500
                Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-05-01 15:10 -0500
              Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) Richard Damon <Richard@Damon-Family.org> - 2019-05-04 15:05 -0400
                Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-05-04 15:07 -0500
    Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) Keith Thompson <kst-u@mib.org> - 2019-04-26 19:43 -0700
    Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) Bonita Montero <Bonita.Montero@gmail.com> - 2019-05-01 17:56 +0200

Page 2 of 3 — ← Prev page 1 [2] 3  Next page →

#143540

On 4/30/2019 11:23 AM, taruss@google.com wrote:
> On Monday, April 29, 2019 at 10:41:40 PM UTC-7, peteolcott wrote:
> 
>> Based on these three axioms Gödel's Incompleteness is refuted:
>> Axiom(1) ∀F ∈ Formal_System ∀x ∈ Closed_WFF(F) (True(F, x) ↔ (F ⊢ x))
>> Axiom(2) ∀F ∈ Formal_System ∀x ∈ Closed_WFF(F) (False(F, x) ↔ (F ⊢ ¬x))
>> Axiom(3) ∀F ∈ Formal_System ∀x ∈ Closed_WFF(F) (True(F,x) ∨ False(F,x))
> 
> Not sure why these are axioms. It would seem that these are properties of
> your formal system, which if satisfied would admit it into your system. I don't
> see how asserting that all formal systems obey these axioms work. For arbitrary
> formal systems, it is clear that these axioms do not hold.
>   
>> ∃F ∈ Formal_System ∃G ∈ Closed_WFF(F) (G ↔ ((F ⊬ G) ∧ (F ⊬ ¬G)))
>> There is no sentence G of Formal System F that is neither True nor False in F.
> 
> I would suggest that claiming Gödel's Incompleteness is refuted is too strong a
> statement.
> 
> Instead, the claim that you have is that if you create a suitably constrained
> formal system, then in *that* system you can have complete inference. This is
> well-recognized result. The interesting question is whether the constraints
> needed to achieve this complete inference will leave you with enough expressive
> power to be able to perform interesting inference in your system.
> 
> Certainly one of Gödel's results is that if you have a formal system that is
> expressive enough to include arithmetic, you run into incompleteness. 

Only because the mathematical system that he used to form this proof was too
weak to discern semantic ill formedness:

In the same way that not all finite strings are well-formed formula
(when semantic criteria is applied) not all closed WFF are logic sentences.

Any expression of language that is neither true nor false is
not a logic sentence of any formal system that has been
adapted to conform to the sound deductive inference model.

Logic sentences are always derived from sound deduction. In
the sound deductive inference model this means that there is:
[a connected sequence of valid deductions from true premises to a true conclusion].

When axioms are construed as expressions of language having the
semantic property of Boolean true then the theorem consequences
of formal proofs form:
[a connected sequence of inference from axioms to a true consequence].

In neither case is undecidability, incompleteness or inconsistency possible.


>A
> consequence of that is that your system, therefore, cannot use arithmetic. As
> long as you don't need arithmetic for the inferences of interest, then you may
> find your formal system adequate.
> 
> For an interesting discussion of some issue having to do with decidability and
> efficiency of reasoning, you may want to look at the Description Logic
> research. There are a number of variants of description logic with different
> expressive power and consequently different decisions regarding what can be
> computed, ranging from tractable complete inference to undecidability.
> 
> Overview: https://en.wikipedia.org/wiki/Description_logic
> Complexity: http://www.cs.man.ac.uk/~ezolin/dl/
> 


-- 
Copyright 2019 Pete Olcott All rights reserved

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

[toc] | [prev] | [next] | [standalone]

#143541

On 4/30/2019 11:47 AM, Pascal J. Bourguignon wrote:
> taruss@google.com writes:
> 
>> On Monday, April 29, 2019 at 10:41:40 PM UTC-7, peteolcott wrote:
>>
>>> Based on these three axioms Gödel's Incompleteness is refuted:
>>> Axiom(1) ∀F ∈ Formal_System ∀x ∈ Closed_WFF(F) (True(F, x) ↔ (F ⊢ x))
>>> Axiom(2) ∀F ∈ Formal_System ∀x ∈ Closed_WFF(F) (False(F, x) ↔ (F ⊢ ¬x))
>>> Axiom(3) ∀F ∈ Formal_System ∀x ∈ Closed_WFF(F) (True(F,x) ∨ False(F,x))
>>
>> Not sure why these are axioms. It would seem that these are properties of
>> your formal system, which if satisfied would admit it into your system. I don't
>> see how asserting that all formal systems obey these axioms work. For arbitrary
>> formal systems, it is clear that these axioms do not hold.
>>   
>>> ∃F ∈ Formal_System ∃G ∈ Closed_WFF(F) (G ↔ ((F ⊬ G) ∧ (F ⊬ ¬G)))
>>> There is no sentence G of Formal System F that is neither True nor False in F.
>>
>> I would suggest that claiming Gödel's Incompleteness is refuted is too strong a
>> statement.
>>
>> Instead, the claim that you have is that if you create a suitably constrained
>> formal system, then in *that* system you can have complete inference. This is
>> well-recognized result. The interesting question is whether the constraints
>> needed to achieve this complete inference will leave you with enough expressive
>> power to be able to perform interesting inference in your system.
>>
>> Certainly one of Gödel's results is that if you have a formal system that is
>> expressive enough to include arithmetic, you run into incompleteness. A
>> consequence of that is that your system, therefore, cannot use arithmetic. As
>> long as you don't need arithmetic for the inferences of interest, then you may
>> find your formal system adequate.
> 
> And note that arithmetic is a consequence of Turing Completeness.  So if
> your formals sytem is any useful to a programmer (ie. is Turing
> Equivalent), then it will have arithmetic, and therefore it will be
> inconsistent or incomplete, choose of of two.
> 
> (Ie. correct programs will produce wrong results, or there will be
> programs that you won't be able to prove if it is correct or incorrect).
> 

My system can express anything including arithmetic, it simply does not
do so erroneously:

In the same way that not all finite strings are well-formed
formula (when semantic criteria is applied) not all closed
WFF are logic sentences.

Any expression of language that is neither true nor false is
not a logic sentence of any formal system that has been
adapted to conform to the sound deductive inference model.

Logic sentences are always derived from sound deduction. In
the sound deductive inference model this means that there is:
[a connected sequence of valid deductions from true premises to a true conclusion].

When axioms are construed as expressions of language having the semantic
property of Boolean true (thus anchoring formal proofs in the semantics of
Boolean values) then the theorem consequences of formal proofs form:
[a connected sequence of inference from axioms to a true consequence].

In neither case is undecidability, incompleteness or inconsistency possible.



-- 
Copyright 2019 Pete Olcott All rights reserved

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

[toc] | [prev] | [next] | [standalone]

#143542

On Tuesday, 30 April 2019 18:02:32 UTC+1, peteolcott  wrote:
> >> On Monday, April 29, 2019 at 10:41:40 PM UTC-7, peteolcott wrote:
etcetera

One of the hallmarks of a crank is being the 
author of nearly all of the posts in a thread.

[toc] | [prev] | [next] | [standalone]

#143549

On 4/30/2019 1:06 PM, bert wrote:
> On Tuesday, 30 April 2019 18:02:32 UTC+1, peteolcott  wrote:
>>>> On Monday, April 29, 2019 at 10:41:40 PM UTC-7, peteolcott wrote:
> etcetera
> 
> One of the hallmarks of a crank is being the
> author of nearly all of the posts in a thread.
> 

What if I am a crank and I am correct?

-- 
Copyright 2019 Pete Olcott All rights reserved

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

[toc] | [prev] | [next] | [standalone]

#143551

On Wednesday, 1 May 2019 06:51:26 UTC+1, peteolcott  wrote:
> On 4/30/2019 1:06 PM, bert wrote:
> > On Tuesday, 30 April 2019 18:02:32 UTC+1, peteolcott  wrote:
> >>>> On Monday, April 29, 2019 at 10:41:40 PM UTC-7, peteolcott wrote:
> > etcetera
> > 
> > One of the hallmarks of a crank is being the
> > author of nearly all of the posts in a thread.
> 
> What if I am a crank and I am correct?

Then other distribution and publicity routes 
would be more appropriate for your theories.

[toc] | [prev] | [next] | [standalone]

#143552

On 5/1/2019 5:21 AM, bert wrote:
> On Wednesday, 1 May 2019 06:51:26 UTC+1, peteolcott  wrote:
>> On 4/30/2019 1:06 PM, bert wrote:
>>> On Tuesday, 30 April 2019 18:02:32 UTC+1, peteolcott  wrote:
>>>>>> On Monday, April 29, 2019 at 10:41:40 PM UTC-7, peteolcott wrote:
>>> etcetera
>>>
>>> One of the hallmarks of a crank is being the
>>> author of nearly all of the posts in a thread.
>>
>> What if I am a crank and I am correct?
> 
> Then other distribution and publicity routes
> would be more appropriate for your theories.
> 

I have to first get someone to consider the possibility that I am correct
so that they can test my actual reasoning and thus prove that I am correct.
Because my result is unbelievable I am simply dismissed out-of-hand.

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

If we simply construe Axioms as expressions of language having
the semantic property of Boolean true this would anchor the syntax
of formal proofs to the semantics of Boolean values.

Now we have: [Deductively Sound Formal Proofs] True(x) ↔ (⊢x)
[a connected sequence of inference from axioms to a true consequence].
AKA the same universal truth predicate that Tarski "proved" was impossible.

he 1936 Tarski Undefinability Proof
http://liarparadox.org/Tarski_Proof_275_276.pdf

-- 
Copyright 2019 Pete Olcott All rights reserved

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

[toc] | [prev] | [next] | [standalone]

#143554

On 5/1/2019 7:53 AM, Pascal J. Bourguignon wrote:
> peteolcott <Here@Home> writes:
> 
>> On 5/1/2019 5:21 AM, bert wrote:
>>> On Wednesday, 1 May 2019 06:51:26 UTC+1, peteolcott  wrote:
>>>> On 4/30/2019 1:06 PM, bert wrote:
>>>>> On Tuesday, 30 April 2019 18:02:32 UTC+1, peteolcott  wrote:
>>>>>>>> On Monday, April 29, 2019 at 10:41:40 PM UTC-7, peteolcott wrote:
>>>>> etcetera
>>>>>
>>>>> One of the hallmarks of a crank is being the
>>>>> author of nearly all of the posts in a thread.
>>>>
>>>> What if I am a crank and I am correct?
>>>
>>> Then other distribution and publicity routes
>>> would be more appropriate for your theories.
>>>
>>
>> I have to first get someone to consider the possibility that I am correct
>> so that they can test my actual reasoning and thus prove that I am correct.
>> Because my result is unbelievable I am simply dismissed out-of-hand.
> 
> Or you could show us a non-trivial formal system that is both consistent
> and complete.
> 

I just did and you trimmed it from your reply.
Go back to my message and analyze the part that you trimmed point-by-point.

-- 
Copyright 2019 Pete Olcott All rights reserved

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

[toc] | [prev] | [next] | [standalone]

#143558

On 5/1/2019 11:37 AM, Pascal J. Bourguignon wrote:
> peteolcott <Here@Home> writes:
> 
>> On 5/1/2019 7:53 AM, Pascal J. Bourguignon wrote:
>>> peteolcott <Here@Home> writes:
>>>
>>>> On 5/1/2019 5:21 AM, bert wrote:
>>>>> On Wednesday, 1 May 2019 06:51:26 UTC+1, peteolcott  wrote:
>>>>>> On 4/30/2019 1:06 PM, bert wrote:
>>>>>>> On Tuesday, 30 April 2019 18:02:32 UTC+1, peteolcott  wrote:
>>>>>>>>>> On Monday, April 29, 2019 at 10:41:40 PM UTC-7, peteolcott wrote:
>>>>>>> etcetera
>>>>>>>
>>>>>>> One of the hallmarks of a crank is being the
>>>>>>> author of nearly all of the posts in a thread.
>>>>>>
>>>>>> What if I am a crank and I am correct?
>>>>>
>>>>> Then other distribution and publicity routes
>>>>> would be more appropriate for your theories.
>>>>>
>>>>
>>>> I have to first get someone to consider the possibility that I am correct
>>>> so that they can test my actual reasoning and thus prove that I am correct.
>>>> Because my result is unbelievable I am simply dismissed out-of-hand.
>>>
>>> Or you could show us a non-trivial formal system that is both consistent
>>> and complete.
>>>
>>
>> I just did and you trimmed it from your reply.
>> Go back to my message and analyze the part that you trimmed point-by-point.
> 
> Well, if I trimmed it, it was trivial…
> Could I have missed arithmetic?
> 

That is exactly what I mean by dismissed out-of-hand

If Axioms are defined as expressions of language having the
semantic property of Boolean true then this: True(x) ↔ (⊢x)
is the universal truth predicate that Tarski "proved" was impossible.





-- 
Copyright 2019 Pete Olcott All rights reserved

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

[toc] | [prev] | [next] | [standalone]

#143556

peteolcott <Here@Home> writes:
[...]

One last try.

Pete, as far as I can tell you have written nothing relevant to
C, C++, or Lisp.  Please stop posting in comp.lang.{c,c++,lisp}.
(I would have emailed you if you had provided a valid email address.)

I do not intend to post again in this thread.

-- 
Keith Thompson (The_Other_Keith) kst-u@mib.org  <http://www.ghoti.net/~kst>
Will write code for food.
void Void(void) { Void(); } /* The recursive call of the void */

[toc] | [prev] | [next] | [standalone]

#143557

Am 01.05.2019 um 19:48 schrieb Keith Thompson:
> peteolcott <Here@Home> writes:
> [...]
> 
> One last try.
> 
> Pete, as far as I can tell you have written nothing relevant to
> C, C++, or Lisp.  Please stop posting in comp.lang.{c,c++,lisp}.
> (I would have emailed you if you had provided a valid email address.)
> I do not intend to post again in this thread.

Look at this thread - he seems to be manic.
Arguing is a waste of time here.

[toc] | [prev] | [next] | [standalone]

#143560 — Re: Eliminating Undecidability and Incompleteness in Formal Systems (HP Proof refutation)

On 5/1/2019 1:25 PM, Bonita Montero wrote:
> Am 01.05.2019 um 19:48 schrieb Keith Thompson:
>> peteolcott <Here@Home> writes:
>> [...]
>>
>> One last try.
>>
>> Pete, as far as I can tell you have written nothing relevant to
>> C, C++, or Lisp.  Please stop posting in comp.lang.{c,c++,lisp}.
>> (I would have emailed you if you had provided a valid email address.)
>> I do not intend to post again in this thread.
> 
> Look at this thread - he seems to be manic.
> Arguing is a waste of time here.
> 

I check each group individually. If respondent were to trim
the other group form their response I would have beet feedback
regrading which groups are relevant.

Although I am not manic I am very excited that I completed
my 22 year 12,000 hour research project with a formalization
of the the notion of True, thus refuting Tarski:

If Axioms are defined as expressions of language having the
semantic property of Boolean true then this: True(x) ↔ (⊢x)
is the universal truth predicate that Tarski "proved" was impossible.

=====================================================================
The Refutation of Peter Linz Halting Problem Proof is complete.
This refutation applies to the other conventional (self-referential) Halting
Problem proofs. This algorithm was completed December 13th 2018 7:00PM

Peter Linz Halting Problem Proof (1993) with Turing Machines H and Ĥ.
http://liarparadox.org/Peter_Linz_HP(Pages_318-319).pdf

Every detail of the design of virtual machines implementing the Peter
Linz H deciding halting for the Peter Linz input pair: (Ĥ, Ĥ) is complete.

The only step remaining is the C++ encoding of the UTM that executes
these virtual machine descriptions.

When this last step is complete I will provide the full execution trace
of H actually deciding halting for input pair: (Ĥ, Ĥ).

The only reason that this is possible is a key undiscovered detail that
no one noticed for 81 years.

-- 
Copyright 2019 Pete Olcott All rights reserved

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

[toc] | [prev] | [next] | [standalone]

#143559

On 5/1/2019 12:48 PM, Keith Thompson wrote:
> peteolcott <Here@Home> writes:
> [...]
> 
> One last try.
> 
> Pete, as far as I can tell you have written nothing relevant to
> C, C++, or Lisp.  Please stop posting in comp.lang.{c,c++,lisp}.
> (I would have emailed you if you had provided a valid email address.)
> 
> I do not intend to post again in this thread.
> 

You have been proven to be incorrect in that people continue to
respond. It is most relevant to Prolog, it is next most relevant
to Lisp because Lisp is an AI language. I might drop C++, and C
off the list of cross-posts.

If Axioms are defined as expressions of language having the
semantic property of Boolean true then this: True(x) ↔ (⊢x)
is the universal truth predicate that Tarski "proved" was impossible.


-- 
Copyright 2019 Pete Olcott All rights reserved

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

[toc] | [prev] | [next] | [standalone]

#143563

On 01/05/2019 21:01, peteolcott wrote:
> On 5/1/2019 12:48 PM, Keith Thompson wrote:
>> peteolcott <Here@Home> writes:
>> [...]
>>
>> One last try.
>>
>> Pete, as far as I can tell you have written nothing relevant to
>> C, C++, or Lisp.  Please stop posting in comp.lang.{c,c++,lisp}.
>> (I would have emailed you if you had provided a valid email address.)
>>
>> I do not intend to post again in this thread.
>>
> 
> You have been proven to be incorrect in that people continue to
> respond. It is most relevant to Prolog, it is next most relevant
> to Lisp because Lisp is an AI language. I might drop C++, and C
> off the list of cross-posts.
> 

Please do drop C and C++ groups.  I can't answer for prolog or lisp 
groups, as I do not follow these.  But I note that everyone else in your 
threads - baring those like me who are complaining - has dropped the C 
and C++ groups.  Thus all we see are endless posts from you, apparently 
replying to yourself, and with no content of any interest to our groups. 
  It may be that you have discovered some important result in formal 
systems, but we in the C and C++ groups are not interested.  (If anyone 
from these groups disagrees with me, please say so.)

[toc] | [prev] | [next] | [standalone]

#143564

On 5/1/2019 4:28 PM, David Brown wrote:
> On 01/05/2019 21:01, peteolcott wrote:
>> On 5/1/2019 12:48 PM, Keith Thompson wrote:
>>> peteolcott <Here@Home> writes:
>>> [...]
>>>
>>> One last try.
>>>
>>> Pete, as far as I can tell you have written nothing relevant to
>>> C, C++, or Lisp.  Please stop posting in comp.lang.{c,c++,lisp}.
>>> (I would have emailed you if you had provided a valid email address.)
>>>
>>> I do not intend to post again in this thread.
>>>
>>
>> You have been proven to be incorrect in that people continue to
>> respond. It is most relevant to Prolog, it is next most relevant
>> to Lisp because Lisp is an AI language. I might drop C++, and C
>> off the list of cross-posts.
>>
> 
> Please do drop C and C++ groups.  I can't answer for prolog or lisp groups, as I do not follow these.  But I note that everyone else in your threads - baring those like me who are complaining - has dropped the C and C++ groups.  Thus all we see are endless 
> posts from you, apparently replying to yourself, and with no content of any interest to our groups.  It may be that you have discovered some important result in formal systems, but we in the C and C++ groups are not interested.  (If anyone from these 
> groups disagrees with me, please say so.)
> 
> 

I used to talk about this on comp.theory and then comp.theory died:

The Refutation of Peter Linz Halting Problem Proof is complete.
This refutation applies to the other conventional (self-referential) Halting
Problem proofs. This algorithm was completed December 13th 2018 7:00PM

Peter Linz Halting Problem Proof (1993) with Turing Machines H and Ĥ.
http://liarparadox.org/Peter_Linz_HP(Pages_318-319).pdf

Every detail of the encoding of virtual machines implementing the Peter
Linz H deciding halting for the Peter Linz input pair: (Ĥ, Ĥ) is complete.

The only step remaining is the C++ encoding of the UTM that executes
these virtual machine descriptions.

When this last step is complete I will provide the full execution trace
of H actually deciding halting for input pair: (Ĥ, Ĥ).

The only reason that this is possible is a key undiscovered detail that
no one noticed for 81 more than eight decades.





-- 
Copyright 2019 Pete Olcott All rights reserved

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

[toc] | [prev] | [next] | [standalone]

#143565

On 01/05/2019 23:44, peteolcott wrote:
> On 5/1/2019 4:28 PM, David Brown wrote:
>> On 01/05/2019 21:01, peteolcott wrote:
>>> On 5/1/2019 12:48 PM, Keith Thompson wrote:
>>>> peteolcott <Here@Home> writes:
>>>> [...]
>>>>
>>>> One last try.
>>>>
>>>> Pete, as far as I can tell you have written nothing relevant to
>>>> C, C++, or Lisp.  Please stop posting in comp.lang.{c,c++,lisp}.
>>>> (I would have emailed you if you had provided a valid email address.)
>>>>
>>>> I do not intend to post again in this thread.
>>>>
>>>
>>> You have been proven to be incorrect in that people continue to
>>> respond. It is most relevant to Prolog, it is next most relevant
>>> to Lisp because Lisp is an AI language. I might drop C++, and C
>>> off the list of cross-posts.
>>>
>>
>> Please do drop C and C++ groups.  I can't answer for prolog or lisp 
>> groups, as I do not follow these.  But I note that everyone else in 
>> your threads - baring those like me who are complaining - has dropped 
>> the C and C++ groups.  Thus all we see are endless posts from you, 
>> apparently replying to yourself, and with no content of any interest 
>> to our groups.  It may be that you have discovered some important 
>> result in formal systems, but we in the C and C++ groups are not 
>> interested.  (If anyone from these groups disagrees with me, please 
>> say so.)
>>
>>
> 
> I used to talk about this on comp.theory and then comp.theory died:
> 

Why am I not surprised?  Posters like you kill groups.

If you ever get as far as working on a C++ implementation and want to 
discuss coding details, come back here.  Until then, please stay out of 
irrelevant groups.

[toc] | [prev] | [next] | [standalone]

#143566

On Thursday, 2 May 2019 08:19:56 UTC+1, David Brown  wrote:
> On 01/05/2019 23:44, peteolcott wrote:
> > On 5/1/2019 4:28 PM, David Brown wrote:
> >> On 01/05/2019 21:01, peteolcott wrote:
> >>> On 5/1/2019 12:48 PM, Keith Thompson wrote:
> >>>> peteolcott <Here@Home> writes:
> >>>> [...]
> >>>>
> >>>> One last try.
> >>>>
> >>>> Pete, as far as I can tell you have written nothing relevant to
> >>>> C, C++, or Lisp.  Please stop posting in comp.lang.{c,c++,lisp}.
> >>>> (I would have emailed you if you had provided a valid email address.)
> >>>>
> >>>> I do not intend to post again in this thread.
> >>>>
> >>>
> >>> You have been proven to be incorrect in that people continue to
> >>> respond. It is most relevant to Prolog, it is next most relevant
> >>> to Lisp because Lisp is an AI language. I might drop C++, and C
> >>> off the list of cross-posts.
> >>>
> >>
> >> Please do drop C and C++ groups.  I can't answer for prolog or lisp 
> >> groups, as I do not follow these.  But I note that everyone else in 
> >> your threads - baring those like me who are complaining - has dropped 
> >> the C and C++ groups.  Thus all we see are endless posts from you, 
> >> apparently replying to yourself, and with no content of any interest 
> >> to our groups.  It may be that you have discovered some important 
> >> result in formal systems, but we in the C and C++ groups are not 
> >> interested.  (If anyone from these groups disagrees with me, please 
> >> say so.)
> >>
> >>
> > 
> > I used to talk about this on comp.theory and then comp.theory died:
> > 
> 
> Why am I not surprised?  Posters like you kill groups.
> 
> If you ever get as far as working on a C++ implementation and want to 
> discuss coding details, come back here.  Until then, please stay out of 
> irrelevant groups.

I'm afraid that in the same way as Christianity is relevant everywhere for
Rick, and Fir's posts fulfill the role that a blog would fulfill for a sane
person, Mr Olcott sees his babblings about his pet theory as relevant 
everywhere. As with Rick and Fir, there's little value in engaging with
him.

As we can't take off and nuke from orbit, I suggest that those of us who 
can do so might deploy suitable killfiles.

[toc] | [prev] | [next] | [standalone]

#143573

mark.bluemel@gmail.com writes:

[...]

> I'm afraid that in the same way as Christianity is relevant
> everywhere for <person X>, and <person Y>'s posts fulfill the role
> that a blog would fulfill for a sane person, <person Z> sees his
> babblings about his pet theory as relevant everywhere.  As with
> <X> and <Y>, there's little value in engaging with <Z>.

I would say that more strongly:  there is negative value in engaging
with such people, not only for them but for the group in general,
and I would be much obliged if the I've-got-to-have-the-last-word
responders would just stop responding in the first place.  And, dare
I say it, ESPECIALLY if the posting is off-topic for the newsgroup.

[toc] | [prev] | [next] | [standalone]

#143570

On 5/2/2019 2:19 AM, David Brown wrote:
> On 01/05/2019 23:44, peteolcott wrote:
>> On 5/1/2019 4:28 PM, David Brown wrote:
>>> On 01/05/2019 21:01, peteolcott wrote:
>>>> On 5/1/2019 12:48 PM, Keith Thompson wrote:
>>>>> peteolcott <Here@Home> writes:
>>>>> [...]
>>>>>
>>>>> One last try.
>>>>>
>>>>> Pete, as far as I can tell you have written nothing relevant to
>>>>> C, C++, or Lisp.  Please stop posting in comp.lang.{c,c++,lisp}.
>>>>> (I would have emailed you if you had provided a valid email address.)
>>>>>
>>>>> I do not intend to post again in this thread.
>>>>>
>>>>
>>>> You have been proven to be incorrect in that people continue to
>>>> respond. It is most relevant to Prolog, it is next most relevant
>>>> to Lisp because Lisp is an AI language. I might drop C++, and C
>>>> off the list of cross-posts.
>>>>
>>>
>>> Please do drop C and C++ groups.  I can't answer for prolog or lisp groups, as I do not follow these.  But I note that everyone else in your threads - baring those like me who are complaining - has dropped the C and C++ groups.  Thus all we see are 
>>> endless posts from you, apparently replying to yourself, and with no content of any interest to our groups.  It may be that you have discovered some important result in formal systems, but we in the C and C++ groups are not interested.  (If anyone from 
>>> these groups disagrees with me, please say so.)
>>>
>>>
>>
>> I used to talk about this on comp.theory and then comp.theory died:
>>
> 
> Why am I not surprised?  Posters like you kill groups.
> 
> If you ever get as far as working on a C++ implementation and want to discuss coding details, come back here.  Until then, please stay out of irrelevant groups.
> 
> 

I only come here because the more relevant groups died.

-- 
Copyright 2019 Pete Olcott All rights reserved

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

[toc] | [prev] | [next] | [standalone]

#143562

On 5/1/2019 12:48 PM, Keith Thompson wrote:
> peteolcott <Here@Home> writes:
> [...]
> 
> One last try.
> 
> Pete, as far as I can tell you have written nothing relevant to
> C, C++, or Lisp.  Please stop posting in comp.lang.{c,c++,lisp}.
> (I would have emailed you if you had provided a valid email address.)
> 
> I do not intend to post again in this thread.
> 

The Refutation of Peter Linz Halting Problem Proof is complete.
This refutation applies to the other conventional (self-referential) Halting
Problem proofs. This algorithm was completed December 13th 2018 7:00PM

Peter Linz Halting Problem Proof (1993) with Turing Machines H and Ĥ.
http://liarparadox.org/Peter_Linz_HP(Pages_318-319).pdf

Every detail of the encoding of virtual machines implementing the Peter
Linz H deciding halting for the Peter Linz input pair: (Ĥ, Ĥ) is complete.

The only step remaining is the C++ encoding of the UTM that executes
these virtual machine descriptions.

When this last step is complete I will provide the full execution trace
of H actually deciding halting for input pair: (Ĥ, Ĥ).

The only reason that this is possible is a key undiscovered detail that
no one noticed for 81 more than eight decades.

-- 
Copyright 2019 Pete Olcott All rights reserved

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

[toc] | [prev] | [next] | [standalone]

#143532

On 4/29/2019 4:53 PM, paul wallich wrote:
> On 4/27/19 7:12 PM, Jeff Barnett wrote:
>> Paul Rubin wrote on 4/27/2019 3:52 PM:
>>> peteolcott <Here@Home> writes:
>>>> I have spent 22 years and 12,000 hours on this.
>>>
>>> http://web.mst.edu/%7Elmhall/WhatToDoWhenTrisectorComes.pdf
>>
>> Thanks for the pointer. It seems I missed that article - it came in a crack between regularly reading the Intelligencer in the USC/ISI library where I was employed and starting my own subscription which I kept for two decades. The Intelligencer went from 
>> wildly entertaining to hard to read during the latter period. The article by Dudley has a wider appeal today than when he wrote it in 1983; we have lots of computer systems to shield cranks and save then postage.
>>
>> PO fits the article's profile to a tee: he claims to be in his 60's, to have spent thousands of hours, keeps cleaning and pushing the same mistakes over and over again, and is basically a very poor mathematician who believes that PROLOG represents real 
>> and deep logic systems. I have been leaning towards troll rather than ignoramus but the article gives me a third choice: trisector! I'll keep it in mind.
>>
>> The thing I find interesting is that most people, including me, find it so hard to not respond to his gibberish. The first reaction is to help a lost soul back onto the path of truth (caps?) while the second reaction is mostly a reaction to a hard 
>> challenge like trying to stare down a lizard.
> 
> I think that the problem isn't trisection exactly but rather a sort of weird semantic capture. The term "unsound" is used to tag the category "neither provable nor refutable" but that's -- within the system -- just a tag. The logical system, such as it is, 
> would work just as well if the tag were "NPNR" or "frabjous" or "charmed" or "boogabooga". But use the tag "unsound", and magically all of the senses of "unsound" from colloguial language and other logical systems suddenly get dragged in and pasted over 
> the top of what might as well be "frabjous".
> 
> Do some brains need better macro systems?

Sound deductive inference
(a) All dogs are mammals
(b) All mammals breath
(c) Therefore all dogs breath

Unsound deductive inference (false premise)
(a) All dogs are office buildings
(b) All office buildings have windows
(c) Therefore all dogs have windows

Unsound deductive inference (invalid inference)
(a) All dogs are mammals
(b) All fish swim
(c) Therefore all dogs breath


-- 
Copyright 2019 Pete Olcott All rights reserved

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

[toc] | [prev] | [next] | [standalone]

Page 2 of 3 — ← Prev page 1 [2] 3  Next page →

Back to top | Article view | comp.lang.c

csiph-web