On Tuesday, 30 August 2022 at 00:15:20 UTC+2, Ben Bacarisse wrote:
> Skep Dick <skepd...@gmail.com> writes:
>
> > On Monday, 29 August 2022 at 17:27:06 UTC+2, Ben Bacarisse wrote:
> >> So it seems. As you say the 0th integer greater than 4 is 4.
> >> Apparently at least one of "ALL the integers greater than 4" is 4 --
> >> specifically the one indexed by 0.
> >> greater than 4" includes 4 as the 0th indexed element (other than you)?
>
> > So you STILL refuse to tell me whether you think the 1st successor to
> > 0 is "succ zero" or "succ succ zero". And you STILL refuse to tell me
> > whether you think the 0th successor to 0 is "zero" or "succ zero".
> >
> > I guess we'll never know whether **TO YOU** ALL the successors to zero
> > includes, or excludes zero itself...
> Nope, and I don't think that the 0th integer greater than 4 is 4 either!

I don’t think it is a matter of what you think. It is a matter of whether the theorem holds given some axioms (of my arbitrary choosing).

You may not like the implications of said axioms/definitions but why should mathematicians care?

On Tuesday, 30 August 2022 at 07:12:41 UTC+2, dklei...@gmail.com wrote:
> On Monday, August 29, 2022 at 3:13:22 AM UTC-7, skepd...@gmail.com wrote:
> > On Monday, 29 August 2022 at 02:08:12 UTC+2, dklei...@gmail.com wrote:
> > > Reflexive language isn't even good linguistics. It has nothing to do with
> > > mathematics.
> > I have no idea what you mean by "good linguistics", but I sure as hell understand what reflection in formal languages is and how it works.
> >
> > Perhaps you want to insist that programming language theory is not
> > Mathematics; or linguistics when it's actually both!
> >
> Well, a programming language theory is a mathematical possibility. I
> have never seen one. Reference?
It literally goes by the name “Programming Language Theory”..

> > > You have that backwards. In the most natural definition
> > I think I have that quite forward, thank you. I am aware of
> > multitude of definitions. I have no idea which your aesthetic
> > sensibilities consider "most natural".
> >
> Like most mathematicians I use "natural" in the meta-language
> in an Occam-like sense. Of two propositions the more natural
> one is one involving the least machinery to define.
> >
> > Maybe you want to formalize your "most natural" proposition?
> > > natural numbers the first natural number is the empty set
> > Oh, wow! So the 1st number is not even the number 1 itself!?!
> > The "first" number is a set! An empty one at that.
> >
> > There's nothing natural about your definition of "natural".
> >
> > Hard to imagine anything simpler.
Your lack of imagination is profound.

> > and the successor (to any natural number) is the union of
> > > the number and the set whose only member is the number.
> > If some technical mumbo jumbo is your idea of "natural"
> > then... the technical definition that is "most natural" to me is
> > a +1 monoid with 1 as the identity element.
> >
> After you have defined "monoid", "identity" and probably more
> stuff. Lots more machinery.
I guess you didn’t get the sarcasm.

The simplest definition of the first natural number is …. “The first natural number.”
The simplest formalization/representation of “The first natural number” is … whatever.

1. 0. A.

Pick a symbol.

> > > Above I gave a meta-language definition of natural numbers.
> >
> > No, you didn't. You gave a set-theoretic definition of the natural
> > numbers.
> >
> > I used set-theory in the meta-language.
> >
> > But if set theory is just the "meta language" then what language
> > are you using to DO mathematics in ?!?
> >
> None. Mathematics is not bound to the language it is expressed
> in. Many mathematicians, like myself, think mostly in pictures.
That is called geometry (if the pictures don’t move) and topology (if they do).

> Computation is a small rarely visited corner of mathematics.
Eeeh… toposes/programming languages are models of computation.

Some would even consider computations such as homotopy types to be the foundation of mathematics.

On Tuesday, August 30, 2022 at 2:52:16 AM UTC-7, skepd...@gmail.com wrote:
> On Tuesday, 30 August 2022 at 07:12:41 UTC+2, dklei...@gmail.com wrote:
> > On Monday, August 29, 2022 at 3:13:22 AM UTC-7, skepd...@gmail.com wrote:
> > > On Monday, 29 August 2022 at 02:08:12 UTC+2, dklei...@gmail.com wrote:
> > > > Reflexive language isn't even good linguistics. It has nothing to do with
> > > > mathematics.
> > > I have no idea what you mean by "good linguistics", but I sure as hell understand what reflection in formal languages is and how it works.
> > >
> > > Perhaps you want to insist that programming language theory is not
> > > Mathematics; or linguistics when it's actually both!
> > >
> > Well, a programming language theory is a mathematical possibility. I
> > have never seen one. Reference?
> It literally goes by the name “Programming Language Theory”.
> > > > You have that backwards. In the most natural definition
> > > I think I have that quite forward, thank you. I am aware of
> > > multitude of definitions. I have no idea which your aesthetic
> > > sensibilities consider "most natural".
> > >
> > Like most mathematicians I use "natural" in the meta-language
> > in an Occam-like sense. Of two propositions the more natural
> > one is one involving the least machinery to define.
> > >
> > > Maybe you want to formalize your "most natural" proposition?
> > > > natural numbers the first natural number is the empty set
> > > Oh, wow! So the 1st number is not even the number 1 itself!?!
> > > The "first" number is a set! An empty one at that.
> > >
> > > There's nothing natural about your definition of "natural".
> > >
> > > Hard to imagine anything simpler.
> Your lack of imagination is profound.
> > > and the successor (to any natural number) is the union of
> > > > the number and the set whose only member is the number.
> > > If some technical mumbo jumbo is your idea of "natural"
> > > then... the technical definition that is "most natural" to me is
> > > a +1 monoid with 1 as the identity element.
> > >
> > After you have defined "monoid", "identity" and probably more
> > stuff. Lots more machinery.
> I guess you didn’t get the sarcasm.
>
> The simplest definition of the first natural number is …. “The first natural number.”
> The simplest formalization/representation of “The first natural number” is … whatever.
>
> 1. 0. A.
>
> Pick a symbol.
> > > > Above I gave a meta-language definition of natural numbers.
> > >
> > > No, you didn't. You gave a set-theoretic definition of the natural
> > > numbers.
> > >
> > > I used set-theory in the meta-language.
> > >
> > > But if set theory is just the "meta language" then what language
> > > are you using to DO mathematics in ?!?
> > >
> > None. Mathematics is not bound to the language it is expressed
> > in. Many mathematicians, like myself, think mostly in pictures.
> That is called geometry (if the pictures don’t move) and topology (if they do).
> > Computation is a small rarely visited corner of mathematics.
> Eeeh… toposes/programming languages are models of computation.
>
> Some would even consider computations such as homotopy types to be the foundation of mathematics.

