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


Groups > comp.lang.prolog > #12766 > unrolled thread

Is this correct Prolog?

Started byolcott <NoOne@NoWhere.com>
First post2022-04-30 02:02 -0500
Last post2022-05-01 11:21 -0600
Articles 20 on this page of 173 — 11 participants

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


Contents

  Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-04-30 02:02 -0500
    Re: Is this correct Prolog? Mikko <mikko.levanto@iki.fi> - 2022-04-30 12:31 +0300
      Re: Is this correct Prolog? Aleksy Grabowski <hurufu@gmail.com> - 2022-04-30 20:15 +0200
        Re: Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-04-30 16:08 -0500
          Re: Is this correct Prolog? Mikko <mikko.levanto@iki.fi> - 2022-05-01 12:26 +0300
            Re: Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-05-01 06:00 -0500
              Re: Is this correct Prolog? Aleksy Grabowski <hurufu@gmail.com> - 2022-05-02 13:49 +0200
                Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-02 08:09 -0500
                  Re: Is this correct Prolog? Aleksy Grabowski <hurufu@gmail.com> - 2022-05-02 15:35 +0200
                    Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-02 08:55 -0500
                      Re: Is this correct Prolog? Aleksy Grabowski <hurufu@gmail.com> - 2022-05-02 16:28 +0200
                        Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-02 10:24 -0500
                          Re: Is this correct Prolog? Aleksy Grabowski <hurufu@gmail.com> - 2022-05-02 17:44 +0200
                            Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-02 11:04 -0500
                              Re: Is this correct Prolog? Aleksy Grabowski <hurufu@gmail.com> - 2022-05-02 18:38 +0200
                                Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-02 11:49 -0500
                                Re: Is this correct Prolog? Julio Di Egidio <julio@diegidio.name> - 2022-05-02 09:51 -0700
                                  Re: Is this correct Prolog? Aleksy Grabowski <hurufu@gmail.com> - 2022-05-02 19:38 +0200
                                    Re: Is this correct Prolog? Julio Di Egidio <julio@diegidio.name> - 2022-05-02 11:04 -0700
                                      Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-02 14:22 -0500
                                    Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-02 14:14 -0500
                                    Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-02 14:24 -0500
                                      Re: Is this correct Prolog? Aleksy Grabowski <hurufu@gmail.com> - 2022-05-02 21:43 +0200
                                        Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-02 15:10 -0500
                                          Re: Is this correct Prolog? Aleksy Grabowski <hurufu@gmail.com> - 2022-05-02 22:37 +0200
                                            Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-02 15:58 -0500
                                              Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-02 16:30 -0500
                                              Re: Is this correct Prolog? Aleksy Grabowski <hurufu@gmail.com> - 2022-05-02 23:33 +0200
                                                Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-02 16:42 -0500
                                                  Re: Is this correct Prolog? Aleksy Grabowski <hurufu@gmail.com> - 2022-05-03 00:13 +0200
                                                    Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-02 19:35 -0500
                          Re: Is this correct Prolog? Jeff Barnett <jbb@notatt.com> - 2022-05-02 11:28 -0600
                            Re: Is this correct Prolog? Mr Flibble <flibble@reddwarf.jmc> - 2022-05-02 19:41 +0100
                              Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-02 14:26 -0500
                            Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-02 14:32 -0500
                              Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-02 18:28 -0400
                                Re: Is this correct Prolog? Aleksy Grabowski <hurufu@gmail.com> - 2022-05-03 00:41 +0200
                                  Re: Is this correct Prolog? Julio Di Egidio <julio@diegidio.name> - 2022-05-02 16:00 -0700
                                    Re: Is this correct Prolog? Aleksy Grabowski <hurufu@gmail.com> - 2022-05-03 01:39 +0200
                                      Re: Is this correct Prolog? Julio Di Egidio <julio@diegidio.name> - 2022-05-02 17:26 -0700
                                  Re: Is this correct Prolog? Ben <ben.usenet@bsb.me.uk> - 2022-05-03 00:43 +0100
                                    Re: Is this correct Prolog? Julio Di Egidio <julio@diegidio.name> - 2022-05-02 17:20 -0700
                                    Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-02 19:57 -0500
                                      Re: Is this correct Prolog? Ben <ben.usenet@bsb.me.uk> - 2022-05-03 03:21 +0100
                                        Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-02 22:01 -0500
                                          Re: Is this correct Prolog? Julio Di Egidio <julio@diegidio.name> - 2022-05-03 01:18 -0700
                                          Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-03 08:05 -0400
                                            Re: Is this correct Prolog? [ Tarski ] olcott <polcott2@gmail.com> - 2022-05-04 21:30 -0500
                                              Re: Is this correct Prolog? [ Tarski ] Richard Damon <Richard@Damon-Family.org> - 2022-05-04 22:46 -0400
                                                Re: Is this correct Prolog? [ Tarski ] olcott <polcott2@gmail.com> - 2022-05-04 22:02 -0500
                                                  Re: Is this correct Prolog? [ Tarski ] Richard Damon <Richard@Damon-Family.org> - 2022-05-05 07:41 -0400
                                                Re: Is this correct Prolog? [ Tarski ] olcott <polcott2@gmail.com> - 2022-05-05 12:57 -0500
                                                  Re: Is this correct Prolog? [ Tarski ] André G. Isaak <agisaak@gm.invalid> - 2022-05-05 12:06 -0600
                                                    Re: Is this correct Prolog? [ Tarski ] olcott <polcott2@gmail.com> - 2022-05-05 16:23 -0500
                                                  Re: Is this correct Prolog? [ Tarski ] Richard Damon <Richard@Damon-Family.org> - 2022-05-05 22:24 -0400
                                                    Re: Is this correct Prolog? [ Tarski ] olcott <polcott2@gmail.com> - 2022-05-05 21:37 -0500
                                                      Re: Is this correct Prolog? [ Tarski ] Richard Damon <Richard@Damon-Family.org> - 2022-05-06 07:43 -0400
                                                        Re: Is this correct Prolog? [ Tarski ] olcott <polcott2@gmail.com> - 2022-05-06 15:29 -0500
                                          Re: Is this correct Prolog? Ben <ben.usenet@bsb.me.uk> - 2022-05-03 15:59 +0100
                                      Re: Is this correct Prolog? André G. Isaak <agisaak@gm.invalid> - 2022-05-03 09:18 -0600
                                        Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-03 11:08 -0500
                                          Re: Is this correct Prolog? André G. Isaak <agisaak@gm.invalid> - 2022-05-03 10:52 -0600
                                            Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-03 12:05 -0500
                                              Re: Is this correct Prolog? André G. Isaak <agisaak@gm.invalid> - 2022-05-03 11:17 -0600
                                                Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-03 12:33 -0500
                                                  Re: Is this correct Prolog? André G. Isaak <agisaak@gm.invalid> - 2022-05-03 12:23 -0600
                                                    Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-03 13:59 -0500
                                                      Re: Is this correct Prolog? André G. Isaak <agisaak@gm.invalid> - 2022-05-03 14:03 -0600
                                                        Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-03 22:24 -0500
                                                          Re: Is this correct Prolog? André G. Isaak <agisaak@gm.invalid> - 2022-05-03 21:54 -0600
                                                          Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-04 07:27 -0400
                                            Re: Is this correct Prolog? [ André didn't lie after all ] olcott <polcott2@gmail.com> - 2022-05-03 12:08 -0500
                                        Re: Is this correct Prolog? Jeff Barnett <jbb@notatt.com> - 2022-05-03 12:33 -0600
                                          Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-03 14:12 -0500
                                            Re: Is this correct Prolog? André G. Isaak <agisaak@gm.invalid> - 2022-05-03 13:22 -0600
                                              Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-03 21:53 -0500
                                                Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-03 23:12 -0400
                                                  Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-03 22:53 -0500
                                                  Re: Is this correct Prolog? André G. Isaak <agisaak@gm.invalid> - 2022-05-03 22:06 -0600
                                                    Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-04 01:17 -0500
                                                      Re: Is this correct Prolog? André G. Isaak <agisaak@gm.invalid> - 2022-05-04 08:02 -0600
                                                        Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-04 14:01 -0500
                                                          Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-04 19:48 -0400
                                            Re: Is this correct Prolog? Jeff Barnett <jbb@notatt.com> - 2022-05-03 15:58 -0600
                                              Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-03 17:13 -0500
                                  Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-02 19:11 -0500
                                    Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-02 19:35 -0500
                                    Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-02 20:47 -0400
                    Re: Is this correct Prolog? Julio Di Egidio <julio@diegidio.name> - 2022-05-02 07:59 -0700
                      Re: Is this correct Prolog? Aleksy Grabowski <hurufu@gmail.com> - 2022-05-02 17:15 +0200
                      Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-02 10:45 -0500
                        Re: Is this correct Prolog? Julio Di Egidio <julio@diegidio.name> - 2022-05-02 09:02 -0700
                          Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-02 11:26 -0500
        Re: Is this correct Prolog? Mikko <mikko.levanto@iki.fi> - 2022-05-01 12:24 +0300
          Re: Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-05-01 05:58 -0500
            Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-01 07:12 -0400
              Re: Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-05-01 06:45 -0500
                Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-01 08:07 -0400
                  Re: Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-05-01 07:15 -0500
                    Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-01 13:49 -0400
      Re: Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-04-30 15:48 -0500
        Re: Is this correct Prolog? Mikko <mikko.levanto@iki.fi> - 2022-05-01 12:38 +0300
          Re: Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-05-01 06:06 -0500
            Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-01 07:26 -0400
              Re: Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-05-01 06:54 -0500
                Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-01 08:11 -0400
                  Re: Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-05-01 07:19 -0500
                    Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-01 14:00 -0400
    Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-04-30 21:08 -0400
      Re: Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-04-30 20:42 -0500
        Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-04-30 22:00 -0400
          Re: Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-04-30 21:21 -0500
            Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-04-30 22:38 -0400
              Re: Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-04-30 21:56 -0500
                Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-04-30 23:11 -0400
                  Re: Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-04-30 22:15 -0500
                    Re: Is this correct Prolog? Jeff Barnett <jbb@notatt.com> - 2022-04-30 23:24 -0600
                      Re: Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-05-01 06:35 -0500
                        Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-01 13:16 -0400
                      Re: Is this correct Prolog? Mr Flibble <flibble@reddwarf.jmc> - 2022-05-01 13:19 +0100
                        Re: Is this correct Prolog? polcott <polcott2@gmail.com> - 2022-05-01 07:51 -0500
                        Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-01 13:19 -0400
                        Re: Is this correct Prolog? Jeff Barnett <jbb@notatt.com> - 2022-05-01 11:22 -0600
                    Re: Is this correct Prolog? Mikko <mikko.levanto@iki.fi> - 2022-05-01 12:45 +0300
                      Re: Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-05-01 06:28 -0500
                        Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-01 08:01 -0400
                          Re: Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-05-01 07:09 -0500
                            Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-01 08:16 -0400
                    Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-01 07:18 -0400
                      Re: Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-05-01 06:50 -0500
                        Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-01 13:26 -0400
      Re: Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-04-30 20:47 -0500
        Re: Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-04-30 23:49 -0500
          Re: Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-05-01 11:08 -0500
            Re: Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-05-01 13:28 -0500
              Re: Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-05-01 14:00 -0500
                Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-01 15:19 -0400
                Re: Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-05-01 14:32 -0500
                  Re: Is this correct Prolog? André G. Isaak <agisaak@gm.invalid> - 2022-05-01 13:44 -0600
                    Re: Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-05-01 14:48 -0500
                      Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-01 16:01 -0400
                      Re: Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-05-01 15:42 -0500
                        Re: Is this correct Prolog? André G. Isaak <agisaak@gm.invalid> - 2022-05-01 14:51 -0600
                          Re: Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-05-01 17:04 -0500
                            Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-01 18:08 -0400
                              Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-01 17:39 -0500
                                Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-01 19:18 -0400
                                  Re: Is this correct Prolog? André G. Isaak <agisaak@gm.invalid> - 2022-05-01 17:26 -0600
                                  Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-01 19:58 -0500
                                    Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-01 21:32 -0400
                                      Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-01 20:53 -0500
                                        Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-01 22:14 -0400
                                          Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-01 21:18 -0500
                                            Re: Is this correct Prolog? André G. Isaak <agisaak@gm.invalid> - 2022-05-01 20:37 -0600
                                            Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-01 22:47 -0400
                                              Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-01 22:04 -0500
                                                Re: Is this correct Prolog? André G. Isaak <agisaak@gm.invalid> - 2022-05-01 22:10 -0600
                                                Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-02 07:10 -0400
                                                  Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-02 08:19 -0500
                                                    Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-02 18:38 -0400
                            Re: Is this correct Prolog? André G. Isaak <agisaak@gm.invalid> - 2022-05-01 16:37 -0600
                              Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-01 17:44 -0500
                                Re: Is this correct Prolog? André G. Isaak <agisaak@gm.invalid> - 2022-05-01 17:15 -0600
                                  Re: Is this correct Prolog? [ André is proven to be a liar ] olcott <NoOne@NoWhere.com> - 2022-05-01 18:33 -0500
                                    Re: Is this correct Prolog? [ André is proven to be a liar ] André G. Isaak <agisaak@gm.invalid> - 2022-05-01 17:44 -0600
                                      Re: Is this correct Prolog? [ André is proven to be a liar ] olcott <NoOne@NoWhere.com> - 2022-05-01 18:53 -0500
                              Re: Is this correct Prolog? [ André is proven to be a liar ] olcott <polcott2@gmail.com> - 2022-05-01 18:15 -0500
                                Re: Is this correct Prolog? [ André is proven to be a liar ] Richard Damon <Richard@Damon-Family.org> - 2022-05-01 19:21 -0400
                                  Re: Is this correct Prolog? [ André is proven to be a liar ] olcott <polcott2@gmail.com> - 2022-05-01 19:56 -0500
                          Re: Is this correct Prolog? olcott <polcott2@gmail.com> - 2022-05-01 17:05 -0500
                        Re: Is this correct Prolog? Richard Damon <Richard@Damon-Family.org> - 2022-05-01 16:55 -0400
          Re: Is this correct Prolog? olcott <NoOne@NoWhere.com> - 2022-05-01 11:57 -0500
            Re: Is this correct Prolog? André G. Isaak <agisaak@gm.invalid> - 2022-05-01 11:21 -0600

Page 3 of 9 — ← Prev page 1 2 [3] 4 5 6 7 8 9  Next page →


#12898

FromBen <ben.usenet@bsb.me.uk>
Date2022-05-03 00:43 +0100
Message-ID<87a6bzfqkz.fsf@bsb.me.uk>
In reply to#12895
Aleksy Grabowski <hurufu@gmail.com> writes:

>> IF you are defining that your logic system is limited to what Prolog can "Prove", that is fine. Just realize that you have just defined that your 
>> logic system can't handle a lot of the real problems in the world, and in particular, it is very limited in the mathematics it can handle.
>> I am pretty sure that Prolog is NOT up to handling the logic needed to 
>> handle the mathematics needed to express Godel's G, or the Halting Problem.
>> Thus, your "Proof" that these Theorems are "Wrong" is incorrect, you 
>> have only proven that your limited logic system can't reach them in expressibility.
>
> Thanks for confirmation, that's what exactly what I was trying to tell
> to topic poster in one of my previous posts. Prolog in it's bare form
> is a bad theorem solver. It wasn't designed a such.
>
> If you want to deal with such problems maybe it is better to use Coq
> theorem prover, I've never used it by myself, but it looks like one of
> the best proving assistants out there.

And indeed there is a fully formalised proof of GIT in Coq (though I
think it's the slightly tighter Gödel-Rosser version).

-- 
Ben.

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


#12900

FromJulio Di Egidio <julio@diegidio.name>
Date2022-05-02 17:20 -0700
Message-ID<9a3b8777-9d86-405e-b6d9-02d516fbf77en@googlegroups.com>
In reply to#12898
On Tuesday, 3 May 2022 at 01:43:56 UTC+2, Ben wrote:
> Aleksy Grabowski <hur...@gmail.com> writes: 
> 
> >> IF you are defining that your logic system is limited to what Prolog can "Prove", that is fine. Just realize that you have just defined that your 
> >> logic system can't handle a lot of the real problems in the world, and in particular, it is very limited in the mathematics it can handle. 
> >> I am pretty sure that Prolog is NOT up to handling the logic needed to 
> >> handle the mathematics needed to express Godel's G, or the Halting Problem. 
> >> Thus, your "Proof" that these Theorems are "Wrong" is incorrect, you 
> >> have only proven that your limited logic system can't reach them in expressibility. 
> > 
> > Thanks for confirmation, that's what exactly what I was trying to tell 
> > to topic poster in one of my previous posts. Prolog in it's bare form 
> > is a bad theorem solver. It wasn't designed a such. 
> > 
> > If you want to deal with such problems maybe it is better to use Coq 
> > theorem prover, I've never used it by myself, but it looks like one of 
> > the best proving assistants out there.
> 
> And indeed there is a fully formalised proof of GIT in Coq (though I 
> think it's the slightly tighter Gödel-Rosser version). 

That's just another piece of nonsense, GIT can be formalised in BASIC for that sake.

You bunch of spamming absolute assholes and spammers of all poonds, indeed Olcott is your good measure.

*Plonk*

Julio

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


#12905

Fromolcott <polcott2@gmail.com>
Date2022-05-02 19:57 -0500
Message-ID<t4pulq$bci$1@dont-email.me>
In reply to#12898
On 5/2/2022 6:43 PM, Ben wrote:
> Aleksy Grabowski <hurufu@gmail.com> writes:
> 
>>> IF you are defining that your logic system is limited to what Prolog can "Prove", that is fine. Just realize that you have just defined that your
>>> logic system can't handle a lot of the real problems in the world, and in particular, it is very limited in the mathematics it can handle.
>>> I am pretty sure that Prolog is NOT up to handling the logic needed to
>>> handle the mathematics needed to express Godel's G, or the Halting Problem.
>>> Thus, your "Proof" that these Theorems are "Wrong" is incorrect, you
>>> have only proven that your limited logic system can't reach them in expressibility.
>>
>> Thanks for confirmation, that's what exactly what I was trying to tell
>> to topic poster in one of my previous posts. Prolog in it's bare form
>> is a bad theorem solver. It wasn't designed a such.
>>
>> If you want to deal with such problems maybe it is better to use Coq
>> theorem prover, I've never used it by myself, but it looks like one of
>> the best proving assistants out there.
> 
> And indeed there is a fully formalised proof of GIT in Coq (though I
> think it's the slightly tighter Gödel-Rosser version).
> 

It is true that G is not provable. G is not provable because it is 
semantically incorrect in the exactly same way that the Liar Paradox is 
semantically incorrect.

Gödel says:
14 Every epistemological antinomy can likewise be used for a similar 
undecidability proof

André denied this six times yesterday
The Liar Paradox is an epistemological antinomy, thus can likewise be 
used for a similar undecidability proof.

Which means that the Liar Paradox is sufficiently equivalent to Gödel's 
G. Which means if the basic mechanism of epistemological antinomy is 
shown to be semantically incorrect then Gödel's G is shown to be 
semantically incorrect.

-- 
Copyright 2022 Pete Olcott "Talent hits a target no one else can hit;
Genius hits a target no one else can see." Arthur Schopenhauer

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


#12906

FromBen <ben.usenet@bsb.me.uk>
Date2022-05-03 03:21 +0100
Message-ID<874k27fjan.fsf@bsb.me.uk>
In reply to#12905
olcott <polcott2@gmail.com> writes:

> On 5/2/2022 6:43 PM, Ben wrote:
>> Aleksy Grabowski <hurufu@gmail.com> writes:

>>> Thanks for confirmation, that's what exactly what I was trying to tell
>>> to topic poster in one of my previous posts. Prolog in it's bare form
>>> is a bad theorem solver. It wasn't designed a such.
>>>
>>> If you want to deal with such problems maybe it is better to use Coq
>>> theorem prover, I've never used it by myself, but it looks like one of
>>> the best proving assistants out there.
>>
>> And indeed there is a fully formalised proof of GIT in Coq (though I
>> think it's the slightly tighter Gödel-Rosser version). 
>
> It is true that G is not provable.

G is provable.  Proofs abound.  I was pointing out one in a proper proof
assistant, Coq.

-- 
Ben.
"le génie humain a des limites, quand la bêtise humaine n’en a pas"
Alexandre Dumas (fils)

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


#12907

Fromolcott <polcott2@gmail.com>
Date2022-05-02 22:01 -0500
Message-ID<t4q5uo$veh$1@dont-email.me>
In reply to#12906
On 5/2/2022 9:21 PM, Ben wrote:
> olcott <polcott2@gmail.com> writes:
> 
>> On 5/2/2022 6:43 PM, Ben wrote:
>>> Aleksy Grabowski <hurufu@gmail.com> writes:
> 
>>>> Thanks for confirmation, that's what exactly what I was trying to tell
>>>> to topic poster in one of my previous posts. Prolog in it's bare form
>>>> is a bad theorem solver. It wasn't designed a such.
>>>>
>>>> If you want to deal with such problems maybe it is better to use Coq
>>>> theorem prover, I've never used it by myself, but it looks like one of
>>>> the best proving assistants out there.
>>>
>>> And indeed there is a fully formalised proof of GIT in Coq (though I
>>> think it's the slightly tighter Gödel-Rosser version).
>>
>> It is true that G is not provable.
> 
> G is provable.  Proofs abound.  I was pointing out one in a proper proof
> assistant, Coq.
> 

It is OK that you are not a math guy.
If you were a math guy you would understand that if G is provable then 
that makes Gödel totally wrong. G is not Gödel's theorem, it is a key 
element of his theorem.

Incomplete T means that there exists a φ such that φ is not provable or 
refutable in formal system T.

Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).


-- 
Copyright 2022 Pete Olcott "Talent hits a target no one else can hit;
Genius hits a target no one else can see." Arthur Schopenhauer

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


#12908

FromJulio Di Egidio <julio@diegidio.name>
Date2022-05-03 01:18 -0700
Message-ID<86965eac-1f4e-4f19-8091-ffc8b3998ff7n@googlegroups.com>
In reply to#12907
On Tuesday, 3 May 2022 at 05:01:46 UTC+2, olcott wrote:
> On 5/2/2022 9:21 PM, Ben wrote: 
> > olcott <polc...@gmail.com> writes: 
> >> On 5/2/2022 6:43 PM, Ben wrote: 
> >>> Aleksy Grabowski <hur...@gmail.com> writes: 
> > 
> >>>> Thanks for confirmation, that's what exactly what I was trying to tell 
> >>>> to topic poster in one of my previous posts. Prolog in it's bare form 
> >>>> is a bad theorem solver. It wasn't designed a such. 
> >>>> 
> >>>> If you want to deal with such problems maybe it is better to use Coq 
> >>>> theorem prover, I've never used it by myself, but it looks like one of 
> >>>> the best proving assistants out there. 
> >>> 
> >>> And indeed there is a fully formalised proof of GIT in Coq (though I 
> >>> think it's the slightly tighter Gödel-Rosser version). 
> >> 
> >> It is true that G is not provable. 
> > 
> > G is provable. Proofs abound. I was pointing out one in a proper proof 
> > assistant, Coq. 
> >
> It is OK that you are not a math guy. 

Or a programmer for that sake, that fucking moron just full of shit.

But it's NOT OK to cross-spam 5 Usenet groups with just your personal demented chats.

Eat shit and die you all.

Julio

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


#12909

FromRichard Damon <Richard@Damon-Family.org>
Date2022-05-03 08:05 -0400
Message-ID<vU8cK.2577$ATo1.2258@fx33.iad>
In reply to#12907
On 5/2/22 11:01 PM, olcott wrote:
> On 5/2/2022 9:21 PM, Ben wrote:
>> olcott <polcott2@gmail.com> writes:
>>
>>> On 5/2/2022 6:43 PM, Ben wrote:
>>>> Aleksy Grabowski <hurufu@gmail.com> writes:
>>
>>>>> Thanks for confirmation, that's what exactly what I was trying to tell
>>>>> to topic poster in one of my previous posts. Prolog in it's bare form
>>>>> is a bad theorem solver. It wasn't designed a such.
>>>>>
>>>>> If you want to deal with such problems maybe it is better to use Coq
>>>>> theorem prover, I've never used it by myself, but it looks like one of
>>>>> the best proving assistants out there.
>>>>
>>>> And indeed there is a fully formalised proof of GIT in Coq (though I
>>>> think it's the slightly tighter Gödel-Rosser version).
>>>
>>> It is true that G is not provable.
>>
>> G is provable.  Proofs abound.  I was pointing out one in a proper proof
>> assistant, Coq.
>>
> 
> It is OK that you are not a math guy.
> If you were a math guy you would understand that if G is provable then 
> that makes Gödel totally wrong. G is not Gödel's theorem, it is a key 
> element of his theorem.
> 
> Incomplete T means that there exists a φ such that φ is not provable or 
> refutable in formal system T.
> 
> Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
> 
> 

No, G IS provable, just not in the system F that G is described in, thus 
F is Incomplete by your definition above.

Part of the key of the Godel proof is that while G sort of refers to 
itself, it does it in a way that F can't handle, so in F, G doesn't 
refer to itself but just "some statement", but in a 'more advanced' 
version of F, say F', we can see that relationship, and show that G must 
be true, proving it in F', but not in F, thus F is incomplete.

We can then show that we can make a G' in F' with the same property, and 
thus show that there exists a system F'' where we can prove G'.

This is why you simplification doesn't work. In F, we can't convert G 
into the statement G says that G is unprovable, but we can in F', thus 
the statement in F' is that G says that G in unprovable in F, and that 
statement is provable in F'

You don't seem to be able to handle the concept of layers of logic systems.

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


#12938 — Re: Is this correct Prolog? [ Tarski ]

Fromolcott <polcott2@gmail.com>
Date2022-05-04 21:30 -0500
SubjectRe: Is this correct Prolog? [ Tarski ]
Message-ID<t4vcsa$g9o$1@dont-email.me>
In reply to#12909
On 5/3/2022 7:05 AM, Richard Damon wrote:
> On 5/2/22 11:01 PM, olcott wrote:
>> On 5/2/2022 9:21 PM, Ben wrote:
>>> olcott <polcott2@gmail.com> writes:
>>>
>>>> On 5/2/2022 6:43 PM, Ben wrote:
>>>>> Aleksy Grabowski <hurufu@gmail.com> writes:
>>>
>>>>>> Thanks for confirmation, that's what exactly what I was trying to 
>>>>>> tell
>>>>>> to topic poster in one of my previous posts. Prolog in it's bare form
>>>>>> is a bad theorem solver. It wasn't designed a such.
>>>>>>
>>>>>> If you want to deal with such problems maybe it is better to use Coq
>>>>>> theorem prover, I've never used it by myself, but it looks like 
>>>>>> one of
>>>>>> the best proving assistants out there.
>>>>>
>>>>> And indeed there is a fully formalised proof of GIT in Coq (though I
>>>>> think it's the slightly tighter Gödel-Rosser version).
>>>>
>>>> It is true that G is not provable.
>>>
>>> G is provable.  Proofs abound.  I was pointing out one in a proper proof
>>> assistant, Coq.
>>>
>>
>> It is OK that you are not a math guy.
>> If you were a math guy you would understand that if G is provable then 
>> that makes Gödel totally wrong. G is not Gödel's theorem, it is a key 
>> element of his theorem.
>>
>> Incomplete T means that there exists a φ such that φ is not provable 
>> or refutable in formal system T.
>>
>> Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
>>
>>
> 
> No, G IS provable, just not in the system F that G is described in, thus 
> F is Incomplete by your definition above.
> 
> Part of the key of the Godel proof is that while G sort of refers to 
> itself, it does it in a way that F can't handle, so in F, G doesn't 
> refer to itself but just "some statement", but in a 'more advanced' 
> version of F, say F', we can see that relationship, and show that G must 
> be true, proving it in F', but not in F, thus F is incomplete.
> 

Tarski's hierarchy of languages.

It only works at a higher level language because the expression of 
language at the next level is not self-contradictory.

All epistemological antinomies are self-contradictory making them 
semantically invalid.

In his undefinability proof: (only two pages long)
https://liarparadox.org/Tarski_275_276.pdf

He defines these two levels as "the theory" and the next higher level is 
called the "the metatheory".  (see link).


> We can then show that we can make a G' in F' with the same property, and 
> thus show that there exists a system F'' where we can prove G'.
> 
> This is why you simplification doesn't work. In F, we can't convert G 
> into the statement G says that G is unprovable, but we can in F', thus 
> the statement in F' is that G says that G in unprovable in F, and that 
> statement is provable in F'
> 

Likewise for the liar Paradox. Apparently Tarski could prove the Liar 
Paradox in his meta-theory.

> You don't seem to be able to handle the concept of layers of logic systems.
> 


-- 
Copyright 2022 Pete Olcott "Talent hits a target no one else can hit;
Genius hits a target no one else can see." Arthur Schopenhauer

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


#12939 — Re: Is this correct Prolog? [ Tarski ]

FromRichard Damon <Richard@Damon-Family.org>
Date2022-05-04 22:46 -0400
SubjectRe: Is this correct Prolog? [ Tarski ]
Message-ID<4UGcK.11523$IQK.4635@fx02.iad>
In reply to#12938
On 5/4/22 10:30 PM, olcott wrote:
> On 5/3/2022 7:05 AM, Richard Damon wrote:
>> On 5/2/22 11:01 PM, olcott wrote:
>>> On 5/2/2022 9:21 PM, Ben wrote:
>>>> olcott <polcott2@gmail.com> writes:
>>>>
>>>>> On 5/2/2022 6:43 PM, Ben wrote:
>>>>>> Aleksy Grabowski <hurufu@gmail.com> writes:
>>>>
>>>>>>> Thanks for confirmation, that's what exactly what I was trying to 
>>>>>>> tell
>>>>>>> to topic poster in one of my previous posts. Prolog in it's bare 
>>>>>>> form
>>>>>>> is a bad theorem solver. It wasn't designed a such.
>>>>>>>
>>>>>>> If you want to deal with such problems maybe it is better to use Coq
>>>>>>> theorem prover, I've never used it by myself, but it looks like 
>>>>>>> one of
>>>>>>> the best proving assistants out there.
>>>>>>
>>>>>> And indeed there is a fully formalised proof of GIT in Coq (though I
>>>>>> think it's the slightly tighter Gödel-Rosser version).
>>>>>
>>>>> It is true that G is not provable.
>>>>
>>>> G is provable.  Proofs abound.  I was pointing out one in a proper 
>>>> proof
>>>> assistant, Coq.
>>>>
>>>
>>> It is OK that you are not a math guy.
>>> If you were a math guy you would understand that if G is provable 
>>> then that makes Gödel totally wrong. G is not Gödel's theorem, it is 
>>> a key element of his theorem.
>>>
>>> Incomplete T means that there exists a φ such that φ is not provable 
>>> or refutable in formal system T.
>>>
>>> Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
>>>
>>>
>>
>> No, G IS provable, just not in the system F that G is described in, 
>> thus F is Incomplete by your definition above.
>>
>> Part of the key of the Godel proof is that while G sort of refers to 
>> itself, it does it in a way that F can't handle, so in F, G doesn't 
>> refer to itself but just "some statement", but in a 'more advanced' 
>> version of F, say F', we can see that relationship, and show that G 
>> must be true, proving it in F', but not in F, thus F is incomplete.
>>
> 
> Tarski's hierarchy of languages.
> 
> It only works at a higher level language because the expression of 
> language at the next level is not self-contradictory.
> 
> All epistemological antinomies are self-contradictory making them 
> semantically invalid.
> 
> In his undefinability proof: (only two pages long)
> https://liarparadox.org/Tarski_275_276.pdf
> 
> He defines these two levels as "the theory" and the next higher level is 
> called the "the metatheory".  (see link).

So we can prove G in the Metatheory, so it is True in the Theory too.

> since in this interpretation the sentence x, which contains no specific term of the metatheory, is its o\vn correlate, the proof of the sentence x given in the metatheory can automatically be carried over into the theory itself: the sentence x which is undecidable in the original theory becomes a decidable sentence in the enriched theory.

But if G is true in the Theory, it is BY DEFINITION not provable in the 
Theory, so the space of the Theory is shown to have a True Statement 
which is not provable, thus the system of the Theory in Incomplete.



> 
> 
>> We can then show that we can make a G' in F' with the same property, 
>> and thus show that there exists a system F'' where we can prove G'.
>>
>> This is why you simplification doesn't work. In F, we can't convert G 
>> into the statement G says that G is unprovable, but we can in F', thus 
>> the statement in F' is that G says that G in unprovable in F, and that 
>> statement is provable in F'
>>
> 
> Likewise for the liar Paradox. Apparently Tarski could prove the Liar 
> Paradox in his meta-theory.
> 
>> You don't seem to be able to handle the concept of layers of logic 
>> systems.
>>
> 
> 

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


#12940 — Re: Is this correct Prolog? [ Tarski ]

Fromolcott <polcott2@gmail.com>
Date2022-05-04 22:02 -0500
SubjectRe: Is this correct Prolog? [ Tarski ]
Message-ID<t4veo9$2d5$1@dont-email.me>
In reply to#12939
On 5/4/2022 9:46 PM, Richard Damon wrote:
> On 5/4/22 10:30 PM, olcott wrote:
>> On 5/3/2022 7:05 AM, Richard Damon wrote:
>>> On 5/2/22 11:01 PM, olcott wrote:
>>>> On 5/2/2022 9:21 PM, Ben wrote:
>>>>> olcott <polcott2@gmail.com> writes:
>>>>>
>>>>>> On 5/2/2022 6:43 PM, Ben wrote:
>>>>>>> Aleksy Grabowski <hurufu@gmail.com> writes:
>>>>>
>>>>>>>> Thanks for confirmation, that's what exactly what I was trying 
>>>>>>>> to tell
>>>>>>>> to topic poster in one of my previous posts. Prolog in it's bare 
>>>>>>>> form
>>>>>>>> is a bad theorem solver. It wasn't designed a such.
>>>>>>>>
>>>>>>>> If you want to deal with such problems maybe it is better to use 
>>>>>>>> Coq
>>>>>>>> theorem prover, I've never used it by myself, but it looks like 
>>>>>>>> one of
>>>>>>>> the best proving assistants out there.
>>>>>>>
>>>>>>> And indeed there is a fully formalised proof of GIT in Coq (though I
>>>>>>> think it's the slightly tighter Gödel-Rosser version).
>>>>>>
>>>>>> It is true that G is not provable.
>>>>>
>>>>> G is provable.  Proofs abound.  I was pointing out one in a proper 
>>>>> proof
>>>>> assistant, Coq.
>>>>>
>>>>
>>>> It is OK that you are not a math guy.
>>>> If you were a math guy you would understand that if G is provable 
>>>> then that makes Gödel totally wrong. G is not Gödel's theorem, it is 
>>>> a key element of his theorem.
>>>>
>>>> Incomplete T means that there exists a φ such that φ is not provable 
>>>> or refutable in formal system T.
>>>>
>>>> Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
>>>>
>>>>
>>>
>>> No, G IS provable, just not in the system F that G is described in, 
>>> thus F is Incomplete by your definition above.
>>>
>>> Part of the key of the Godel proof is that while G sort of refers to 
>>> itself, it does it in a way that F can't handle, so in F, G doesn't 
>>> refer to itself but just "some statement", but in a 'more advanced' 
>>> version of F, say F', we can see that relationship, and show that G 
>>> must be true, proving it in F', but not in F, thus F is incomplete.
>>>
>>
>> Tarski's hierarchy of languages.
>>
>> It only works at a higher level language because the expression of 
>> language at the next level is not self-contradictory.
>>
>> All epistemological antinomies are self-contradictory making them 
>> semantically invalid.
>>
>> In his undefinability proof: (only two pages long)
>> https://liarparadox.org/Tarski_275_276.pdf
>>
>> He defines these two levels as "the theory" and the next higher level 
>> is called the "the metatheory".  (see link).
> 
> So we can prove G in the Metatheory, so it is True in the Theory too.

In the same way that having a cat in your attic is proof that your car 
is leaking oil.

>> since in this interpretation the sentence x, which contains no 
>> specific term of the metatheory, is its o\vn correlate, the proof of 
>> the sentence x given in the metatheory can automatically be carried 
>> over into the theory itself: the sentence x which is undecidable in 
>> the original theory becomes a decidable sentence in the enriched theory.
> 
> But if G is true in the Theory, it is BY DEFINITION not provable in the 
> Theory, so the space of the Theory is shown to have a True Statement 
> which is not provable, thus the system of the Theory in Incomplete.

It really has never made any sense how people can't understand that 
self-contradictory expressions of language are necessary semantically 
invalid. Back in 1974 mankind has had almost 2000 years to think about 
the Liar Paradox and no one had a clue what the issue was.

Any unprovable expression of any formal or natural language is simply 
untrue and nothing more.

>>
>>
>>> We can then show that we can make a G' in F' with the same property, 
>>> and thus show that there exists a system F'' where we can prove G'.
>>>
>>> This is why you simplification doesn't work. In F, we can't convert G 
>>> into the statement G says that G is unprovable, but we can in F', 
>>> thus the statement in F' is that G says that G in unprovable in F, 
>>> and that statement is provable in F'
>>>
>>
>> Likewise for the liar Paradox. Apparently Tarski could prove the Liar 
>> Paradox in his meta-theory.
>>
>>> You don't seem to be able to handle the concept of layers of logic 
>>> systems.
>>>
>>
>>
> 


-- 
Copyright 2022 Pete Olcott "Talent hits a target no one else can hit;
Genius hits a target no one else can see." Arthur Schopenhauer

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


#12951 — Re: Is this correct Prolog? [ Tarski ]

FromRichard Damon <Richard@Damon-Family.org>
Date2022-05-05 07:41 -0400
SubjectRe: Is this correct Prolog? [ Tarski ]
Message-ID<XJOcK.720276$7F2.122603@fx12.iad>
In reply to#12940
On 5/4/22 11:02 PM, olcott wrote:
> On 5/4/2022 9:46 PM, Richard Damon wrote:
>> On 5/4/22 10:30 PM, olcott wrote:
>>> On 5/3/2022 7:05 AM, Richard Damon wrote:
>>>> On 5/2/22 11:01 PM, olcott wrote:
>>>>> On 5/2/2022 9:21 PM, Ben wrote:
>>>>>> olcott <polcott2@gmail.com> writes:
>>>>>>
>>>>>>> On 5/2/2022 6:43 PM, Ben wrote:
>>>>>>>> Aleksy Grabowski <hurufu@gmail.com> writes:
>>>>>>
>>>>>>>>> Thanks for confirmation, that's what exactly what I was trying 
>>>>>>>>> to tell
>>>>>>>>> to topic poster in one of my previous posts. Prolog in it's 
>>>>>>>>> bare form
>>>>>>>>> is a bad theorem solver. It wasn't designed a such.
>>>>>>>>>
>>>>>>>>> If you want to deal with such problems maybe it is better to 
>>>>>>>>> use Coq
>>>>>>>>> theorem prover, I've never used it by myself, but it looks like 
>>>>>>>>> one of
>>>>>>>>> the best proving assistants out there.
>>>>>>>>
>>>>>>>> And indeed there is a fully formalised proof of GIT in Coq 
>>>>>>>> (though I
>>>>>>>> think it's the slightly tighter Gödel-Rosser version).
>>>>>>>
>>>>>>> It is true that G is not provable.
>>>>>>
>>>>>> G is provable.  Proofs abound.  I was pointing out one in a proper 
>>>>>> proof
>>>>>> assistant, Coq.
>>>>>>
>>>>>
>>>>> It is OK that you are not a math guy.
>>>>> If you were a math guy you would understand that if G is provable 
>>>>> then that makes Gödel totally wrong. G is not Gödel's theorem, it 
>>>>> is a key element of his theorem.
>>>>>
>>>>> Incomplete T means that there exists a φ such that φ is not 
>>>>> provable or refutable in formal system T.
>>>>>
>>>>> Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
>>>>>
>>>>>
>>>>
>>>> No, G IS provable, just not in the system F that G is described in, 
>>>> thus F is Incomplete by your definition above.
>>>>
>>>> Part of the key of the Godel proof is that while G sort of refers to 
>>>> itself, it does it in a way that F can't handle, so in F, G doesn't 
>>>> refer to itself but just "some statement", but in a 'more advanced' 
>>>> version of F, say F', we can see that relationship, and show that G 
>>>> must be true, proving it in F', but not in F, thus F is incomplete.
>>>>
>>>
>>> Tarski's hierarchy of languages.
>>>
>>> It only works at a higher level language because the expression of 
>>> language at the next level is not self-contradictory.
>>>
>>> All epistemological antinomies are self-contradictory making them 
>>> semantically invalid.
>>>
>>> In his undefinability proof: (only two pages long)
>>> https://liarparadox.org/Tarski_275_276.pdf
>>>
>>> He defines these two levels as "the theory" and the next higher level 
>>> is called the "the metatheory".  (see link).
>>
>> So we can prove G in the Metatheory, so it is True in the Theory too.
> 
> In the same way that having a cat in your attic is proof that your car 
> is leaking oil.

Nope, shows you don't understand the proof. Have you actually read it, 
or just the 'cliff notes' version. You know, the one with the actual

> 
>>> since in this interpretation the sentence x, which contains no 
>>> specific term of the metatheory, is its o\vn correlate, the proof of 
>>> the sentence x given in the metatheory can automatically be carried 
>>> over into the theory itself: the sentence x which is undecidable in 
>>> the original theory becomes a decidable sentence in the enriched theory.
>>
>> But if G is true in the Theory, it is BY DEFINITION not provable in 
>> the Theory, so the space of the Theory is shown to have a True 
>> Statement which is not provable, thus the system of the Theory in 
>> Incomplete.
> 
> It really has never made any sense how people can't understand that 
> self-contradictory expressions of language are necessary semantically 
> invalid. Back in 1974 mankind has had almost 2000 years to think about 
> the Liar Paradox and no one had a clue what the issue was.

Except that G isn't self-contradictory. The actual G makes a statement 
of a mathematical problem and asks if it has a solution. That sort of 
statement is ALWAYS a Truth Bearer.

I think your problem is you don't even uderstand that power and limits 
of semantics.

> 
> Any unprovable expression of any formal or natural language is simply 
> untrue and nothing more.

Nope. Truth does not mean Provable. An Unproven statement (or even 
unprovable statement) might still be True, it just can't be KNOWN. You 
confuse truth with knowledge, maybe because you have too much ego and 
think your knowledge defines what is.

By your statement, the Bible is untrue, and you are thus a Liar for 
making statements based on it being true.

We can't beleive the words of a Liar, so we shouldn't beleive you when 
you claim Truth implies Provable.

Yes, you can build a logic system that defines that, in that system, a 
statement is only a Truth Bearer is it is provable or refutable, but 
such a system can not handle our mathematics (at least not and stay 
consistent).

All you are doing is showing you don't understand how logic actually works.

> 
>>>
>>>
>>>> We can then show that we can make a G' in F' with the same property, 
>>>> and thus show that there exists a system F'' where we can prove G'.
>>>>
>>>> This is why you simplification doesn't work. In F, we can't convert 
>>>> G into the statement G says that G is unprovable, but we can in F', 
>>>> thus the statement in F' is that G says that G in unprovable in F, 
>>>> and that statement is provable in F'
>>>>
>>>
>>> Likewise for the liar Paradox. Apparently Tarski could prove the Liar 
>>> Paradox in his meta-theory.
>>>
>>>> You don't seem to be able to handle the concept of layers of logic 
>>>> systems.
>>>>
>>>
>>>
>>
> 
> 

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


#12952 — Re: Is this correct Prolog? [ Tarski ]

Fromolcott <polcott2@gmail.com>
Date2022-05-05 12:57 -0500
SubjectRe: Is this correct Prolog? [ Tarski ]
Message-ID<t5136n$4j0$1@dont-email.me>
In reply to#12939
On 5/4/2022 9:46 PM, Richard Damon wrote:
> On 5/4/22 10:30 PM, olcott wrote:
>> On 5/3/2022 7:05 AM, Richard Damon wrote:
>>> On 5/2/22 11:01 PM, olcott wrote:
>>>> On 5/2/2022 9:21 PM, Ben wrote:
>>>>> olcott <polcott2@gmail.com> writes:
>>>>>
>>>>>> On 5/2/2022 6:43 PM, Ben wrote:
>>>>>>> Aleksy Grabowski <hurufu@gmail.com> writes:
>>>>>
>>>>>>>> Thanks for confirmation, that's what exactly what I was trying 
>>>>>>>> to tell
>>>>>>>> to topic poster in one of my previous posts. Prolog in it's bare 
>>>>>>>> form
>>>>>>>> is a bad theorem solver. It wasn't designed a such.
>>>>>>>>
>>>>>>>> If you want to deal with such problems maybe it is better to use 
>>>>>>>> Coq
>>>>>>>> theorem prover, I've never used it by myself, but it looks like 
>>>>>>>> one of
>>>>>>>> the best proving assistants out there.
>>>>>>>
>>>>>>> And indeed there is a fully formalised proof of GIT in Coq (though I
>>>>>>> think it's the slightly tighter Gödel-Rosser version).
>>>>>>
>>>>>> It is true that G is not provable.
>>>>>
>>>>> G is provable.  Proofs abound.  I was pointing out one in a proper 
>>>>> proof
>>>>> assistant, Coq.
>>>>>
>>>>
>>>> It is OK that you are not a math guy.
>>>> If you were a math guy you would understand that if G is provable 
>>>> then that makes Gödel totally wrong. G is not Gödel's theorem, it is 
>>>> a key element of his theorem.
>>>>
>>>> Incomplete T means that there exists a φ such that φ is not provable 
>>>> or refutable in formal system T.
>>>>
>>>> Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
>>>>
>>>>
>>>
>>> No, G IS provable, just not in the system F that G is described in, 
>>> thus F is Incomplete by your definition above.
>>>
>>> Part of the key of the Godel proof is that while G sort of refers to 
>>> itself, it does it in a way that F can't handle, so in F, G doesn't 
>>> refer to itself but just "some statement", but in a 'more advanced' 
>>> version of F, say F', we can see that relationship, and show that G 
>>> must be true, proving it in F', but not in F, thus F is incomplete.
>>>
>>
>> Tarski's hierarchy of languages.
>>
>> It only works at a higher level language because the expression of 
>> language at the next level is not self-contradictory.
>>
>> All epistemological antinomies are self-contradictory making them 
>> semantically invalid.
>>
>> In his undefinability proof: (only two pages long)
>> https://liarparadox.org/Tarski_275_276.pdf
>>
>> He defines these two levels as "the theory" and the next higher level 
>> is called the "the metatheory".  (see link).
> 
> So we can prove G in the Metatheory, 

Yes.

> so it is True in the Theory too.
> 

Not at all.
In the theory p is self-contradictory thus not a truth bearer.
In the meta-theory p is NOT self-contradictory.

>> since in this interpretation the sentence x, which contains no 
>> specific term of the metatheory, is its o\vn correlate, the proof of 
>> the sentence x given in the metatheory can automatically be carried 
>> over into the theory itself: the sentence x which is undecidable in 
>> the original theory becomes a decidable sentence in the enriched theory.
> 
> But if G is true in the Theory, it is BY DEFINITION not provable in the 
> Theory, so the space of the Theory is shown to have a True Statement 
> which is not provable, thus the system of the Theory in Incomplete.

G is self-contradictory on the theory and non self-contradictory in the 
meta-theory.

>>
>>
>>> We can then show that we can make a G' in F' with the same property, 
>>> and thus show that there exists a system F'' where we can prove G'.
>>>
>>> This is why you simplification doesn't work. In F, we can't convert G 
>>> into the statement G says that G is unprovable, but we can in F', 
>>> thus the statement in F' is that G says that G in unprovable in F, 
>>> and that statement is provable in F'
>>>
>>
>> Likewise for the liar Paradox. Apparently Tarski could prove the Liar 
>> Paradox in his meta-theory.
>>
>>> You don't seem to be able to handle the concept of layers of logic 
>>> systems.
>>>
>>
>>
> 


-- 
Copyright 2022 Pete Olcott "Talent hits a target no one else can hit;
Genius hits a target no one else can see." Arthur Schopenhauer

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


#12953 — Re: Is this correct Prolog? [ Tarski ]

FromAndré G. Isaak <agisaak@gm.invalid>
Date2022-05-05 12:06 -0600
SubjectRe: Is this correct Prolog? [ Tarski ]
Message-ID<t513mm$7em$1@dont-email.me>
In reply to#12952
On 2022-05-05 11:57, olcott wrote:
> On 5/4/2022 9:46 PM, Richard Damon wrote:

>> But if G is true in the Theory, it is BY DEFINITION not provable in 
>> the Theory, so the space of the Theory is shown to have a True 
>> Statement which is not provable, thus the system of the Theory in 
>> Incomplete.
> 
> G is self-contradictory on the theory and non self-contradictory in the 
> meta-theory.

G is not self-contradictory in either the theory or the meta-theory.

The Liar Paradox and G are not the same sentence. You keep treating them 
as if they were based solely on Gödel's claim that there is a close 
relationship between them. But saying two things are closely related 
does not mean they are the same.

G asserts a claim about arithmetic. It asserts nothing about itself.

André

-- 
To email remove 'invalid' & replace 'gm' with well known Google mail 
service.

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


#12954 — Re: Is this correct Prolog? [ Tarski ]

Fromolcott <polcott2@gmail.com>
Date2022-05-05 16:23 -0500
SubjectRe: Is this correct Prolog? [ Tarski ]
Message-ID<t51f8k$5sc$1@dont-email.me>
In reply to#12953
On 5/5/2022 1:06 PM, André G. Isaak wrote:
> On 2022-05-05 11:57, olcott wrote:
>> On 5/4/2022 9:46 PM, Richard Damon wrote:
> 
>>> But if G is true in the Theory, it is BY DEFINITION not provable in 
>>> the Theory, so the space of the Theory is shown to have a True 
>>> Statement which is not provable, thus the system of the Theory in 
>>> Incomplete.
>>
>> G is self-contradictory on the theory and non self-contradictory in 
>> the meta-theory.
> 
> G is not self-contradictory in either the theory or the meta-theory.
> 
> The Liar Paradox and G are not the same sentence. You keep treating them 
> as if they were based solely on Gödel's claim that there is a close 
> relationship between them. But saying two things are closely related 
> does not mean they are the same.
> 
> G asserts a claim about arithmetic. It asserts nothing about itself.
> 
> André
> 

 From the quote below:
We are therefore confronted with a proposition which asserts its own 
unprovability.

Gödel says:
The analogy between this result and Richard’s antinomy leaps to the eye; 
there is also a close relationship with the “liar” antinomy,14 since the 
undecidable proposition [R(q); q] states precisely that q belongs to K, 
i.e. according to (1), that [R(q); q] is not provable. We are therefore 
confronted with a proposition which asserts its own unprovability.


Tarski proof is based on this exact same thing in its first step:
https://liarparadox.org/Tarski_275_276.pdf

(1) x ⋶ Pr if and only if p
where the symbol 'p' represents the whole sentence x
and Pr means Provable

This is a Tarski was of saying:
"a proposition which asserts its own unprovability."


-- 
Copyright 2022 Pete Olcott "Talent hits a target no one else can hit;
Genius hits a target no one else can see." Arthur Schopenhauer

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


#12955 — Re: Is this correct Prolog? [ Tarski ]

FromRichard Damon <Richard@Damon-Family.org>
Date2022-05-05 22:24 -0400
SubjectRe: Is this correct Prolog? [ Tarski ]
Message-ID<8F%cK.42$t72a.1@fx10.iad>
In reply to#12952
On 5/5/22 1:57 PM, olcott wrote:
> On 5/4/2022 9:46 PM, Richard Damon wrote:
>> On 5/4/22 10:30 PM, olcott wrote:
>>> On 5/3/2022 7:05 AM, Richard Damon wrote:
>>>> On 5/2/22 11:01 PM, olcott wrote:
>>>>> On 5/2/2022 9:21 PM, Ben wrote:
>>>>>> olcott <polcott2@gmail.com> writes:
>>>>>>
>>>>>>> On 5/2/2022 6:43 PM, Ben wrote:
>>>>>>>> Aleksy Grabowski <hurufu@gmail.com> writes:
>>>>>>
>>>>>>>>> Thanks for confirmation, that's what exactly what I was trying 
>>>>>>>>> to tell
>>>>>>>>> to topic poster in one of my previous posts. Prolog in it's 
>>>>>>>>> bare form
>>>>>>>>> is a bad theorem solver. It wasn't designed a such.
>>>>>>>>>
>>>>>>>>> If you want to deal with such problems maybe it is better to 
>>>>>>>>> use Coq
>>>>>>>>> theorem prover, I've never used it by myself, but it looks like 
>>>>>>>>> one of
>>>>>>>>> the best proving assistants out there.
>>>>>>>>
>>>>>>>> And indeed there is a fully formalised proof of GIT in Coq 
>>>>>>>> (though I
>>>>>>>> think it's the slightly tighter Gödel-Rosser version).
>>>>>>>
>>>>>>> It is true that G is not provable.
>>>>>>
>>>>>> G is provable.  Proofs abound.  I was pointing out one in a proper 
>>>>>> proof
>>>>>> assistant, Coq.
>>>>>>
>>>>>
>>>>> It is OK that you are not a math guy.
>>>>> If you were a math guy you would understand that if G is provable 
>>>>> then that makes Gödel totally wrong. G is not Gödel's theorem, it 
>>>>> is a key element of his theorem.
>>>>>
>>>>> Incomplete T means that there exists a φ such that φ is not 
>>>>> provable or refutable in formal system T.
>>>>>
>>>>> Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
>>>>>
>>>>>
>>>>
>>>> No, G IS provable, just not in the system F that G is described in, 
>>>> thus F is Incomplete by your definition above.
>>>>
>>>> Part of the key of the Godel proof is that while G sort of refers to 
>>>> itself, it does it in a way that F can't handle, so in F, G doesn't 
>>>> refer to itself but just "some statement", but in a 'more advanced' 
>>>> version of F, say F', we can see that relationship, and show that G 
>>>> must be true, proving it in F', but not in F, thus F is incomplete.
>>>>
>>>
>>> Tarski's hierarchy of languages.
>>>
>>> It only works at a higher level language because the expression of 
>>> language at the next level is not self-contradictory.
>>>
>>> All epistemological antinomies are self-contradictory making them 
>>> semantically invalid.
>>>
>>> In his undefinability proof: (only two pages long)
>>> https://liarparadox.org/Tarski_275_276.pdf
>>>
>>> He defines these two levels as "the theory" and the next higher level 
>>> is called the "the metatheory".  (see link).
>>
>> So we can prove G in the Metatheory, 
> 
> Yes.
> 
>> so it is True in the Theory too.
>>
> 
> Not at all.
> In the theory p is self-contradictory thus not a truth bearer.
> In the meta-theory p is NOT self-contradictory.

How do you get that.

In the Theory, you can't even tell that G references itself, but is just 
a statement about mathematics.

> 
>>> since in this interpretation the sentence x, which contains no 
>>> specific term of the metatheory, is its o\vn correlate, the proof of 
>>> the sentence x given in the metatheory can automatically be carried 
>>> over into the theory itself: the sentence x which is undecidable in 
>>> the original theory becomes a decidable sentence in the enriched theory.
>>
>> But if G is true in the Theory, it is BY DEFINITION not provable in 
>> the Theory, so the space of the Theory is shown to have a True 
>> Statement which is not provable, thus the system of the Theory in 
>> Incomplete.
> 
> G is self-contradictory on the theory and non self-contradictory in the 
> meta-theory.

No, because in the theory, G doesn't even reference itself, so it can't 
be self-contradictory.

I think you don't even know what G is, but have only read the clift 
notes edition that actually explain it in the meta-theory.

> 
>>>
>>>
>>>> We can then show that we can make a G' in F' with the same property, 
>>>> and thus show that there exists a system F'' where we can prove G'.
>>>>
>>>> This is why you simplification doesn't work. In F, we can't convert 
>>>> G into the statement G says that G is unprovable, but we can in F', 
>>>> thus the statement in F' is that G says that G in unprovable in F, 
>>>> and that statement is provable in F'
>>>>
>>>
>>> Likewise for the liar Paradox. Apparently Tarski could prove the Liar 
>>> Paradox in his meta-theory.
>>>
>>>> You don't seem to be able to handle the concept of layers of logic 
>>>> systems.
>>>>
>>>
>>>
>>
> 
> 

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


#12956 — Re: Is this correct Prolog? [ Tarski ]

Fromolcott <polcott2@gmail.com>
Date2022-05-05 21:37 -0500
SubjectRe: Is this correct Prolog? [ Tarski ]
Message-ID<t521m1$u43$1@dont-email.me>
In reply to#12955
On 5/5/2022 9:24 PM, Richard Damon wrote:
> On 5/5/22 1:57 PM, olcott wrote:
>> On 5/4/2022 9:46 PM, Richard Damon wrote:
>>> On 5/4/22 10:30 PM, olcott wrote:
>>>> On 5/3/2022 7:05 AM, Richard Damon wrote:
>>>>> On 5/2/22 11:01 PM, olcott wrote:
>>>>>> On 5/2/2022 9:21 PM, Ben wrote:
>>>>>>> olcott <polcott2@gmail.com> writes:
>>>>>>>
>>>>>>>> On 5/2/2022 6:43 PM, Ben wrote:
>>>>>>>>> Aleksy Grabowski <hurufu@gmail.com> writes:
>>>>>>>
>>>>>>>>>> Thanks for confirmation, that's what exactly what I was trying 
>>>>>>>>>> to tell
>>>>>>>>>> to topic poster in one of my previous posts. Prolog in it's 
>>>>>>>>>> bare form
>>>>>>>>>> is a bad theorem solver. It wasn't designed a such.
>>>>>>>>>>
>>>>>>>>>> If you want to deal with such problems maybe it is better to 
>>>>>>>>>> use Coq
>>>>>>>>>> theorem prover, I've never used it by myself, but it looks 
>>>>>>>>>> like one of
>>>>>>>>>> the best proving assistants out there.
>>>>>>>>>
>>>>>>>>> And indeed there is a fully formalised proof of GIT in Coq 
>>>>>>>>> (though I
>>>>>>>>> think it's the slightly tighter Gödel-Rosser version).
>>>>>>>>
>>>>>>>> It is true that G is not provable.
>>>>>>>
>>>>>>> G is provable.  Proofs abound.  I was pointing out one in a 
>>>>>>> proper proof
>>>>>>> assistant, Coq.
>>>>>>>
>>>>>>
>>>>>> It is OK that you are not a math guy.
>>>>>> If you were a math guy you would understand that if G is provable 
>>>>>> then that makes Gödel totally wrong. G is not Gödel's theorem, it 
>>>>>> is a key element of his theorem.
>>>>>>
>>>>>> Incomplete T means that there exists a φ such that φ is not 
>>>>>> provable or refutable in formal system T.
>>>>>>
>>>>>> Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
>>>>>>
>>>>>>
>>>>>
>>>>> No, G IS provable, just not in the system F that G is described in, 
>>>>> thus F is Incomplete by your definition above.
>>>>>
>>>>> Part of the key of the Godel proof is that while G sort of refers 
>>>>> to itself, it does it in a way that F can't handle, so in F, G 
>>>>> doesn't refer to itself but just "some statement", but in a 'more 
>>>>> advanced' version of F, say F', we can see that relationship, and 
>>>>> show that G must be true, proving it in F', but not in F, thus F is 
>>>>> incomplete.
>>>>>
>>>>
>>>> Tarski's hierarchy of languages.
>>>>
>>>> It only works at a higher level language because the expression of 
>>>> language at the next level is not self-contradictory.
>>>>
>>>> All epistemological antinomies are self-contradictory making them 
>>>> semantically invalid.
>>>>
>>>> In his undefinability proof: (only two pages long)
>>>> https://liarparadox.org/Tarski_275_276.pdf
>>>>
>>>> He defines these two levels as "the theory" and the next higher 
>>>> level is called the "the metatheory".  (see link).
>>>
>>> So we can prove G in the Metatheory, 
>>
>> Yes.
>>
>>> so it is True in the Theory too.
>>>
>>
>> Not at all.
>> In the theory p is self-contradictory thus not a truth bearer.
>> In the meta-theory p is NOT self-contradictory.
> 
> How do you get that.
> 

In Tarski's theory p <is> the formalized liar paradox.

> In the Theory, you can't even tell that G references itself, but is just 
> a statement about mathematics.
> 
>>
>>>> since in this interpretation the sentence x, which contains no 
>>>> specific term of the metatheory, is its o\vn correlate, the proof of 
>>>> the sentence x given in the metatheory can automatically be carried 
>>>> over into the theory itself: the sentence x which is undecidable in 
>>>> the original theory becomes a decidable sentence in the enriched 
>>>> theory.
>>>
>>> But if G is true in the Theory, it is BY DEFINITION not provable in 
>>> the Theory, so the space of the Theory is shown to have a True 
>>> Statement which is not provable, thus the system of the Theory in 
>>> Incomplete.
>>
>> G is self-contradictory on the theory and non self-contradictory in 
>> the meta-theory.
> 
> No, because in the theory, G doesn't even reference itself, so it can't 
> be self-contradictory.
> 

Gödel says:
...We are therefore confronted with a proposition which asserts its own 
unprovability.

> I think you don't even know what G is, but have only read the clift 
> notes edition that actually explain it in the meta-theory.




>>
>>>>
>>>>
>>>>> We can then show that we can make a G' in F' with the same 
>>>>> property, and thus show that there exists a system F'' where we can 
>>>>> prove G'.
>>>>>
>>>>> This is why you simplification doesn't work. In F, we can't convert 
>>>>> G into the statement G says that G is unprovable, but we can in F', 
>>>>> thus the statement in F' is that G says that G in unprovable in F, 
>>>>> and that statement is provable in F'
>>>>>
>>>>
>>>> Likewise for the liar Paradox. Apparently Tarski could prove the 
>>>> Liar Paradox in his meta-theory.
>>>>
>>>>> You don't seem to be able to handle the concept of layers of logic 
>>>>> systems.
>>>>>
>>>>
>>>>
>>>
>>
>>
> 


-- 
Copyright 2022 Pete Olcott "Talent hits a target no one else can hit;
Genius hits a target no one else can see." Arthur Schopenhauer

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


#12958 — Re: Is this correct Prolog? [ Tarski ]

FromRichard Damon <Richard@Damon-Family.org>
Date2022-05-06 07:43 -0400
SubjectRe: Is this correct Prolog? [ Tarski ]
Message-ID<aR7dK.408$Acq9.201@fx13.iad>
In reply to#12956
On 5/5/22 10:37 PM, olcott wrote:
> On 5/5/2022 9:24 PM, Richard Damon wrote:
>> On 5/5/22 1:57 PM, olcott wrote:

>>> G is self-contradictory on the theory and non self-contradictory in 
>>> the meta-theory.
>>
>> No, because in the theory, G doesn't even reference itself, so it 
>> can't be self-contradictory.
>>
> 
> Gödel says:
> ...We are therefore confronted with a proposition which asserts its own 
> unprovability.
> 

Which is Godel making a comment about G, and not a statement in G itself.

G does not directly mention itself in the Theory.

>> I think you don't even know what G is, but have only read the clift 
>> notes edition that actually explain it in the meta-theory.
> 
> 

So this comment of mine is now proven.

And you have prooved to be a Liar and an idiot, as you abolutely don't 
know what you are talking about.

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


#12959 — Re: Is this correct Prolog? [ Tarski ]

Fromolcott <polcott2@gmail.com>
Date2022-05-06 15:29 -0500
SubjectRe: Is this correct Prolog? [ Tarski ]
Message-ID<t540g5$jst$1@dont-email.me>
In reply to#12958
On 5/6/2022 6:43 AM, Richard Damon wrote:
> 
> On 5/5/22 10:37 PM, olcott wrote:
>> On 5/5/2022 9:24 PM, Richard Damon wrote:
>>> On 5/5/22 1:57 PM, olcott wrote:
> 
>>>> G is self-contradictory on the theory and non self-contradictory in 
>>>> the meta-theory.
>>>
>>> No, because in the theory, G doesn't even reference itself, so it 
>>> can't be self-contradictory.
>>>
>>
>> Gödel says:
>> ...We are therefore confronted with a proposition which asserts its 
>> own unprovability.
>>
> 
> Which is Godel making a comment about G, and not a statement in G itself.
> 
> G does not directly mention itself in the Theory.

Gödel says that it does with dodgy words that also says that it does not.

15 In spite of appearances, there is nothing circular about such a 
proposition, since it begins by asserting the unprovability of a wholly 
determinate formula (namely the q-th in the alphabetical arrangement 
with a definite substitution), and only subsequently (and in some way by 
accident)does it emerge that this formula is precisely that by which the 
proposition was itself expressed.END:(Gödel 1931:39-41)

Gödel's footnote 15 is dodgy in that although it denies the circularity 
of his proposition he affirms its circularity in the same paragraph that 
he denies it:

Removing the dodgy words from the above.
a proposition...begins by asserting the unprovability of a wholly 
determinate formula...this formula is precisely that by which the 
proposition was itself expressed.

Paraphrasing the above using less clumsy words:
a proposition asserts the unprovability of a formula that expresses this 
same proposition

https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence 


> 
>>> I think you don't even know what G is, but have only read the clift 
>>> notes edition that actually explain it in the meta-theory.
>>
>>
> 
> So this comment of mine is now proven.
> 
> And you have prooved to be a Liar and an idiot, as you abolutely don't 
> know what you are talking about.


-- 
Copyright 2022 Pete Olcott "Talent hits a target no one else can hit;
Genius hits a target no one else can see." Arthur Schopenhauer

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


#12910

FromBen <ben.usenet@bsb.me.uk>
Date2022-05-03 15:59 +0100
Message-ID<874k26slv4.fsf@bsb.me.uk>
In reply to#12907
olcott <polcott2@gmail.com> writes:

> On 5/2/2022 9:21 PM, Ben wrote:
>> olcott <polcott2@gmail.com> writes:
>> 
>>> On 5/2/2022 6:43 PM, Ben wrote:
>>>> Aleksy Grabowski <hurufu@gmail.com> writes:
>> 
>>>>> Thanks for confirmation, that's what exactly what I was trying to tell
>>>>> to topic poster in one of my previous posts. Prolog in it's bare form
>>>>> is a bad theorem solver. It wasn't designed a such.
>>>>>
>>>>> If you want to deal with such problems maybe it is better to use Coq
>>>>> theorem prover, I've never used it by myself, but it looks like one of
>>>>> the best proving assistants out there.
>>>>
>>>> And indeed there is a fully formalised proof of GIT in Coq (though I
>>>> think it's the slightly tighter Gödel-Rosser version).
>>>
>>> It is true that G is not provable.
>> G is provable.  Proofs abound.  I was pointing out one in a proper proof
>> assistant, Coq.
>
> It is OK that you are not a math guy.

You are not a math guy.  I am.

> If you were a math guy you would understand that if G is provable then
> that makes Gödel totally wrong. G is not Gödel's theorem, it is a key
> element of his theorem.

No.  G is provable.  Though I did make a mistake -- the link was to a
proof of G-RIT not G.

How are you getting on with E and specifying P?  Have you given up?

-- 
Ben.
"le génie humain a des limites, quand la bêtise humaine n’en a pas"
Alexandre Dumas (fils)

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


#12911

FromAndré G. Isaak <agisaak@gm.invalid>
Date2022-05-03 09:18 -0600
Message-ID<t4rh4c$t51$1@dont-email.me>
In reply to#12905
On 2022-05-02 18:57, olcott wrote:
> On 5/2/2022 6:43 PM, Ben wrote:
>> Aleksy Grabowski <hurufu@gmail.com> writes:
>>
>>>> IF you are defining that your logic system is limited to what Prolog 
>>>> can "Prove", that is fine. Just realize that you have just defined 
>>>> that your
>>>> logic system can't handle a lot of the real problems in the world, 
>>>> and in particular, it is very limited in the mathematics it can handle.
>>>> I am pretty sure that Prolog is NOT up to handling the logic needed to
>>>> handle the mathematics needed to express Godel's G, or the Halting 
>>>> Problem.
>>>> Thus, your "Proof" that these Theorems are "Wrong" is incorrect, you
>>>> have only proven that your limited logic system can't reach them in 
>>>> expressibility.
>>>
>>> Thanks for confirmation, that's what exactly what I was trying to tell
>>> to topic poster in one of my previous posts. Prolog in it's bare form
>>> is a bad theorem solver. It wasn't designed a such.
>>>
>>> If you want to deal with such problems maybe it is better to use Coq
>>> theorem prover, I've never used it by myself, but it looks like one of
>>> the best proving assistants out there.
>>
>> And indeed there is a fully formalised proof of GIT in Coq (though I
>> think it's the slightly tighter Gödel-Rosser version).
>>
> 
> It is true that G is not provable. G is not provable because it is 
> semantically incorrect in the exactly same way that the Liar Paradox is 
> semantically incorrect.
> 
> Gödel says:
> 14 Every epistemological antinomy can likewise be used for a similar 
> undecidability proof
> 
> André denied this six times yesterday
> The Liar Paradox is an epistemological antinomy, thus can likewise be 
> used for a similar undecidability proof.

No. The Liar can be used to construct an *identical* proof. Other 
antinomies could be used for similar proofs. He's already talking about 
The Liar.

> Which means that the Liar Paradox is sufficiently equivalent to Gödel's 
> G. Which means if the basic mechanism of epistemological antinomy is 
> shown to be semantically incorrect then Gödel's G is shown to be 
> semantically incorrect.

You have some serious reading comprehension problems. I never denied the 
things Gödel wrote. I denied your conclusion because it does not follow.

Gödel starts by claiming there is a close relationship (*not* 
equivalence) between one particular antinomy, The Liar, and his G.

He then states that similar proofs could be constructed using any antinomy.

That entails that other antinomies could be used to construct similar 
proofs involving a similar close relation (again, *not* equivalence).

Gödel never claims *any* antinomy is equivalent to his G. Merely that a 
close relationship holds.

And all my comments concerned exactly what that relationship is.

André

-- 
To email remove 'invalid' & replace 'gm' with well known Google mail 
service.

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


Page 3 of 9 — ← Prev page 1 2 [3] 4 5 6 7 8 9  Next page →

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


csiph-web