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

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

Re: How teach logic? [The Jokes] (Re: People that have a very shallow understanding of these things)

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

This discussion starts older than the indexed window; earlier articles aren't shown. The article labeled Started by below is the oldest one visible, not the original post.

Contents

  Re: How teach logic? [The Jokes] (Re: People that have a very shallow understanding of these things) olcott <polcott333@gmail.com> - 2025-11-18 16:02 -0600
    Enjoying some logic under a shadowy tree? (Was: How teach logic? [The Jokes]) Mild Shock <janburse@fastmail.fm> - 2025-11-18 23:15 +0100
      Re: Enjoying some logic under a shadowy tree? (Was: How teach logic? [The Jokes]) olcott <polcott333@gmail.com> - 2025-11-18 16:54 -0600
        What did you do before 2001 ? (Was: Enjoying some logic under a shadowy tree?) Mild Shock <janburse@fastmail.fm> - 2025-11-19 09:50 +0100
          What are top ten books in set theory? (Re: What did you do before 2001 ?) Mild Shock <janburse@fastmail.fm> - 2025-11-19 10:16 +0100
            Slim Fermats Last Theorem (FLT) only for Lean4? (Was: What are top ten books in set theory?) Mild Shock <janburse@fastmail.fm> - 2025-11-19 11:14 +0100
    Re: How teach logic? [The Jokes] (Re: People that have a very shallow understanding of these things) "Chris M. Thomasson" <chris.m.thomasson.1@gmail.com> - 2025-11-18 15:15 -0800

#15027 — Re: How teach logic? [The Jokes] (Re: People that have a very shallow understanding of these things)

On 11/18/2025 3:46 PM, Mild Shock wrote:
<big snip>

*I remember you in the Prolog Group*
*I remember you in the Prolog Group*
*I remember you in the Prolog Group*

The Liar Paradox formalized in the Prolog Programming language

This sentence is not true.
It is not true about what?
It is not true about being not true.
It is not true about being not true about what?
It is not true about being not true about being not true.
Oh I see you are stuck in a loop!


This is formalized in the Prolog programming language
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.

Failing an occurs check seems to mean that the
resolution of an expression remains stuck in
an infinite loop. Just as the formalized Prolog
determines that there is a cycle in the directed
graph of the evaluation sequence of LP the simple
English proves that the Liar Paradox never gets
to the point. It has merely been semantically
unsound all these years.

-- 
Copyright 2025 Olcott

My 28 year goal has been to make
"true on the basis of meaning" computable.

[toc] | [next] | [standalone]

#15029 — Enjoying some logic under a shadowy tree? (Was: How teach logic? [The Jokes])

Hi,

So you say I was your logic teacher? I doubt
so. Who was your logic teacher from the cradle
to the appearance of the internet, when

you still had to carry heavy paper books, while
visiting the lake front in summer, looking for
a shadowy tree, and the enjoying some logic?

What books did you read ? What people did you know ?

Bye

olcott schrieb:
> On 11/18/2025 3:46 PM, Mild Shock wrote:
> <big snip>
> 
> *I remember you in the Prolog Group*
> *I remember you in the Prolog Group*
> *I remember you in the Prolog Group*
> 
> The Liar Paradox formalized in the Prolog Programming language
> 
> This sentence is not true.
> It is not true about what?
> It is not true about being not true.
> It is not true about being not true about what?
> It is not true about being not true about being not true.
> Oh I see you are stuck in a loop!
> 
> 
> This is formalized in the Prolog programming language
> ?- LP = not(true(LP)).
> LP = not(true(LP)).
> ?- unify_with_occurs_check(LP, not(true(LP))).
> false.
> 
> Failing an occurs check seems to mean that the
> resolution of an expression remains stuck in
> an infinite loop. Just as the formalized Prolog
> determines that there is a cycle in the directed
> graph of the evaluation sequence of LP the simple
> English proves that the Liar Paradox never gets
> to the point. It has merely been semantically
> unsound all these years.
> 

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

#15031 — Re: Enjoying some logic under a shadowy tree? (Was: How teach logic? [The Jokes])

On 11/18/2025 4:15 PM, Mild Shock wrote:
> Hi,
> 
> So you say I was your logic teacher? I doubt
> so. Who was your logic teacher from the cradle
> to the appearance of the internet, when
> 
> you still had to carry heavy paper books, while
> visiting the lake front in summer, looking for
> a shadowy tree, and the enjoying some logic?
> 
> What books did you read ? What people did you know ?
> 
> Bye
> 

