Groups | Search | Server Info | Login | Register

Groups > sci.logic > #340862

Old School Logicians waste time with compare/3 ? (Was: Gold medal waiting for the crankiest of cranks)

Show all headers | View raw

Hi,

Did the old School Logicians waste time
with compare/3 ? I guess no:

Ernst Specker, my beloved Professor, and
Dana Scott made only a partial order. A
partial order might have transitivity

of (<') lacking:

"Scott's model construction is in fact
closely related to Specker's but there
is a subtle difference in the notion of
tree that they use. In fact neither of
them formulate their notion of tree in
terms of graphs but rather in terms of
what it will be convenient here to
call tree-partial-orderings."

See here:

NON-WELL-FOUNDED SETS
Peter Aczel - 1988
https://les-mathematiques.net/vanilla/uploads/editor/fh/v4pi6qyxfbel.pdf

There is also the notion of co-well-
foundedness, something like Noetherian but
up side down, i.e. certain ascending
chains stabilizing.

Bye

Mild Shock schrieb:
> 
> 
>  > I guess there is a bug in preparing flat terms vector
> 
> I give you a gold medal 🥇, if you can prove a
> compare_index/3 correct that uses this rule. It
> was already shown impossible by Matt Carlson.
> 
> There are alternative approaches that can reach
> transitivity, but do not use the below step
> inside some compare_index/3.
> 
> compare_term_args(I, C, X, Y, A, H):-
>          arg(I, X, K),
>          arg(I, Y, L),
>          !,
>          compare_index(D, K, L, A, H),
>          (    D = (=) ->
>              I0 is I + 1,
>              compare_term_args(I0, C, X, Y, A, H)
>          ;    C = D
>          ).
> compare_term_args(_ ,= , _, _, _, _).
> 
> Maybe there is a grain of salt of invoking the
> Axiom of Choice (AC) in some previous posts.
> Although the Axiom of Choice is not needed for
> 
> finite sets, they have anyway some choice.
> 
> BTW: When Peter Aczel writes ZFC-, he then
> means ZFC without AC, right? But he doesn’t
> show some compare/3 .
> 
> Mild Shock schrieb:
>> Hi,
>>
>> Take this exercise. Exercise 4.1 Draw the tree
>> represented by the term n1(n2(n4),n3(n5,n6)).
>> https://book.simply-logical.space/src/text/2_part_ii/4.1.html
>>
>> Maybe there was a plan that SWISH can draw trees,
>> and it could be that something was implemented as well.
>>
>> But I don't see anything dynamic working on the
>> above web site link. Next challenge for Simply Logical,
>>
>> in another life. Draw a rational tree.
>> The Prolog system has them:
>>
>> /* SWI-Prolog 9.3.26 */
>> ?- X = a(Y,_), Y = b(X,_).
>> X = a(b(X, _A), _),
>> Y = b(X, _A).
>>
>> Bye

Back to sci.logic | Previous | Next — Previous in thread | Next in thread | Find similar

Thread

The Prolog Community is extremly embarrassing (Re: Prolog totally missed the AI Boom) Mild Shock <janburse@fastmail.fm> - 2025-07-25 21:28 +0200
  Non-Wellfounded and Russell Paradox, what is your opinion? (Re: The Prolog Community is extremly embarrassing) Mild Shock <janburse@fastmail.fm> - 2025-07-25 21:37 +0200
    Unfinished Bimbo Stuff: 4.1. Trees as terms (Was: Non-Wellfounded and Russell Paradox, what is your opinion?) Mild Shock <janburse@fastmail.fm> - 2025-07-25 23:03 +0200
      Gold medal waiting for the crankiest of cranks (Re: Unfinished Bimbo Stuff: 4.1. Trees as terms) Mild Shock <janburse@fastmail.fm> - 2025-07-26 16:12 +0200
        Old School Logicians waste time with compare/3 ? (Was: Gold medal waiting for the crankiest of cranks) Mild Shock <janburse@fastmail.fm> - 2025-07-26 16:18 +0200
          RIs compare/3 a sunflower study subject? (e: Old School Logicians waste time with compare/3 ?) Mild Shock <janburse@fastmail.fm> - 2025-07-26 16:37 +0200

csiph-web