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

Groups > comp.lang.lisp > #32764 > unrolled thread

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

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

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) paul wallich <pw@panix.com> - 2019-04-26 13:40 -0400
          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) Siebe de Vos <siebe@de-vos.de> - 2019-04-26 17:24 +0200
      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:10 -0500
          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) Paul Rubin <no.email@nospam.invalid> - 2019-04-27 14:44 -0700
                    Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) Kaz Kylheku <847-115-0292@kylheku.com> - 2019-04-28 03:40 +0000
                  Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-04-27 16:48 -0500
                    Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) Paul Rubin <no.email@nospam.invalid> - 2019-04-27 14:52 -0700
                      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) Jeff Barnett <jbb@notatt.com> - 2019-04-27 17:12 -0600
                        Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-04-27 18:41 -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) Paul Rubin <no.email@nospam.invalid> - 2019-04-27 17:10 -0700
                          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) Jeff Barnett <jbb@notatt.com> - 2019-04-27 19:26 -0600
                            Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) Paul Rubin <no.email@nospam.invalid> - 2019-04-27 18:52 -0700
                              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) "Pascal J. Bourguignon" <pjb@informatimago.com> - 2019-04-30 07:08 +0200
                                    Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-04-30 00:41 -0500
                                      Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) taruss@google.com - 2019-04-30 09:23 -0700
                                        Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) "Pascal J. Bourguignon" <pjb@informatimago.com> - 2019-04-30 18:47 +0200
                                          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) peteolcott <Here@Home> - 2019-05-01 07:50 -0500
                                              Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) "Pascal J. Bourguignon" <pjb@informatimago.com> - 2019-05-01 14:53 +0200
                                                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) "Pascal J. Bourguignon" <pjb@informatimago.com> - 2019-05-01 18:37 +0200
                                                    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) peteolcott <Here@Home> - 2019-05-01 13:56 -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 15:14 -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-27 21:28 -0500
                            Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-05-01 15:12 -0500
                          Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-05-01 15:12 -0500
                        Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) Spiros Bousbouras <spibou@gmail.com> - 2019-04-28 00:16 +0000
                          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) paul wallich <pw@panix.com> - 2019-04-29 17:53 -0400
                          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) luserdroog <mijoryx@yahoo.com> - 2019-04-29 17:22 -0700
                              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) Kaz Kylheku <847-115-0292@kylheku.com> - 2019-04-30 00:18 +0000
                          Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) Paul Rubin <no.email@nospam.invalid> - 2019-04-29 18:11 -0700
                          Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-04-29 21:58 -0500
                      Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) Stefan Monnier <monnier@iro.umontreal.ca> - 2019-05-02 15:11 -0400
                        Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) Jeff Barnett <jbb@notatt.com> - 2019-05-02 16:46 -0600
                          Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) Kaz Kylheku <847-115-0292@kylheku.com> - 2019-05-02 23:21 +0000
                            Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-05-02 22:04 -0500
                            Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) Jeff Barnett <jbb@notatt.com> - 2019-05-02 21:13 -0600
                              Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-05-02 22:42 -0500
                                Re: Eliminating Undecidability and Incompleteness in Formal Systems (Halting Problem) peteolcott <Here@Home> - 2019-05-02 22:46 -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:13 -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:49 -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
    Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) Rabican <gavinschuette@gmail.com> - 2019-05-06 05:51 -0700

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

#32832 — 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]

#32831

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]

#32838

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]

#32837

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]

#32817

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]

#32795

