Re: I have always been correct about emulating termination analyzers --- PROOF

On 2024-10-22 14:02:01 +0000, olcott said:

On 10/22/2024 2:13 AM, Mikko wrote:

On 2024-10-21 13:52:28 +0000, olcott said:
 

On 10/21/2024 3:41 AM, Mikko wrote:

On 2024-10-20 15:32:45 +0000, olcott said:
 

The actual barest essence for formal systems and computations
is finite string transformation rules applied to finite strings.

 Before you can start from that you need a formal theory that
can be interpreted as a theory of finite strings.

 Not at all. The only theory needed are the operations
that can be performed on finite strings:
concatenation, substring, relational operator ...

 You may try with an informal foundation but you need to make sure
that it is sufficicently well defined and that is easier with a
formal theory.
 

The minimal complete theory that I can think of computes
the sum of pairs of ASCII digit strings.

 That is easily extended to Peano arithmetic.
 As a bottom layer you need some sort of logic. There must be unambifuous
rules about syntax and inference.
 

 I already wrote this in C a long time ago.
It simply computes the sum the same way
that a first grader would compute the sum.
 I have no idea how the first grade arithmetic
algorithm could be extended to PA.

Basically you define that the successor of X is X + 1. The only
primitive function of Peano arithmetic is the successor. Addition
and multiplication are recursively defined from the successor
function. Equality is often included in the underlying logic but
can be defined recursively from the successor function and the
order relation is defined similarly.
Anyway, the details are not important, only that it can be done.
--
Mikko