I wonder why you haven't actually said that you are basing your
theories on category theory. I am aware that category theory has
been suggested as a better foundation than set theory, But I have
never bothered to follow through the arguments because set theory
is adequate for what I do (actually "did", I've been retired a long time.

There is a lot of words out there called the theory of programming
languages but it is not mathematical theory. I observe that the
Wikipedia article doesn't even consider assembly language. I fear
this a a theory only in the meta-language sense.

On 8/30/2022 12:25 PM, dklei...@gmail.com wrote:
> On Tuesday, August 30, 2022 at 2:52:16 AM UTC-7, skepd...@gmail.com wrote:
>> On Tuesday, 30 August 2022 at 07:12:41 UTC+2, dklei...@gmail.com wrote:
>>> On Monday, August 29, 2022 at 3:13:22 AM UTC-7, skepd...@gmail.com wrote:
>>>> On Monday, 29 August 2022 at 02:08:12 UTC+2, dklei...@gmail.com wrote:
>>>>> Reflexive language isn't even good linguistics. It has nothing to do with
>>>>> mathematics.
>>>> I have no idea what you mean by "good linguistics", but I sure as hell understand what reflection in formal languages is and how it works.
>>>>
>>>> Perhaps you want to insist that programming language theory is not
>>>> Mathematics; or linguistics when it's actually both!
>>>>
>>> Well, a programming language theory is a mathematical possibility. I
>>> have never seen one. Reference?
>> It literally goes by the name “Programming Language Theory”.
>>>>> You have that backwards. In the most natural definition
>>>> I think I have that quite forward, thank you. I am aware of
>>>> multitude of definitions. I have no idea which your aesthetic
>>>> sensibilities consider "most natural".
>>>>
>>> Like most mathematicians I use "natural" in the meta-language
>>> in an Occam-like sense. Of two propositions the more natural
>>> one is one involving the least machinery to define.
>>>>
>>>> Maybe you want to formalize your "most natural" proposition?
>>>>> natural numbers the first natural number is the empty set
>>>> Oh, wow! So the 1st number is not even the number 1 itself!?!
>>>> The "first" number is a set! An empty one at that.
>>>>
>>>> There's nothing natural about your definition of "natural".
>>>>
>>>> Hard to imagine anything simpler.
>> Your lack of imagination is profound.
>>>> and the successor (to any natural number) is the union of
>>>>> the number and the set whose only member is the number.
>>>> If some technical mumbo jumbo is your idea of "natural"
>>>> then... the technical definition that is "most natural" to me is
>>>> a +1 monoid with 1 as the identity element.
>>>>
>>> After you have defined "monoid", "identity" and probably more
>>> stuff. Lots more machinery.
>> I guess you didn’t get the sarcasm.
>>
>> The simplest definition of the first natural number is …. “The first natural number.”
>> The simplest formalization/representation of “The first natural number” is … whatever.
>>
>> 1. 0. A.
>>
>> Pick a symbol.
>>>>> Above I gave a meta-language definition of natural numbers.
>>>>
>>>> No, you didn't. You gave a set-theoretic definition of the natural
>>>> numbers.
>>>>
>>>> I used set-theory in the meta-language.
>>>>
>>>> But if set theory is just the "meta language" then what language
>>>> are you using to DO mathematics in ?!?
>>>>
>>> None. Mathematics is not bound to the language it is expressed
>>> in. Many mathematicians, like myself, think mostly in pictures.
>> That is called geometry (if the pictures don’t move) and topology (if they do).
>>> Computation is a small rarely visited corner of mathematics.
>> Eeeh… toposes/programming languages are models of computation.
>>
>> Some would even consider computations such as homotopy types to be the foundation of mathematics.
>
> I wonder why you haven't actually said that you are basing your
> theories on category theory. I am aware that category theory has
> been suggested as a better foundation than set theory, But I have
> never bothered to follow through the arguments because set theory
> is adequate for what I do (actually "did", I've been retired a long time.
>
> There is a lot of words out there called the theory of programming
> languages but it is not mathematical theory. I observe that the
> Wikipedia article doesn't even consider assembly language. I fear
> this a a theory only in the meta-language sense.
Something slightly off topic that might interest you: Steve Crocker was
a CS graduate student in the late 1960s. When he finished, he went to
DARPA as a program manager where he was involved with networks, speech
understanding systems, and a few other things. At UCLA he became
interested in formal methods applied to programs and programming
languages. The driving motivation for research in these areas was to
find ways to develop secure software and PROVE it secure. Most of the
efforts first tried to handle programs written in high level languages
and, when that proved too difficult, motivated the invention of
"logical" specification languages where the translation from
representation language to theorems was straightforward and amenable to
work with theorem provers.
Steve went in a different direction when he did his dissertation: he was
going to prove some things about real code written for the Honeywell
516. There were several points to be noted: 1) the code was in assembly
language, 2) it was interrupt driven for the most part, 3) the code was
self modifying!! I think that code was from an early development for the
IMP (Intermediate Message Processor) used as the store and forward
agents for the early research net and for connections to the host computers.
So here was one of the few (very few) attempts to formalize machine
actions and the raw programs they ran. I believe that Steve's approach
was called "State Deltas" where there was a change operator that could
specify changes to machine state and rules for telescoping sequences of
changes to more compact representations and easier (simpler?) to check
current state properties.
This fascinating work like so much of that done in the field of program
language semantics and property assurance has not had a major impact.
For industrial use, the languages and language processors (compilers)
could not be changed to save a nanosecond here and there - they would
need to recertify whatever changed. Steve, in a sense finessed that
problem since there were no tools between the program and runtime; he
was in the business of validating raw machine code, i.e., programs in
their most scruffy form. It always seemed to me something like trying to
put a leash on a hyena and taking it to a dog obedience class - my money
was on the hyena.
--
Jeff Barnett

On Tuesday, August 30, 2022 at 12:35:14 PM UTC-7, Jeff Barnett wrote:
> On 8/30/2022 12:25 PM, dklei...@gmail.com wrote:
> > On Tuesday, August 30, 2022 at 2:52:16 AM UTC-7, skepd...@gmail.com wrote:
> >> On Tuesday, 30 August 2022 at 07:12:41 UTC+2, dklei...@gmail.com wrote:
> >>> On Monday, August 29, 2022 at 3:13:22 AM UTC-7, skepd...@gmail.com wrote:
> >>>> On Monday, 29 August 2022 at 02:08:12 UTC+2, dklei...@gmail.com wrote:
> >>>>> Reflexive language isn't even good linguistics. It has nothing to do with
> >>>>> mathematics.
> >>>> I have no idea what you mean by "good linguistics", but I sure as hell understand what reflection in formal languages is and how it works.
> >>>>
> >>>> Perhaps you want to insist that programming language theory is not
> >>>> Mathematics; or linguistics when it's actually both!
> >>>>
> >>> Well, a programming language theory is a mathematical possibility. I
> >>> have never seen one. Reference?
> >> It literally goes by the name “Programming Language Theory”.
> >>>>> You have that backwards. In the most natural definition
> >>>> I think I have that quite forward, thank you. I am aware of
> >>>> multitude of definitions. I have no idea which your aesthetic
> >>>> sensibilities consider "most natural".
> >>>>
> >>> Like most mathematicians I use "natural" in the meta-language
> >>> in an Occam-like sense. Of two propositions the more natural
> >>> one is one involving the least machinery to define.
> >>>>
> >>>> Maybe you want to formalize your "most natural" proposition?
> >>>>> natural numbers the first natural number is the empty set
> >>>> Oh, wow! So the 1st number is not even the number 1 itself!?!
> >>>> The "first" number is a set! An empty one at that.
> >>>>
> >>>> There's nothing natural about your definition of "natural".
> >>>>
> >>>> Hard to imagine anything simpler.
> >> Your lack of imagination is profound.
> >>>> and the successor (to any natural number) is the union of
> >>>>> the number and the set whose only member is the number.
> >>>> If some technical mumbo jumbo is your idea of "natural"
> >>>> then... the technical definition that is "most natural" to me is
> >>>> a +1 monoid with 1 as the identity element.
> >>>>
> >>> After you have defined "monoid", "identity" and probably more
> >>> stuff. Lots more machinery.
> >> I guess you didn’t get the sarcasm.
> >>
> >> The simplest definition of the first natural number is …. “The first natural number.”
> >> The simplest formalization/representation of “The first natural number” is … whatever.
> >>
> >> 1. 0. A.
> >>
> >> Pick a symbol.
> >>>>> Above I gave a meta-language definition of natural numbers.
> >>>>
> >>>> No, you didn't. You gave a set-theoretic definition of the natural
> >>>> numbers.
> >>>>
> >>>> I used set-theory in the meta-language.
> >>>>
> >>>> But if set theory is just the "meta language" then what language
> >>>> are you using to DO mathematics in ?!?
> >>>>
> >>> None. Mathematics is not bound to the language it is expressed
> >>> in. Many mathematicians, like myself, think mostly in pictures.
> >> That is called geometry (if the pictures don’t move) and topology (if they do).
> >>> Computation is a small rarely visited corner of mathematics.
> >> Eeeh… toposes/programming languages are models of computation.
> >>
> >> Some would even consider computations such as homotopy types to be the foundation of mathematics.
> >
> > I wonder why you haven't actually said that you are basing your
> > theories on category theory. I am aware that category theory has
> > been suggested as a better foundation than set theory, But I have
> > never bothered to follow through the arguments because set theory
> > is adequate for what I do (actually "did", I've been retired a long time.
> >
> > There is a lot of words out there called the theory of programming
> > languages but it is not mathematical theory. I observe that the
> > Wikipedia article doesn't even consider assembly language. I fear
> > this a a theory only in the meta-language sense.
> Something slightly off topic that might interest you: Steve Crocker was
> a CS graduate student in the late 1960s. When he finished, he went to
> DARPA as a program manager where he was involved with networks, speech
> understanding systems, and a few other things. At UCLA he became
> interested in formal methods applied to programs and programming
> languages. The driving motivation for research in these areas was to
> find ways to develop secure software and PROVE it secure. Most of the
> efforts first tried to handle programs written in high level languages
> and, when that proved too difficult, motivated the invention of
> "logical" specification languages where the translation from
> representation language to theorems was straightforward and amenable to
> work with theorem provers.
>
> Steve went in a different direction when he did his dissertation: he was
> going to prove some things about real code written for the Honeywell
> 516. There were several points to be noted: 1) the code was in assembly
> language, 2) it was interrupt driven for the most part, 3) the code was
> self modifying!! I think that code was from an early development for the
> IMP (Intermediate Message Processor) used as the store and forward
> agents for the early research net and for connections to the host computers.
>
> So here was one of the few (very few) attempts to formalize machine
> actions and the raw programs they ran. I believe that Steve's approach
> was called "State Deltas" where there was a change operator that could
> specify changes to machine state and rules for telescoping sequences of
> changes to more compact representations and easier (simpler?) to check
> current state properties.
>
> This fascinating work like so much of that done in the field of program
> language semantics and property assurance has not had a major impact.
> For industrial use, the languages and language processors (compilers)
> could not be changed to save a nanosecond here and there - they would
> need to recertify whatever changed. Steve, in a sense finessed that
> problem since there were no tools between the program and runtime; he
> was in the business of validating raw machine code, i.e., programs in
> their most scruffy form. It always seemed to me something like trying to
> put a leash on a hyena and taking it to a dog obedience class - my money
> was on the hyena.