On 4/27/2019 8:26 PM, Jeff Barnett wrote:
> Paul Rubin wrote on 4/27/2019 6:10 PM:
>> Jeff Barnett <jbb@notatt.com> writes:
>>> believes that PROLOG represents real and deep logic systems.
>>
>> I don't know Prolog but have been wondering what kind of logic it uses.
>> I.e. I thought that it basically solves constraint satisfaction problems
>> in what amounts to propositional logic.  That is in fact a decidable
>> system, but it's a very weak one, being unable to express propositions
>> about arithmetic.  Can one write the twin prime conjecture in Prolog?
> 
> Probably not. I haven't looked at PROLOG for a while but for at least the first decade of its existence it only allowed Horn clauses - pretty week stuff. It basically was like some of the old AI by-rule systems with a vanilla execution engine. With Horn 
> clauses you could not imply a negative nor could anything be implied by a negative. Total toy.
> 
>> OTOH, the OP says propositions are true (provable), false (the negation
>> is provable), or unsound.  If "unsound" just means "unprovable in the
>> given theory", then fine, that's what I'm used to.  Maybe he adds a
>> philosophical claim that the statement then doesn't have a truth value,
>> so there is no such thing as an intended model.  I can live with that,
>> but the terminology is so weird and vague as to not have much meaning.
> 
> Don't assume the OP aka PO knows anything of which he speaks. 

I proved that I did know and the guy the you responding to understood
me completely.  Quit being a jackass ?

You can act like such a dumb bunny.
I was going to say that you ARE a dumb bunny yet since
that is not true I had to refrain. From past conversations
I think that you may have proved to be smart.

> His math, logic, and programming skills are pathetic. His abilities to concentrate and check what he is saying are non existent. That is why he can publish a half dozen versions of the same 
> gibberish, trying to correct minor issues, in a single day. In anther area, he would be accused of premature ejaculation and sent to a urologist for a consultation. I think the current issues need a psychiatrist prescribing meds.
> 
>> OP, please read a logic book and use standard terminology if you want
>> anyone to understand you.  I liked Enderton's "A Mathematical
>> Introduction to Logic" though it might be considered old-fashioned by
>> onw.
> 
> High school books would be a great help but, then, he'd think we'd think he's a dumb bunny. Some of us think that anyway.


-- 
Copyright 2019 Pete Olcott All rights reserved

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

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

#32836

On 4/27/2019 8:26 PM, Jeff Barnett wrote:
> Paul Rubin wrote on 4/27/2019 6:10 PM:
>> Jeff Barnett <jbb@notatt.com> writes:
>>> believes that PROLOG represents real and deep logic systems.
>>
>> I don't know Prolog but have been wondering what kind of logic it uses.
>> I.e. I thought that it basically solves constraint satisfaction problems
>> in what amounts to propositional logic.  That is in fact a decidable
>> system, but it's a very weak one, being unable to express propositions
>> about arithmetic.  Can one write the twin prime conjecture in Prolog?
> 
> Probably not. I haven't looked at PROLOG for a while but for at least the first decade of its existence it only allowed Horn clauses - pretty week stuff. It basically was like some of the old AI by-rule systems with a vanilla execution engine. With Horn 
> clauses you could not imply a negative nor could anything be implied by a negative. Total toy.
> 
>> OTOH, the OP says propositions are true (provable), false (the negation
>> is provable), or unsound.  If "unsound" just means "unprovable in the
>> given theory", then fine, that's what I'm used to.  Maybe he adds a
>> philosophical claim that the statement then doesn't have a truth value,
>> so there is no such thing as an intended model.  I can live with that,
>> but the terminology is so weird and vague as to not have much meaning.
> 

[Deductively Sound Formal Proofs]
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]

#32835

On 4/27/2019 7:10 PM, Paul Rubin wrote:
> Jeff Barnett <jbb@notatt.com> writes:
>> believes that PROLOG represents real and deep logic systems.
> 
> I don't know Prolog but have been wondering what kind of logic it uses.
> I.e. I thought that it basically solves constraint satisfaction problems
> in what amounts to propositional logic.  That is in fact a decidable
> system, but it's a very weak one, being unable to express propositions
> about arithmetic.  Can one write the twin prime conjecture in Prolog?
> 
> OTOH, the OP says propositions are true (provable), false (the negation
> is provable), or unsound.  If "unsound" just means "unprovable in the
> given theory", then fine, that's what I'm used to.  Maybe he adds a
> philosophical claim that the statement then doesn't have a truth value,
> so there is no such thing as an intended model.  I can live with that,
> but the terminology is so weird and vague as to not have much meaning.
> 
> OP, please read a logic book and use standard terminology if you want
> anyone to understand you.  I liked Enderton's "A Mathematical
> Introduction to Logic" though it might be considered old-fashioned by
> onw.
> 