I Learned FOL from Wikipedia.

I know PhD computer science professor Eric Hehner
though many email conversations.

This was the only book that I read on logic.
https://www.amazon.com/Formal-Semantics-Cambridge-Textbooks-Linguistics/dp/0521376106

I have been a software engineer since 1984.

I am the creator of Google[Olcott's Minimal Type Theory]

> olcott schrieb:
>> On 11/18/2025 3:46 PM, Mild Shock wrote:
>> <big snip>
>>
>> *I remember you in the Prolog Group*
>> *I remember you in the Prolog Group*
>> *I remember you in the Prolog Group*
>>
>> The Liar Paradox formalized in the Prolog Programming language
>>
>> This sentence is not true.
>> It is not true about what?
>> It is not true about being not true.
>> It is not true about being not true about what?
>> It is not true about being not true about being not true.
>> Oh I see you are stuck in a loop!
>>
>>
>> This is formalized in the Prolog programming language
>> ?- LP = not(true(LP)).
>> LP = not(true(LP)).
>> ?- unify_with_occurs_check(LP, not(true(LP))).
>> false.
>>
>> Failing an occurs check seems to mean that the
>> resolution of an expression remains stuck in
>> an infinite loop. Just as the formalized Prolog
>> determines that there is a cycle in the directed
>> graph of the evaluation sequence of LP the simple
>> English proves that the Liar Paradox never gets
>> to the point. It has merely been semantically
>> unsound all these years.
>>
> 


-- 
Copyright 2025 Olcott

My 28 year goal has been to make
"true on the basis of meaning" computable.

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

#15033 — What did you do before 2001 ? (Was: Enjoying some logic under a shadowy tree?)

Hi,

Wikipedia only exists since 2001. How did people
learn Logic before the new millenium? Seems you
have been alive before 2001 already,

when you are a software engineer since 1984. No
logic for Acyclic Ozelot before 2001. Did really
only bring Wikipedia, a secondary reference,

logic to you. No primary sources of logic?

Bye

olcott schrieb:
> 
> I Learned FOL from Wikipedia. 
 > I have been a software engineer since 1984.

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

#15034 — What are top ten books in set theory? (Re: What did you do before 2001 ?)

Hi,

How it started, DeepSeek:

me: What are top ten books in set theory?
ai: bla bla
ai: Classic Set Theory: For Guided Independent Study by Derek C. Goldrei

How its going, ChatGPT:

me: What are top ten books in set theory?
ai: bla bla
ai: The Incomparable Axioms — Koellner (more philosophical, modern)

me: Nice try, I don't find "The Incomparable Axioms —
Koellner", you halucinated that

ai: You’re right — I made a mistake. I hallucinated a
book title. Sorry about that.

ai: Peter Koellner has written influential papers and
a thesis/lecture notes, but there is no book titled
The Incomparable Axioms by Koellner that I can find.

The Search for New Axioms
https://dspace.mit.edu/bitstream/handle/1721.1/7989/53014647-MIT.pdf

LoL

Bye

Mild Shock schrieb:
> Hi,
> 
> Wikipedia only exists since 2001. How did people
> learn Logic before the new millenium? Seems you
> have been alive before 2001 already,
> 
> when you are a software engineer since 1984. No
> logic for Acyclic Ozelot before 2001. Did really
> only bring Wikipedia, a secondary reference,
> 
> logic to you. No primary sources of logic?
> 
> Bye
> 
> olcott schrieb:
>>
>> I Learned FOL from Wikipedia. 
>  > I have been a software engineer since 1984.

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

#15035 — Slim Fermats Last Theorem (FLT) only for Lean4? (Was: What are top ten books in set theory?)

Hi,

Is there a Slim Fermats Last Theorem (FLT) but
only for Lean4? There is a new proof:

We formalize a complete proof of the regular
case of Fermat's Last Theorem in the Lean4
theorem prover. Our formalization includes a
proof of Kummer's lemma, that is the main
obstruction to Fermat's Last Theorem for
regular primes. Rather than following the
modern proof of Kummer's lemma via class
field theory, we prove it by using Hilbert's
Theorems 90-94 in a way that is more
amenable to formalization.
https://arxiv.org/abs/2410.01466v3

Is this also available for Rocq or Isabelle/HOL.
In as far I feel with ChatGPTs invention of
a set theory book:

 > ai: The Incomparable Axioms — Koellner
(more philosophical, modern)

If we have to axiom systems A and B, it is
often easy to invoke proof theory and then
show A ⊆ B or B ⊆ A. Trouble might start if
we want to show A ⊈ B and B ⊈ A,

this traditional fell into the category of
model theory, but modern proof assistants might
be better off maybe. Such a proof could be
a pebble game, as in EF games,

or even some things that go beyond EF games.
Now for the question whether Rocq or Isabelle/HOL
has also a proof, the comparability of Axioms
is somehow aggravated, when different proof

systems have different foundations. What
we then need to compare is F+A with G+B,
where F and G are the varying foundations.
Who said that logic is easy and beautiful?

Bye

Mild Shock schrieb:
> Hi,
> 
> How it started, DeepSeek:
> 
> me: What are top ten books in set theory?
> ai: bla bla
> ai: Classic Set Theory: For Guided Independent Study by Derek C. Goldrei
> 
> How its going, ChatGPT:
> 
> me: What are top ten books in set theory?
> ai: bla bla
> ai: The Incomparable Axioms — Koellner (more philosophical, modern)
> 
> me: Nice try, I don't find "The Incomparable Axioms —
> Koellner", you halucinated that
> 
> ai: You’re right — I made a mistake. I hallucinated a
> book title. Sorry about that.
> 
> ai: Peter Koellner has written influential papers and
> a thesis/lecture notes, but there is no book titled
> The Incomparable Axioms by Koellner that I can find.
> 
> The Search for New Axioms
> https://dspace.mit.edu/bitstream/handle/1721.1/7989/53014647-MIT.pdf
> 
> LoL
> 
> Bye
> 
> Mild Shock schrieb:
>> Hi,
>>
>> Wikipedia only exists since 2001. How did people
>> learn Logic before the new millenium? Seems you
>> have been alive before 2001 already,
>>
>> when you are a software engineer since 1984. No
>> logic for Acyclic Ozelot before 2001. Did really
>> only bring Wikipedia, a secondary reference,
>>
>> logic to you. No primary sources of logic?
>>
>> Bye
>>
>> olcott schrieb:
>>>
>>> I Learned FOL from Wikipedia. 
>>  > I have been a software engineer since 1984.
> 

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

#15032

On 11/18/2025 2:02 PM, olcott wrote:
> On 11/18/2025 3:46 PM, Mild Shock wrote:
> <big snip>
> 
> *I remember you in the Prolog Group*
> *I remember you in the Prolog Group*
> *I remember you in the Prolog Group*
> 
> The Liar Paradox formalized in the Prolog Programming language
> 
> This sentence is not true.
> It is not true about what?
> It is not true about being not true.
> It is not true about being not true about what?
> It is not true about being not true about being not true.
> Oh I see you are stuck in a loop!
[...]

DD says, I can halt, or not halt... That is 100% true about DD. So, lets 
explore both paths, and fin the sim when they are _both_ hit. Actually, 
the following models your DD:
____________________________
1 HOME
5 PRINT "ct_dr_fuzz lol. ;^)"
6 P0 = 0
7 P1 = 0

10 REM Fuzzer... ;^)
20 A$ = "NOPE!"
30 IF RND(1) < .5 THEN A$ = "YES"

100 REM INPUT "Shall DD halt or not? " ; A$
110 PRINT "Shall DD halt or not? " ; A$
200 IF A$ = "YES" GOTO 666
300 P0 = P0 + 1
400 IF P0 > 0 AND P1 > 0 GOTO 1000
500 GOTO 10

666 PRINT "OK!"
667 P1 = P1 + 1
700 PRINT "NON_HALT P0 = "; P0
710 PRINT "HALT P1 = "; P1
720 IF P0 > 0 AND P1 > 0 GOTO 1000
730 PRINT "ALL PATHS FAILED TO BE HIT!"
740 GOTO 10


1000
1010 PRINT "FIN... All paths hit."
1020 PRINT "NON_HALT P0 = "; P0
1030 PRINT "HALT P1 = "; P1
____________________________

Fair enough?

[toc] | [prev] | [standalone]

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

csiph-web