Thank You for the information. Totally new to me.

Thinking about programming I was surprise to find myself concluding
that Turing Machines were almost the best model for a "computer".
A bit Turing Machine does four things in each action (I assume a two
stack model) :
1) Decides which (of two) action to take on the basis of the current
value
2) Stores the current value
3) Replaces the current value with a new value
4) Goes to another state.

So each step could be written:
NX LR XX NY
where LR and XX are bits and NX and NY are state names. LR is
stack selector and XX the new value.

A program is then a set of steps. The first task seems to be - get
rid of the state names,

On 8/30/2022 6:13 PM, dklei...@gmail.com wrote:
> On Tuesday, August 30, 2022 at 12:35:14 PM UTC-7, Jeff Barnett wrote:
>> On 8/30/2022 12:25 PM, dklei...@gmail.com wrote:
>>> On Tuesday, August 30, 2022 at 2:52:16 AM UTC-7, skepd...@gmail.com wrote:
>>>> On Tuesday, 30 August 2022 at 07:12:41 UTC+2, dklei...@gmail.com wrote:
>>>>> On Monday, August 29, 2022 at 3:13:22 AM UTC-7, skepd...@gmail.com wrote:
>>>>>> On Monday, 29 August 2022 at 02:08:12 UTC+2, dklei...@gmail.com wrote:
>>>>>>> Reflexive language isn't even good linguistics. It has nothing to do with
>>>>>>> mathematics.
>>>>>> I have no idea what you mean by "good linguistics", but I sure as hell understand what reflection in formal languages is and how it works.
>>>>>>
>>>>>> Perhaps you want to insist that programming language theory is not
>>>>>> Mathematics; or linguistics when it's actually both!
>>>>>>
>>>>> Well, a programming language theory is a mathematical possibility. I
>>>>> have never seen one. Reference?
>>>> It literally goes by the name “Programming Language Theory”.
>>>>>>> You have that backwards. In the most natural definition
>>>>>> I think I have that quite forward, thank you. I am aware of
>>>>>> multitude of definitions. I have no idea which your aesthetic
>>>>>> sensibilities consider "most natural".
>>>>>>
>>>>> Like most mathematicians I use "natural" in the meta-language
>>>>> in an Occam-like sense. Of two propositions the more natural
>>>>> one is one involving the least machinery to define.
>>>>>>
>>>>>> Maybe you want to formalize your "most natural" proposition?
>>>>>>> natural numbers the first natural number is the empty set
>>>>>> Oh, wow! So the 1st number is not even the number 1 itself!?!
>>>>>> The "first" number is a set! An empty one at that.
>>>>>>
>>>>>> There's nothing natural about your definition of "natural".
>>>>>>
>>>>>> Hard to imagine anything simpler.
>>>> Your lack of imagination is profound.
>>>>>> and the successor (to any natural number) is the union of
>>>>>>> the number and the set whose only member is the number.
>>>>>> If some technical mumbo jumbo is your idea of "natural"
>>>>>> then... the technical definition that is "most natural" to me is
>>>>>> a +1 monoid with 1 as the identity element.
>>>>>>
>>>>> After you have defined "monoid", "identity" and probably more
>>>>> stuff. Lots more machinery.
>>>> I guess you didn’t get the sarcasm.
>>>>
>>>> The simplest definition of the first natural number is …. “The first natural number.”
>>>> The simplest formalization/representation of “The first natural number” is … whatever.
>>>>
>>>> 1. 0. A.
>>>>
>>>> Pick a symbol.
>>>>>>> Above I gave a meta-language definition of natural numbers.
>>>>>>
>>>>>> No, you didn't. You gave a set-theoretic definition of the natural
>>>>>> numbers.
>>>>>>
>>>>>> I used set-theory in the meta-language.
>>>>>>
>>>>>> But if set theory is just the "meta language" then what language
>>>>>> are you using to DO mathematics in ?!?
>>>>>>
>>>>> None. Mathematics is not bound to the language it is expressed
>>>>> in. Many mathematicians, like myself, think mostly in pictures.
>>>> That is called geometry (if the pictures don’t move) and topology (if they do).
>>>>> Computation is a small rarely visited corner of mathematics.
>>>> Eeeh… toposes/programming languages are models of computation.
>>>>
>>>> Some would even consider computations such as homotopy types to be the foundation of mathematics.
>>>
>>> I wonder why you haven't actually said that you are basing your
>>> theories on category theory. I am aware that category theory has
>>> been suggested as a better foundation than set theory, But I have
>>> never bothered to follow through the arguments because set theory
>>> is adequate for what I do (actually "did", I've been retired a long time.
>>>
>>> There is a lot of words out there called the theory of programming
>>> languages but it is not mathematical theory. I observe that the
>>> Wikipedia article doesn't even consider assembly language. I fear
>>> this a a theory only in the meta-language sense.
>> Something slightly off topic that might interest you: Steve Crocker was
>> a CS graduate student in the late 1960s. When he finished, he went to
>> DARPA as a program manager where he was involved with networks, speech
>> understanding systems, and a few other things. At UCLA he became
>> interested in formal methods applied to programs and programming
>> languages. The driving motivation for research in these areas was to
>> find ways to develop secure software and PROVE it secure. Most of the
>> efforts first tried to handle programs written in high level languages
>> and, when that proved too difficult, motivated the invention of
>> "logical" specification languages where the translation from
>> representation language to theorems was straightforward and amenable to
>> work with theorem provers.
>>
>> Steve went in a different direction when he did his dissertation: he was
>> going to prove some things about real code written for the Honeywell
>> 516. There were several points to be noted: 1) the code was in assembly
>> language, 2) it was interrupt driven for the most part, 3) the code was
>> self modifying!! I think that code was from an early development for the
>> IMP (Intermediate Message Processor) used as the store and forward
>> agents for the early research net and for connections to the host computers.
>>
>> So here was one of the few (very few) attempts to formalize machine
>> actions and the raw programs they ran. I believe that Steve's approach
>> was called "State Deltas" where there was a change operator that could
>> specify changes to machine state and rules for telescoping sequences of
>> changes to more compact representations and easier (simpler?) to check
>> current state properties.
>>
>> This fascinating work like so much of that done in the field of program
>> language semantics and property assurance has not had a major impact.
>> For industrial use, the languages and language processors (compilers)
>> could not be changed to save a nanosecond here and there - they would
>> need to recertify whatever changed. Steve, in a sense finessed that
>> problem since there were no tools between the program and runtime; he
>> was in the business of validating raw machine code, i.e., programs in
>> their most scruffy form. It always seemed to me something like trying to
>> put a leash on a hyena and taking it to a dog obedience class - my money
>> was on the hyena.
>
> Thank You for the information. Totally new to me.
>
> Thinking about programming I was surprise to find myself concluding
> that Turing Machines were almost the best model for a "computer".
> A bit Turing Machine does four things in each action (I assume a two
> stack model) :
> 1) Decides which (of two) action to take on the basis of the current
> value
> 2) Stores the current value
> 3) Replaces the current value with a new value
> 4) Goes to another state.
>
> So each step could be written:
> NX LR XX NY
> where LR and XX are bits and NX and NY are state names. LR is
> stack selector and XX the new value.
>
> A program is then a set of steps. The first task seems to be - get
> rid of the state names,
I'm not quiet sure what you mean by a "bit TM". What you did write,
though, reminds me of an interesting architecture - two stack machines.
For fun let the characters be 0 (like a blank square) and a 1.
Essentially you build a tape with the two stacks; one being the tape
front and the other the tape back. You scan the tape by reading the
value off the top of one stack and write it on the head of the other.
This simulates scanning forward or backwards depending on which stack
you read and which you write. There are lots of ways to set up the state
transition function. One way is