[Deductively Sound Formal Proofs]
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]

#32790

On Sat, 27 Apr 2019 17:12:45 -0600
Jeff Barnett <jbb@notatt.com> 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.

Dudley has written a whole book on the subject , "A budget of trisections".

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

#32792

On 4/27/2019 7:16 PM, Spiros Bousbouras wrote:
> On Sat, 27 Apr 2019 17:12:45 -0600
> Jeff Barnett <jbb@notatt.com> 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.
> 
> Dudley has written a whole book on the subject , "A budget of trisections".
> 

The huge difference in this case is that deriving a complete and consistent
formulation of the notion of True finally anchors Truth Conditional Semantics.
https://en.wikipedia.org/wiki/Truth-conditional_semantics



-- 
Copyright 2019 Pete Olcott All rights reserved

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

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

#32803

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?

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

#32804

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]

#32806

On Monday, April 29, 2019 at 6:43:11 PM UTC-5, peteolcott wrote:

> 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
> 
> 

Nit: the verb is "breathe", breath is the noun as in
"dog's have bad breath."

This looks almost like Aristotle's syllogisms. These
were treated in a very interesting book by Lukasiewicz.

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

#32810

On 4/29/2019 7:22 PM, luserdroog 0wrote:
> On Monday, April 29, 2019 at 6:43:11 PM UTC-5, peteolcott wrote:
> 
>> 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
>>
>>
> 
> Nit: the verb is "breathe", breath is the noun as in
> "dog's have bad breath."
> 
> This looks almost like Aristotle's syllogisms. These
> were treated in a very interesting book by Lukasiewicz.
> 

The only reason that incompleteness is provable is that the formal
proofs of symbolic logic diverge from that simple pattern.

Summing it up:
True(X) is Provable(X) from True Premises.
False(X) is Provable(¬X) from True Premises.
Otherwise Unsound(X).

Technically {Unsound} only applies to arguments and not to single
expressions of language I had to extend the meaning of the term
{Unsound} when I applied the concept of soundness to formal proofs.

-- 
Copyright 2019 Pete Olcott All rights reserved

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

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

#32805

On 2019-04-27, Jeff Barnett <jbb@notatt.com> wrote:
>> 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 

I'm familiar with this. I think it came up with some Peter Olcott
threads before.

I think Peter Olcott may in fact have subconsciously (or consciously)
pulled that 12,000 hour figure from the above article. It is not a
coincidence.

Quote from "What To Do when the Trisector Comes"

] The trisector will leave, but he will be back with a revised proof,
] longer, more complicated, and with the error harder to find.

