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

Groups > comp.lang.lisp > #32816

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

From "Pascal J. Bourguignon" <pjb@informatimago.com>
Newsgroups comp.lang.lisp
Subject Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this)
Date 2019-04-30 18:47 +0200
Organization Informatimago
Message-ID <m2ftpzxwxn.fsf@despina.home> (permalink)
References (16 earlier) <c3461c97-d07c-4261-8505-17c1e5704edf@googlegroups.com> <TOydnSJT068oJVrBnZ2dnUU7-dPNnZ2d@giganews.com> <m2k1fcxepj.fsf@despina.home> <wLydnVr9gKKRfVrBnZ2dnUU7-fvNnZ2d@giganews.com> <40f4acd5-de82-4b2f-94b6-b419ae5b23b6@googlegroups.com>

Show all headers | View raw

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


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

-- 
__Pascal J. Bourguignon__
http://www.informatimago.com

Back to comp.lang.lisp | Previous | Next — Previous in thread | Next in thread | Find similar | Unroll thread

Thread

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

csiph-web