Click here to read the complete article

On Tuesday, August 30, 2022 at 8:13:26 PM UTC-7, Jeff Barnett wrote:
> On 8/30/2022 6:13 PM, dklei...@gmail.com wrote:
> > On Tuesday, August 30, 2022 at 12:35:14 PM UTC-7, Jeff Barnett wrote:
> >> On 8/30/2022 12:25 PM, dklei...@gmail.com wrote:
> >>> On Tuesday, August 30, 2022 at 2:52:16 AM UTC-7, skepd...@gmail.com wrote:
> >>>> On Tuesday, 30 August 2022 at 07:12:41 UTC+2, dklei...@gmail.com wrote:
> >>>>> On Monday, August 29, 2022 at 3:13:22 AM UTC-7, skepd...@gmail.com wrote:
> >>>>>> On Monday, 29 August 2022 at 02:08:12 UTC+2, dklei...@gmail.com wrote:
> >>>>>>> Reflexive language isn't even good linguistics. It has nothing to do with
> >>>>>>> mathematics.
> >>>>>> I have no idea what you mean by "good linguistics", but I sure as hell understand what reflection in formal languages is and how it works.
> >>>>>>
> >>>>>> Perhaps you want to insist that programming language theory is not
> >>>>>> Mathematics; or linguistics when it's actually both!
> >>>>>>
> >>>>> Well, a programming language theory is a mathematical possibility. I
> >>>>> have never seen one. Reference?
> >>>> It literally goes by the name “Programming Language Theory”.
> >>>>>>> You have that backwards. In the most natural definition
> >>>>>> I think I have that quite forward, thank you. I am aware of
> >>>>>> multitude of definitions. I have no idea which your aesthetic
> >>>>>> sensibilities consider "most natural".
> >>>>>>
> >>>>> Like most mathematicians I use "natural" in the meta-language
> >>>>> in an Occam-like sense. Of two propositions the more natural
> >>>>> one is one involving the least machinery to define.
> >>>>>>
> >>>>>> Maybe you want to formalize your "most natural" proposition?
> >>>>>>> natural numbers the first natural number is the empty set
> >>>>>> Oh, wow! So the 1st number is not even the number 1 itself!?!
> >>>>>> The "first" number is a set! An empty one at that.
> >>>>>>
> >>>>>> There's nothing natural about your definition of "natural".
> >>>>>>
> >>>>>> Hard to imagine anything simpler.
> >>>> Your lack of imagination is profound.
> >>>>>> and the successor (to any natural number) is the union of
> >>>>>>> the number and the set whose only member is the number.
> >>>>>> If some technical mumbo jumbo is your idea of "natural"
> >>>>>> then... the technical definition that is "most natural" to me is
> >>>>>> a +1 monoid with 1 as the identity element.
> >>>>>>
> >>>>> After you have defined "monoid", "identity" and probably more
> >>>>> stuff. Lots more machinery.
> >>>> I guess you didn’t get the sarcasm.
> >>>>
> >>>> The simplest definition of the first natural number is …. “The first natural number.”
> >>>> The simplest formalization/representation of “The first natural number” is … whatever.
> >>>>
> >>>> 1. 0. A.
> >>>>
> >>>> Pick a symbol.
> >>>>>>> Above I gave a meta-language definition of natural numbers.
> >>>>>>
> >>>>>> No, you didn't. You gave a set-theoretic definition of the natural
> >>>>>> numbers.
> >>>>>>
> >>>>>> I used set-theory in the meta-language.
> >>>>>>
> >>>>>> But if set theory is just the "meta language" then what language
> >>>>>> are you using to DO mathematics in ?!?
> >>>>>>
> >>>>> None. Mathematics is not bound to the language it is expressed
> >>>>> in. Many mathematicians, like myself, think mostly in pictures.
> >>>> That is called geometry (if the pictures don’t move) and topology (if they do).
> >>>>> Computation is a small rarely visited corner of mathematics.
> >>>> Eeeh… toposes/programming languages are models of computation.
> >>>>
> >>>> Some would even consider computations such as homotopy types to be the foundation of mathematics.
> >>>
> >>> I wonder why you haven't actually said that you are basing your
> >>> theories on category theory. I am aware that category theory has
> >>> been suggested as a better foundation than set theory, But I have
> >>> never bothered to follow through the arguments because set theory
> >>> is adequate for what I do (actually "did", I've been retired a long time.
> >>>
> >>> There is a lot of words out there called the theory of programming
> >>> languages but it is not mathematical theory. I observe that the
> >>> Wikipedia article doesn't even consider assembly language. I fear
> >>> this a a theory only in the meta-language sense.
> >> Something slightly off topic that might interest you: Steve Crocker was
> >> a CS graduate student in the late 1960s. When he finished, he went to
> >> DARPA as a program manager where he was involved with networks, speech
> >> understanding systems, and a few other things. At UCLA he became
> >> interested in formal methods applied to programs and programming
> >> languages. The driving motivation for research in these areas was to
> >> find ways to develop secure software and PROVE it secure. Most of the
> >> efforts first tried to handle programs written in high level languages
> >> and, when that proved too difficult, motivated the invention of
> >> "logical" specification languages where the translation from
> >> representation language to theorems was straightforward and amenable to
> >> work with theorem provers.
> >>
> >> Steve went in a different direction when he did his dissertation: he was
> >> going to prove some things about real code written for the Honeywell
> >> 516. There were several points to be noted: 1) the code was in assembly
> >> language, 2) it was interrupt driven for the most part, 3) the code was
> >> self modifying!! I think that code was from an early development for the
> >> IMP (Intermediate Message Processor) used as the store and forward
> >> agents for the early research net and for connections to the host computers.
> >>
> >> So here was one of the few (very few) attempts to formalize machine
> >> actions and the raw programs they ran. I believe that Steve's approach
> >> was called "State Deltas" where there was a change operator that could
> >> specify changes to machine state and rules for telescoping sequences of
> >> changes to more compact representations and easier (simpler?) to check
> >> current state properties.
> >>
> >> This fascinating work like so much of that done in the field of program
> >> language semantics and property assurance has not had a major impact.
> >> For industrial use, the languages and language processors (compilers)
> >> could not be changed to save a nanosecond here and there - they would
> >> need to recertify whatever changed. Steve, in a sense finessed that
> >> problem since there were no tools between the program and runtime; he
> >> was in the business of validating raw machine code, i.e., programs in
> >> their most scruffy form. It always seemed to me something like trying to
> >> put a leash on a hyena and taking it to a dog obedience class - my money
> >> was on the hyena.
> >
> > Thank You for the information. Totally new to me.
> >
> > Thinking about programming I was surprise to find myself concluding
> > that Turing Machines were almost the best model for a "computer".
> > A bit Turing Machine does four things in each action (I assume a two
> > stack model) :
> > 1) Decides which (of two) action to take on the basis of the current
> > value
> > 2) Stores the current value
> > 3) Replaces the current value with a new value
> > 4) Goes to another state.
> >
> > So each step could be written:
> > NX LR XX NY
> > where LR and XX are bits and NX and NY are state names. LR is
> > stack selector and XX the new value.
> >
> > A program is then a set of steps. The first task seems to be - get
> > rid of the state names,
> I'm not quiet sure what you mean by a "bit TM". What you did write,
> though, reminds me of an interesting architecture - two stack machines.
> For fun let the characters be 0 (like a blank square) and a 1.
> Essentially you build a tape with the two stacks; one being the tape
> front and the other the tape back. You scan the tape by reading the
> value off the top of one stack and write it on the head of the other.
> This simulates scanning forward or backwards depending on which stack
> you read and which you write. There are lots of ways to set up the state
> transition function. One way is
>
> current-state char-on-stack1 char-on-stack2 delta1 delta2 new-state
>
>
> where delta-i is what to do at the head of stack-i: stand pat, pop,
> replace top, add item. As I said. there are lots of ways to do this. And
> it's obvious that you can simulate any TM with this two-stack mechanism
> if you recall that any TM computation can be done with a two character
> alphabet.
>
> I think (but am not sure) that you can even do full Touring things with
> two adders where you can see the low order bits of each. If memory
> serves me, the trick is that you can simulate the two-stack set up and
> that can simulate the TM.