(Absolutely no danger of that here; just basically the same stuff in
circles. "I didn't understand a word of your objections; here is the
same stuff rephrased.")

What I didn't know (TIL) is that Dudley became as obsessed with these
cranks as they themselves are with trisecting. In 1996 he wrote a book,
_The Trisectors_.

https://en.wikipedia.org/wiki/Underwood_Dudley

By the way, I think trisecting is in fact possible. Well, at least
as a continous process that converges to 1/3.  The reason is that 1/3 is
very clean continued fraction in binary: #b0.0101010101..  In other
words, the simple and easy to remember series: 1/4 + 1/16 + 1/64
+ 1/256 ...

We can certainly bisect angles, which means that we can repeatedly
bisect the original angle to obtain power of two subdivisions, and
follow the above series to pick out an approximation that will get as
close to 1/3 as physical error that the execution of method and its
tools will allow. By the time you're doing 1/1024, you have three digits
of precision in there; more than enough for most applications. (Which
are, what? ...)

If Trisector came knocking, I might just hand him this.

-- 
TXR Programming Lanuage: http://nongnu.org/txr
Music DIY Mailing List:  http://www.kylheku.com/diy
ADA MP-1 Mailing List:   http://www.kylheku.com/mp1

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

#32807

Kaz Kylheku <847-115-0292@kylheku.com> writes:
> By the way, I think trisecting is in fact possible.

Exact trisection is possible if you have a ruler rather than just a
straightedge.  The difference is that a ruler has marks on it (say an
inch apart) while a straightedge has no marks.  See:

https://en.wikipedia.org/wiki/Neusis_construction

> 1/3 is very clean continued fraction in binary: #b0.0101010101..

That's a repeating decimal except in base 2 ;-).  A continued fraction
is something different:

https://en.wikipedia.org/wiki/Continued_fraction

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

#32809

On 4/29/2019 7:18 PM, Kaz Kylheku wrote:
> On 2019-04-27, Jeff Barnett <jbb@notatt.com> wrote:
>>> 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
> 
> I'm familiar with this. I think it came up with some Peter Olcott
> threads before.
> 
> I think Peter Olcott may in fact have subconsciously (or consciously)
> pulled that 12,000 hour figure from the above article. It is not a
> coincidence.
> 
No I counted the total USENET posts with every variation of my name in a key
group and estimated time per post. It was 12,000 posts sine 2004 with 1/2
hour per post and 1/2 hour of prep time per post.


-- 
Copyright 2019 Pete Olcott All rights reserved

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

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

#32843

>> I have spent 22 years and 12,000 hours on this.
> http://web.mst.edu/%7Elmhall/WhatToDoWhenTrisectorComes.pdf

OK, I'll bite: how do we do the equivalent of showing a "computer
printout giving the errors in the construction for angles of various
sizes"?


        Stefan

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

#32844

Stefan Monnier wrote on 5/2/2019 1:11 PM:
>>> I have spent 22 years and 12,000 hours on this.
>> http://web.mst.edu/%7Elmhall/WhatToDoWhenTrisectorComes.pdf
> 
> OK, I'll bite: how do we do the equivalent of showing a "computer
> printout giving the errors in the construction for angles of various
> sizes"?

Steps in a construction are representable by an algebraic formula. These 
formulas can be evaluated for specific sets of values (such as each 
angle between 0 and 360 degrees). The total imprecision caused by 
floating point is very small in comparison to the error when one asks 
"Is this a third of the input angle?". Of course if you were using Lisp, 
you might be able to do most things with rationals and get more exact 
answers. Dudley was just trying to show his correspondents that they 
were mistaken.
-- 
Jeff Barnett

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

#32845

On 2019-05-02, Jeff Barnett <jbb@notatt.com> wrote:
> Stefan Monnier wrote on 5/2/2019 1:11 PM:
>>>> I have spent 22 years and 12,000 hours on this.
>>> http://web.mst.edu/%7Elmhall/WhatToDoWhenTrisectorComes.pdf
>> 
>> OK, I'll bite: how do we do the equivalent of showing a "computer
>> printout giving the errors in the construction for angles of various
>> sizes"?
>
> Steps in a construction are representable by an algebraic formula. These 
> formulas can be evaluated for specific sets of values (such as each 
> angle between 0 and 360 degrees). The total imprecision caused by 
> floating point is very small in comparison to the error when one asks 
> "Is this a third of the input angle?". Of course if you were using Lisp, 
> you might be able to do most things with rationals and get more exact 
> answers. Dudley was just trying to show his correspondents that they 
> were mistaken.

I suspect Stefan might mean "how do we do the equivalent of ... in this
present situation, in the domain of incompleteness and halting."

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

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

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

csiph-web