Turing machines vs computation

<< Dependent type theories that are total and have a computable normalization procedure are Turing-incomplete. This is a theorem, not an opinion. Now, what the implications are for practical usability of dependent type theories that are total, that is an entirely different matter. >> [1] (slightly adapted: see the entire discussion for background)

Conversely, I would argue that Turing Machines are not an adequate model of computation: there just is no such thing as a machine that does not halt or crash or get switched off, eventually. And, eventually rather goes with interactively.

In fact, more generally, the name of that "misunderstanding" is yet again the problem of infinity in standard mathematics and mathematical logic.

[1] SE, Proof Assistants, "Possible root cause(s) of the misunderstanding that DTT implies not Turing complete?"
https://proofassistants.stackexchange.com/q/4002/3006#comment7782_4002

A Solution to Epimenides' Paradox

<< 'Morning everybody,
"Epimenides lies iff everybody lies!" which
I am taking to be the predicative version of
the uncooperative rational player. >>

Presentation and formal development (in Coq):
https://gist.github.com/jp-diegidio/f9a18bb0a8c87d585b1d56458cd082f6

[1] Wikipedia, "Epimenides paradox"
https://en.wikipedia.org/wiki/Epimenides_paradox

[2] Wikipedia, "Non-cooperative game theory"
https://en.wikipedia.org/wiki/Non-cooperative_game_theory

On the logic of "it"

# On the logic of "it" - Sparse (hopefully-)not-so-metaphysical thoughts

The idea of a Characteristica Universalis, i.e. an encyclopedic compendium of *acquired knowledge* in terms of a universal formal *language* that is potentially able to express all *understanding*, becomes in our times the inverse idea that *language* encapsulates all there is to *understanding* (whence e.g. the idea/hope that so called Large Language Models are a "solution to problems").

But the simplest formalization exercise indicates that between *language* and *understanding* (or, language and "reality") there is an essential gap that only *imagination* can fill.

What does this expression *mean*: `fun x y => x + y` ?
What does this expression *mean*: `a^$2 <>= T` ?
What does this expression *mean*: `2` ?

Sure, we might *explain* each of those, but as long as the explanation is itself formal, we still need to find a bottom to it (what does "it" *mean*?).  Eventually, the problem of meaning remains at the level of our formal *primitives*.

And that is properly our *symbolic* level, the one that simply "can-/will *not* be explained".  I.e. not any more than its own shape is its own *diagram* (or that "(its) nature is its own explanation"): ultimately, the idea/hope being, we cannot explain it but we can understand it to the point of *naming* it.

Indeed, a principle is "let code speak for itself", which means our formal language should be as readable as a natural language, just without the ambiguities, as the formal aspect "just" takes care that *code* cannot lie about *itself* (about its assumptions as well as derivations).

So, I think Leibniz's formal-encyclopedic project is by now doable, with applications potentially up to the legal context.  On the other hand, and exactly for reasons of concreteness and applicability, I do *not* think *we* can get away without the umbrella of a (trustless, hopefully) *contract*, where "it" takes the form of a (collaborative, hopefully) *game*-theoretic protocol, for *the acquisition, revision, consolidation and exercise of mutually informed and formally verified knowledge*.