On 8/30/2022 10:00 PM, dklei...@gmail.com wrote:
> On Tuesday, August 30, 2022 at 8:13:26 PM UTC-7, Jeff Barnett wrote:
>> On 8/30/2022 6:13 PM, dklei...@gmail.com wrote:
>>> On Tuesday, August 30, 2022 at 12:35:14 PM UTC-7, Jeff Barnett wrote:
>>>> On 8/30/2022 12:25 PM, dklei...@gmail.com wrote:
>>>>> On Tuesday, August 30, 2022 at 2:52:16 AM UTC-7, skepd...@gmail.com wrote:
>>>>>> On Tuesday, 30 August 2022 at 07:12:41 UTC+2, dklei...@gmail.com wrote:
>>>>>>> On Monday, August 29, 2022 at 3:13:22 AM UTC-7, skepd...@gmail.com wrote:
>>>>>>>> On Monday, 29 August 2022 at 02:08:12 UTC+2, dklei...@gmail.com wrote:
>>>>>>>>> Reflexive language isn't even good linguistics. It has nothing to do with
>>>>>>>>> mathematics.
>>>>>>>> I have no idea what you mean by "good linguistics", but I sure as hell understand what reflection in formal languages is and how it works.
>>>>>>>>
>>>>>>>> Perhaps you want to insist that programming language theory is not
>>>>>>>> Mathematics; or linguistics when it's actually both!
>>>>>>>>
>>>>>>> Well, a programming language theory is a mathematical possibility. I
>>>>>>> have never seen one. Reference?
>>>>>> It literally goes by the name “Programming Language Theory”.
>>>>>>>>> You have that backwards. In the most natural definition
>>>>>>>> I think I have that quite forward, thank you. I am aware of
>>>>>>>> multitude of definitions. I have no idea which your aesthetic
>>>>>>>> sensibilities consider "most natural".
>>>>>>>>
>>>>>>> Like most mathematicians I use "natural" in the meta-language
>>>>>>> in an Occam-like sense. Of two propositions the more natural
>>>>>>> one is one involving the least machinery to define.
>>>>>>>>
>>>>>>>> Maybe you want to formalize your "most natural" proposition?
>>>>>>>>> natural numbers the first natural number is the empty set
>>>>>>>> Oh, wow! So the 1st number is not even the number 1 itself!?!
>>>>>>>> The "first" number is a set! An empty one at that.
>>>>>>>>
>>>>>>>> There's nothing natural about your definition of "natural".
>>>>>>>>
>>>>>>>> Hard to imagine anything simpler.
>>>>>> Your lack of imagination is profound.
>>>>>>>> and the successor (to any natural number) is the union of
>>>>>>>>> the number and the set whose only member is the number.
>>>>>>>> If some technical mumbo jumbo is your idea of "natural"
>>>>>>>> then... the technical definition that is "most natural" to me is
>>>>>>>> a +1 monoid with 1 as the identity element.
>>>>>>>>
>>>>>>> After you have defined "monoid", "identity" and probably more
>>>>>>> stuff. Lots more machinery.
>>>>>> I guess you didn’t get the sarcasm.
>>>>>>
>>>>>> The simplest definition of the first natural number is …. “The first natural number.”
>>>>>> The simplest formalization/representation of “The first natural number” is … whatever.
>>>>>>
>>>>>> 1. 0. A.
>>>>>>
>>>>>> Pick a symbol.
>>>>>>>>> Above I gave a meta-language definition of natural numbers.
>>>>>>>>
>>>>>>>> No, you didn't. You gave a set-theoretic definition of the natural
>>>>>>>> numbers.
>>>>>>>>
>>>>>>>> I used set-theory in the meta-language.
>>>>>>>>
>>>>>>>> But if set theory is just the "meta language" then what language
>>>>>>>> are you using to DO mathematics in ?!?
>>>>>>>>
>>>>>>> None. Mathematics is not bound to the language it is expressed
>>>>>>> in. Many mathematicians, like myself, think mostly in pictures.
>>>>>> That is called geometry (if the pictures don’t move) and topology (if they do).
>>>>>>> Computation is a small rarely visited corner of mathematics.
>>>>>> Eeeh… toposes/programming languages are models of computation.
>>>>>>
>>>>>> Some would even consider computations such as homotopy types to be the foundation of mathematics.
>>>>>
>>>>> I wonder why you haven't actually said that you are basing your
>>>>> theories on category theory. I am aware that category theory has
>>>>> been suggested as a better foundation than set theory, But I have
>>>>> never bothered to follow through the arguments because set theory
>>>>> is adequate for what I do (actually "did", I've been retired a long time.
>>>>>
>>>>> There is a lot of words out there called the theory of programming
>>>>> languages but it is not mathematical theory. I observe that the
>>>>> Wikipedia article doesn't even consider assembly language. I fear
>>>>> this a a theory only in the meta-language sense.
>>>> Something slightly off topic that might interest you: Steve Crocker was
>>>> a CS graduate student in the late 1960s. When he finished, he went to
>>>> DARPA as a program manager where he was involved with networks, speech
>>>> understanding systems, and a few other things. At UCLA he became
>>>> interested in formal methods applied to programs and programming
>>>> languages. The driving motivation for research in these areas was to
>>>> find ways to develop secure software and PROVE it secure. Most of the
>>>> efforts first tried to handle programs written in high level languages
>>>> and, when that proved too difficult, motivated the invention of
>>>> "logical" specification languages where the translation from
>>>> representation language to theorems was straightforward and amenable to
>>>> work with theorem provers.
>>>>
>>>> Steve went in a different direction when he did his dissertation: he was
>>>> going to prove some things about real code written for the Honeywell
>>>> 516. There were several points to be noted: 1) the code was in assembly
>>>> language, 2) it was interrupt driven for the most part, 3) the code was
>>>> self modifying!! I think that code was from an early development for the
>>>> IMP (Intermediate Message Processor) used as the store and forward
>>>> agents for the early research net and for connections to the host computers.
>>>>
>>>> So here was one of the few (very few) attempts to formalize machine
>>>> actions and the raw programs they ran. I believe that Steve's approach
>>>> was called "State Deltas" where there was a change operator that could
>>>> specify changes to machine state and rules for telescoping sequences of
>>>> changes to more compact representations and easier (simpler?) to check
>>>> current state properties.
>>>>
>>>> This fascinating work like so much of that done in the field of program
>>>> language semantics and property assurance has not had a major impact.
>>>> For industrial use, the languages and language processors (compilers)
>>>> could not be changed to save a nanosecond here and there - they would
>>>> need to recertify whatever changed. Steve, in a sense finessed that
>>>> problem since there were no tools between the program and runtime; he
>>>> was in the business of validating raw machine code, i.e., programs in
>>>> their most scruffy form. It always seemed to me something like trying to
>>>> put a leash on a hyena and taking it to a dog obedience class - my money
>>>> was on the hyena.
>>>
>>> Thank You for the information. Totally new to me.
>>>
>>> Thinking about programming I was surprise to find myself concluding
>>> that Turing Machines were almost the best model for a "computer".
>>> A bit Turing Machine does four things in each action (I assume a two
>>> stack model) :
>>> 1) Decides which (of two) action to take on the basis of the current
>>> value
>>> 2) Stores the current value
>>> 3) Replaces the current value with a new value
>>> 4) Goes to another state.
>>>
>>> So each step could be written:
>>> NX LR XX NY
>>> where LR and XX are bits and NX and NY are state names. LR is
>>> stack selector and XX the new value.
>>>
>>> A program is then a set of steps. The first task seems to be - get
>>> rid of the state names,
>> I'm not quiet sure what you mean by a "bit TM". What you did write,
>> though, reminds me of an interesting architecture - two stack machines.
>> For fun let the characters be 0 (like a blank square) and a 1.
>> Essentially you build a tape with the two stacks; one being the tape
>> front and the other the tape back. You scan the tape by reading the
>> value off the top of one stack and write it on the head of the other.
>> This simulates scanning forward or backwards depending on which stack
>> you read and which you write. There are lots of ways to set up the state
>> transition function. One way is
>>
>> current-state char-on-stack1 char-on-stack2 delta1 delta2 new-state
>>
>>
>> where delta-i is what to do at the head of stack-i: stand pat, pop,
>> replace top, add item. As I said. there are lots of ways to do this. And
>> it's obvious that you can simulate any TM with this two-stack mechanism
>> if you recall that any TM computation can be done with a two character
>> alphabet.
>>
>> I think (but am not sure) that you can even do full Touring things with
>> two adders where you can see the low order bits of each. If memory
>> serves me, the trick is that you can simulate the two-stack set up and
>> that can simulate the TM.
>
> Yes, that's the way the two stack model of a Turing Machine I described
> a couple of weeks ago on comp.theory works. Two stacks called LEFT
> and RIGHT and a single symbol I called VALUE. To move right one looks
> at RIGHT and pops it if it is not empty otherwise get the EMPTY symbol
> and push VALUE onto LEFT. Etc.
>
> By bit Turing Machine I mean one whose data is one bit. Stack machines
> can have any finite set of symbols as their alphabet.
>
> But I was messing with what Turing Machines are in order to define the
> most general "computer" that could be usefully used. Which, not too
> surprisingly, turns out to be essentially Turing Machines.
>
> But states still bother me,

Click here to read the complete article

Skep Dick <skepdick22@gmail.com> writes:

> On Tuesday, 30 August 2022 at 00:15:20 UTC+2, Ben Bacarisse wrote:
>> Skep Dick <skepd...@gmail.com> writes:
>>
>> > On Monday, 29 August 2022 at 17:27:06 UTC+2, Ben Bacarisse wrote:
>> >> So it seems. As you say the 0th integer greater than 4 is 4.
>> >> Apparently at least one of "ALL the integers greater than 4" is 4 --
>> >> specifically the one indexed by 0.
>> >> greater than 4" includes 4 as the 0th indexed element (other than you)?
>>
>> > So you STILL refuse to tell me whether you think the 1st successor to
>> > 0 is "succ zero" or "succ succ zero". And you STILL refuse to tell me
>> > whether you think the 0th successor to 0 is "zero" or "succ zero".
>> >
>> > I guess we'll never know whether **TO YOU** ALL the successors to zero
>> > includes, or excludes zero itself...
>> Nope, and I don't think that the 0th integer greater than 4 is 4 either!
>
> I don’t think it is a matter of what you think. It is a matter of
> whether the theorem holds given some axioms (of my arbitrary
> choosing).

So now you will claim that you get to decide you meant by greater than 4
all along having give no hint that you have your own secret meaning for
such a common term. In fact, we have no idea what 4 means to you do we?
I think everyone should read your posts with that in mind. When you say
that 5 > 4 you may be making a mistake.

> You may not like the implications of said axioms/definitions but why
> should mathematicians care?

If you were someone posting in good faith, I'd ask to see the axioms
that lets you answer the question "What's the 0th integer greater than
4?" with "It's 4!". Would you post them if I asked for them?

--
Ben.

On Wednesday, 31 August 2022 at 17:22:17 UTC+2, Ben Bacarisse wrote:
> So now you will claim that you get to decide you meant by greater than 4
> all along having give no hint that you have your own secret meaning for
> such a common term.
But I am not speaking about "greater than"?!?!
I am speaking about "nth greater than"!

Why are you bringing your Mathematical baggage to the question?

>In fact, we have no idea what 4 means to you do we?
It doesn't mean anything to anyone. Me or you.

The way you can establish this fact is by trying (and failing) to tell me something about 4 without appealing to any of its relations. Perhaps you'll even be tempted to relate it to the English word "four".

But you never know. You might surprise me. Tell me a true thing about 4.

> I think everyone should read your posts with that in mind. When you say
> that 5 > 4 you may be making a mistake.
What could you possibly mean by a "mistake" - that idea is not definable within the language of any formal system.

I mean.. YOU could be making a mistake. Is 5>4 = 1 or is 5 > 4 = True? Are the numbers open or closed under >?

Who knows?

> > You may not like the implications of said axioms/definitions but why
> > should mathematicians care?
> If you were someone posting in good faith, I'd ask to see the axioms
> that lets you answer the question "What's the 0th integer greater than
> 4?" with "It's 4!". Would you post them if I asked for them?
Would it even matter if I said yes?

You don't even accept my theorem, but you care about the axioms.

Skep Dick <skepdick22@gmail.com> writes:

> On Wednesday, 31 August 2022 at 17:22:17 UTC+2, Ben Bacarisse wrote:
>> So now you will claim that you get to decide you meant by greater than 4
>> all along having give no hint that you have your own secret meaning for
>> such a common term.
> But I am not speaking about "greater than"?!?!
> I am speaking about "nth greater than"!

Exactly what you have contrived to redefine is not the point. You have
your own meaning for something that readers should be able to take for
granted. You were talking about how to index the collection of all
integers greater the 4. If it has a 0th element it's 5. If it only has
a 1st element it's 5. That, at least, is the non-SD use of these terms.

> Why are you bringing your Mathematical baggage to the question?

Because I was being generous and was not assuming you'd asked a question
in bad faith -- one based on secret axioms.

>> If you were someone posting in good faith, I'd ask to see the axioms
>> that lets you answer the question "What's the 0th integer greater than
>> 4?" with "It's 4!". Would you post them if I asked for them?
>
> Would it even matter if I said yes?

Of course; it would make asking worth while. But I'll ask anyway.
Please give the axioms you were using when you wrote

"What's the 0th integer greater than 4? It's 4!"

> You don't even accept my theorem, but you care about the axioms.

Don't be silly. Of course it could be a theorem. For example, if you
used inconsistent axioms, everything is a theorem. It just sounds like
you are preparing the ground for not posting them...

--
Ben.

On Thursday, 1 September 2022 at 00:04:25 UTC+2, Ben Bacarisse wrote:
> Skep Dick <skepd...@gmail.com> writes:
>
> > On Wednesday, 31 August 2022 at 17:22:17 UTC+2, Ben Bacarisse wrote:

> > But I am not speaking about "greater than"?!?!
> > I am speaking about "nth greater than"!
> Exactly what you have contrived to redefine is not the point. You have
> your own meaning for something that readers should be able to take for
> granted.
You understand that all matters pertaining to "should" are opinions, yes?

>You were talking about how to index the collection of all
> integers greater the 4. If it has a 0th element it's 5. If it only has
> a 1st element it's 5. That, at least, is the non-SD use of these terms.
Oh, so there is a standard use of the notion "nth greater than" ? Show me.

N.B I am NOT talking about "greater than", I am talking about "nth greater than".

I feel like I have to stress this upon you since you keep brinding your baggage of assumptions ot my questions.

> > Why are you bringing your Mathematical baggage to the question?
> Because I was being generous and was not assuming you'd asked a question
> in bad faith -- one based on secret axioms.
The question is in English. Axioms are about Mathematics. Why do you keep bringing your Mathematical baggage to my English questions?

> > Would it even matter if I said yes?
> Of course; it would make asking worth while. But I'll ask anyway.
> Please give the axioms you were using when you wrote
ANY axiom-schema satisfying my theorem is sufficient.

Take the axioms of OCAML's formal semantics such that:

# let nth_greater_than n x = x - n + 0;;
val nth_greater_than : int -> int -> int = <fun>
# nth_greater_than 0 4;;
- : int = 4

Of course, you can make the function 1-indexed?

# let nth_greater_than n x = x - n + 1;;
val nth_greater_than : int -> int -> int = <fun>
# nth_greater_than 0 4;;
- : int = 5

OR you can make it index agnostic?

# let nth_greater_than_with_index n x i = x - n + i;;
val nth_greater_than_with_index : int -> int -> int -> int = <fun>
# nth_greater_than_with_index 0 4 0;;
- : int = 4
# nth_greater_than_with_index 0 4 1;;
- : int = 5

> "What's the 0th integer greater than 4? It's 4!"
> > You don't even accept my theorem, but you care about the axioms.
> Don't be silly. Of course it could be a theorem. For example, if you
> used inconsistent axioms, everything is a theorem.
What? That's not true! It depends on which system you are using. It's absolutely not the case in para-consistent logics.

>It just sounds like you are preparing the ground for not posting them...
It sounds like axioms are unlikely to address our misunderstanding...

Skep Dick <skepdick22@gmail.com> writes:

> On Thursday, 1 September 2022 at 00:04:25 UTC+2, Ben Bacarisse wrote:
>> Skep Dick <skepd...@gmail.com> writes:
>>
>> > On Wednesday, 31 August 2022 at 17:22:17 UTC+2, Ben Bacarisse wrote:
>
>> > But I am not speaking about "greater than"?!?!
>> > I am speaking about "nth greater than"!
>> Exactly what you have contrived to redefine is not the point. You have
>> your own meaning for something that readers should be able to take for
>> granted.
>
> You understand that all matters pertaining to "should" are opinions,
> yes?

Of course. This is the key difference between us. It is my _opinion_
that retroactively claiming unstated axioms to justify otherwise
apparently absurd remarks is unreasonable. Your _opinion_ is different.

>>You were talking about how to index the collection of all
>> integers greater the 4. If it has a 0th element it's 5. If it only has
>> a 1st element it's 5. That, at least, is the non-SD use of these
>> terms.
>
> Oh, so there is a standard use of the notion "nth greater than" ? Show
> me.

Ordinal numbers index a set. You were indexing the set of "all integers
greater than 4". 4 is not a member of that set. There is no nth member
of that set that is 4. That, of course, is my "baggage", otherwise know
as "what the words mean". In your subsequent justification, 4 might
well be in that set. You don't actually say how that set is defined
because you are currently pretend that you didn't talk about "greater
than".

> N.B I am NOT talking about "greater than", I am talking about "nth
> greater than".

If you are going to flat-out lie, there is no point. You explicitly
referred to "all numbers greater than 4". How is that not talking about
"greater than"?

Unfortunately, despite havine revealed some of the secret axioms, you
omit to say how "all numbers greater than 4" might be defined. But
there's nothing to prevent 4, or even -23, being in that set, now that
we know the plain words can't be relied on.

> I feel like I have to stress this upon you since you keep brinding
> your baggage of assumptions ot my questions.

I know. You reserve the right pull unstated axiom out of the bag at any
stage. I consider that dishonest. My "baggage of assumptions" is that
when you write "all integers greater than 4" you mean "all integers
greater than 4" in the usual non-disingenuous sense. And that baggage
includes the crazy notion that no indexed member of that collection will
be 4. Crazy baggage, right? How could I have been so naive. Just as
well you explained, five days later, that

"It is a matter of whether the theorem holds given some axioms (of my
arbitrary choosing)."

>> > Why are you bringing your Mathematical baggage to the question?
>> Because I was being generous and was not assuming you'd asked a question
>> in bad faith -- one based on secret axioms.
>
> The question is in English. Axioms are about Mathematics. Why do you
> keep bringing your Mathematical baggage to my English questions?

You are determined to be dishonest. /You/ brought up the idea of
axioms when you said

"It is a matter of whether the theorem holds given some axioms (of my
arbitrary choosing)."

I never mentioned axioms until you did. Until then I was going with the
notion that the plain meaning of the words was what you meant.

When I interpret terms like "all integers greater than 4" as having some
numerical meaning you complain about my "mathematical baggage". You
retrospectively justify the junk claim by bringing up unspecified axioms
and that's fine, apparently, but if I even mention your axioms its my
baggage again. There is no end to your duplicity.

>> > Would it even matter if I said yes?
>> Of course; it would make asking worth while. But I'll ask anyway.
>> Please give the axioms you were using when you wrote
>
> ANY axiom-schema satisfying my theorem is sufficient.
>
> Take the axioms of OCAML's formal semantics such that:
>
> # let nth_greater_than n x = x - n + 0;;
> val nth_greater_than : int -> int -> int = <fun>
> # nth_greater_than 0 4;;
> - : int = 4

You could just say that n + k > n for all k in N and be done with it.
When your only goal is justifying nonsense words, any old axioms will
do.

I'd hoped you'd explain "all integers greater than 4" using axioms. Is
3 in the collection of "all integers greater than 4"? What about -7?
Without axioms for greater than (you know, that thing you didn't talk
about) I can't be sure.

You could equally have said, that 3 the 0th integer greater than 4 and
then, ten days later written

let nth_greater_than n x = x - n - 1;;

to justify it. Wouldn't that have been more fun?

>> "What's the 0th integer greater than 4? It's 4!"
>> > You don't even accept my theorem, but you care about the axioms.
>> Don't be silly. Of course it could be a theorem. For example, if you
>> used inconsistent axioms, everything is a theorem.
>
> What? That's not true! It depends on which system you are using. It's
> absolutely not the case in para-consistent logics.

Silly me! You retroactively brought up the notion of undisclosed
axioms, so why not make the underlying logic up for grabs too! In fact,
unless you explicitly say so, no one should assume that /any/ logic is
being used. You might, for example, be writing maths poems like PO
does.

--
Ben.

On Friday, 2 September 2022 at 04:58:58 UTC+2, Ben Bacarisse wrote:
> > You understand that all matters pertaining to "should" are opinions,
> > yes?
> Of course. This is the key difference between us. It is my _opinion_
> that retroactively claiming unstated axioms to justify otherwise
> apparently absurd remarks is unreasonable. Your _opinion_ is different.
I don't understand why you would say that's even a difference between us?!?

Obviously it's just your opinion.
And obviously it's just my opinion.

Exactly like it's just your _opinion_ that it's "unreasonable" to have unstated axioms. A property for which _you_ have unstated axioms!

We are far more alike than you think, you and I ;)

> > Oh, so there is a standard use of the notion "nth greater than" ? Show
> > me.
> Ordinal numbers index a set.
Yes but that's not the point! Ordinal numbers also form a set. What indexes that?

>You were indexing the set of "all integers
> greater than 4". 4 is not a member of that set. There is no nth member
> of that set that is 4. That, of course, is my "baggage", otherwise know
> as "what the words mean".
No! That is absolutely the baggage of your (unstated) axioms!

I bet you are also going to tell me silly, unprovable stuff like "ALL subsets of finite sets are finite."

Your notion of "ALL" is not constructive. Mine is!

>In your subsequent justification, 4 might
> well be in that set. You don't actually say how that set is defined
> because you are currently pretend that you didn't talk about "greater
> than".
I am doing no more "pretending" than you are. I am just working in my usua l system. Just like you are working in your usual system.

Of course, my usual and your usual are just _opinions_ !

> > N.B I am NOT talking about "greater than", I am talking about "nth
> > greater than".
> If you are going to flat-out lie, there is no point. You explicitly
> referred to "all numbers greater than 4". How is that not talking about
> "greater than"?
Well because in the BHK/realizability interpretation ∀ means something different than what you think it means.
In my world (of computation) ∀ doesn't mean “it holds for every instance”. It means “there is a program which produces/computes a witness from an instance"

∀x ∈ A.P(x) is realized by a program which maps a representation of any a ∈ A to a realizer of P (a).

> Unfortunately, despite havine revealed some of the secret axioms, you
> omit to say how "all numbers greater than 4" might be defined.
Exactly how you omit to say how "forall" and "all" might be defined.

> there's nothing to prevent 4, or even -23, being in that set, now that
> we know the plain words can't be relied on.
There's nothing to say how the property you call "plain" is to be proved either.

> > I feel like I have to stress this upon you since you keep brinding
> > your baggage of assumptions ot my questions.
> I know. You reserve the right pull unstated axiom out of the bag at any
> stage. I consider that dishonest.
And I consider the property you call "dishonest" to be a theorem for which you have failed to provide a proof.

>My "baggage of assumptions" is that
> when you write "all integers greater than 4" you mean "all integers
> greater than 4" in the usual non-disingenuous sense.
Heh! You see! There's all that "excluded middle" baggage I am talking about!

What I expect is that when you present me with a disjunction such as P v not-P (e.g disingenuous v not-disingenuous) I demand a continuous proof! A program, a decision procedure which proves P; or proves not-P.
And I also demand you tell me WHICH ONE you've proven!

>And that baggage
> includes the crazy notion that no indexed member of that collection will
> be 4. Crazy baggage, right? How could I have been so naive. Just as
> well you explained, five days later, that
> "It is a matter of whether the theorem holds given some axioms (of my
> arbitrary choosing)."
Yeah. And? It's been what? More than 5 days now and YOU haven't even brought your arbitrary axioms to the table!

Under the pretense that they are "usual" (while having failed to provide a decision procedure; a proof! for the usual v not-usual disjunction).

> >> > Why are you bringing your Mathematical baggage to the question?
> >> Because I was being generous and was not assuming you'd asked a question
> >> in bad faith -- one based on secret axioms.
> >
> > The question is in English. Axioms are about Mathematics. Why do you
> > keep bringing your Mathematical baggage to my English questions?
> You are determined to be dishonest. /You/ brought up the idea of
> axioms when you said
> "It is a matter of whether the theorem holds given some axioms (of my
> arbitrary choosing)."
Yes! ____I_____ brought it up. ____YOU____ didn't. So which one of us is dishonest?

> I never mentioned axioms until you did. Until then I was going with the
> notion that the plain meaning of the words was what you meant.
You fail to provide the axioms from which the plain v not-plain disjunction is proven.

> When I interpret terms like "all integers greater than 4" as having some
> numerical meaning you complain about my "mathematical baggage".
This is comp.theory! Why are you bringing your NON-computational baggage?

> retrospectively justify the junk claim by bringing up unspecified axioms
> and that's fine, apparently, but if I even mention your axioms its my
> baggage again. There is no end to your duplicity.
Because this is comp.theory! And I need not make my computational baggage explicit.

But if you want me to make it explicit (even though I am using the usual meanings for a computational theorist)... fine.

The Brouwer–Heyting–Kolmogorov rules explain when a program realizes a statement:
(1) falsehood ⊥ is not realized by anything;
(2) truth ⊤ is realized by a chosen constant, say ⋆;
(3) P∧Q is realized by a pair (p,q) such that p is a realizer of P and q of Q
(4) P ∨ Q is realized either by (0, p), where p realizes P , or by (1, q), where q realizes Q;
(5) P ⇒ Q is realized by a program which maps realizers of P to realizers of Q;
(6) ∀x ∈ A.P(x) is realized by a program which maps (a representation of) any a ∈ A to a realizer of P (a);
(7) ∃x ∈ A.P(x) is realized by a pair (p,q) such that p represents some a ∈ A and q realizes P(a);
(8) a = b is realized by a p which represents both a and b.

So when YOU tell me that either Halts ∨ not-Halts is true, I demand a proof! And I also demand you tell which one of the two cases in the disjunction you've proven.

If this universe is foreign to you - it's the usual universe of empiricism, science and evidence.

> You could just say that n + k > n for all k in N and be done with it.
> When your only goal is justifying nonsense words, any old axioms will
> do.
No, I can't! Because my "all" and your "all" are not the same.

> > What? That's not true! It depends on which system you are using. It's
> > absolutely not the case in para-consistent logics.
> Silly me! You retroactively brought up the notion of undisclosed
> axioms, so why not make the underlying logic up for grabs too!
Well that's YOUR problem. Your set-theoretic (guessing here) baggage doesn't have its own deductive system.

My computational baggage (type theory) is its own deductive system!

> unless you explicitly say so, no one should assume that /any/ logic is
> being used. You might, for example, be writing maths poems like PO
> does.
Liar. Deduction/logic is ABSOLUTELY being used.

What is unspecified is the introduction and elimination rules. The axioms.

Skep Dick <skepdick22@gmail.com> writes:

> On Friday, 2 September 2022 at 04:58:58 UTC+2, Ben Bacarisse wrote:
<you cut attribution lines again...>

>> > N.B I am NOT talking about "greater than", I am talking about "nth
>> > greater than".

You said, in the same post as the original nonsense, that you were
indexing "all the integers greater than 4".

>> If you are going to flat-out lie, there is no point. You explicitly
>> referred to "all numbers greater than 4". How is that not talking about
>> "greater than"?

> Well because in the BHK/realizability interpretation ∀ means something
> different than what you think it means. In my world (of computation)
> ∀ doesn't mean “it holds for every instance”. It means “there is a
> program which produces/computes a witness from an instance"

Dodging the lie, I see. Nothing here addresses it.

> ∀x ∈ A.P(x) is realized by a program which maps a representation of
> any a ∈ A to a realizer of P (a).

You talked about greater than and then tried to pretend you didn't.
It's not a good look, even when trolling.

--
Ben.
"What's the 0th integer greater than 4? It's 4!"
"It is a matter of whether the theorem holds given some axioms (of my
arbitrary choosing)." (Skep Dick, five days later)

On Saturday, 3 September 2022 at 03:03:42 UTC+2, Ben Bacarisse wrote:
> Skep Dick <skepd...@gmail.com> writes:
>
> > On Friday, 2 September 2022 at 04:58:58 UTC+2, Ben Bacarisse wrote:
> <you cut attribution lines again...>
> >> > N.B I am NOT talking about "greater than", I am talking about "nth
> >> > greater than".
> You said, in the same post as the original nonsense, that you were
> indexing "all the integers greater than 4".
> >> If you are going to flat-out lie, there is no point. You explicitly
> >> referred to "all numbers greater than 4". How is that not talking about
> >> "greater than"?
>
> > Well because in the BHK/realizability interpretation ∀ means something
> > different than what you think it means. In my world (of computation)
> > ∀ doesn't mean “it holds for every instance”. It means “there is a
> > program which produces/computes a witness from an instance"
> Dodging the lie, I see. Nothing here addresses it.
> > ∀x ∈ A.P(x) is realized by a program which maps a representation of
> > any a ∈ A to a realizer of P (a).
> You talked about greater than and then tried to pretend you didn't.
> It's not a good look, even when trolling.
That is a misrepresentation, colloquially - a lie.

Or maybe it is just your axioms. A lot of your thinking seems to boil down to P v not P dichotomies. Could it just be your life-long indoctrination? Time to wake up to the fact that disjunctions require proof!.

I mean… you totally dodged the question on whether you believe that all subsets of finite sets are finite.