Wednesday, July 15, 2026

Investigations into the Idris2 proof assistant and some formalizations

Is there a proof assistant which combines the best aspects of Coq/Rocq and Agda? We would like the construction of proof-terms be done in a natural deduction style, close to actual mathematical practice (at least for the proofs of category theory). This is different at once from the top-down method of constructing proofs in Coq/Rocq and from the emacs interface of Agda and its system of refinement, filling holes, etc.

Dependent type theory - extensions of type theories such as used in Ocaml and Haskell - seems to us philosophically, computationally, logically and practically the best foundation for mathematics. The elegant Idris 2 proof assistant - which we could call an idealized version of Agda (but with linear types!) - seems to be most promising. It is simple and versatile and can work with emacs, vim or nano. Could we use it as a basis to develop our natural deduction style interactive theorem proving?

Idris 2 with its REPL in fact feel like a enhanced version of Ocaml or Haskell (upon which it is based) - but it is not so easy to install (we are running it on an Ubuntu virtual machine in whih we need rlwrap to get command history).

We can seemlessly formalize category theory in Idris 2 (it seems this can be done in a simpler and more direct way than in Coq/Rocq) - a fact which is already of logico-philosophical significance.

https://github.com/owl77/Idris2_formalizations/blob/main/ct.idr

As an exercise we prove that any two terminal objects in a category are isomorphic. To do this we show first that given a terminal object T its canonical morphism to itself must be id_T (this is the lemma1 term). This is how in our natural deduction extension of Idris we would construct the lemma1 term in the way a mathematician would prove the result. 

1 c : Cat Hyp
2 a : obj C Hyp 
3 t : terminal c a Hyp
4 t : forall (x: obj c), exists (g : hom c (x,a)), forall (h: hom c (x,a)), h = g Expand 3
5 t a : exists (g : hom c(a,a)), forall (h : hom c(a,a)), h = g Inst 4,2
6 snd (ta) : forall (h : hom c (a,a)), h = fst (ta) Sigma type stuff
7 id c a : hom c (a,a) By def
8 (snd (ta)) (id c a) : id c a = fst (ta) Inst 6,7
9 (c : Cat)(a : obj c)(t : terminal ca), (snd (ta)) (id c a) : (c: Cat) -> (a : obj c) -> (t : terminal c a) -> h = fst (ta) QED

Monday, July 13, 2026

Critique of Quantum Mechanics and Quantum Field Theory

Here we will present some short logical and philosophical critiques and questions concerning quantum mechanics and quantum field theory with the ultimate goal of going beyond these theories and constructing more satisfactory ones. We will also attempt to bridge the gap between some of our previous speculations and the actual mathematical structure of quantum theory.

We focus on the collapse of the wave-function. But the root of the problem can already be found in the singular situation of observables corresponding to Hermitian operators while the temporal evolution of the state of a system corresponds to unitary operators. The collapse is essentially a projection onto an eigenvector. In classical physics measurement and observations are external to the system. In quantum mechanics they become internalized. The observation process, the applications of hermitian operators, suggest a highly sensitive non-linear response of a system whose nature is still not understood.

What if we viewed space as discrete (like the lattice structures used to explain free fields in QFT)? Then the wave function becomes just a finite vector, the space points mere indexes - just like time is a mere index. We loose the topology.  It is curious that  position can be promoted to an operator but time cannot. A time operator in quantum theory seems to be a notion derived from momentum and as such recalls the classical Aristotelian notion of time being a "measure of change".  

Understanding what the vacuum state $|0\rangle$ is in QFT is not easy - and many different accounts are given in the textbook of why the Green function takes on a particular interpretation of a particle being created at point $x$ and destroyed a point $y$.  Understanding what the spatial-temporally indexed operators are - and what measurements they correspond to - is also not easy. The creation and annihilation operators are not Hermitian and do not correspond to observations and measurements and yet Hermitian operators (or operator-valued distributions) can be written in terms of them.  These supposedly correspond to measurements.  We must first of all understand the Vacuum Expectancy Value, what $\langle 0 | \phi(y) \phi(x) | 0 \rangle$ means (which is obviously similar to the expected value in quantum mechanics $\langle \phi | A | \phi \rangle$). And understand it experimentally. The first $\phi(x)$ corresponds to the high-energy localized injection of a particle (perhaps the product of decay) while the second $\phi(y)$ could correspond to collision with a detector (which thus destroys the particle).

We think that the statistical mechanics motivations of second quantization and QFT is particularly interesting. Our "wave function" gives a probabilistic distribution over occupation numbers $(N_1,...,N_n)$. The interpretation of the creation and annihilation operators in this context is subtle. How are we really to understand

$a_i \Phi (N_1,...,N_i,...,N_k,...) = \sqrt{N_i} \Phi(N_1,...,N_i -1,...,N_k,...)$?

Too often we see physical metaphors applied rather vaguely to mathematical constructs. To us these operators only really make sense in the context of the rigorous formulation of Fock spaces (tensor products, symmetric and anti-symmetric products of Hilbert space $H$). Given an orthonormal basis $\epsilon_i$ of $H$ then the operator $\Sigma_{i=1}^\infty a^\dagger(\epsilon_i)a (\epsilon_i)$ has very clear properties ($Sv = nv$ for $v$ in the $n$th component of the Fock space), far more illuminating than speaking of "particle number". But of course Fock space pertains only to the theory of free fields. The general case, the perturbative case, seems intimately connected to the general concept of formal deformation of an object by formal power series (cf. quantum groups or Hopf algebras in general), but there is no rigorous mathematical structure for perturbative QFT.

 A central flaw in the theoretical treatment of QFT is that it systematically ignores the central unspoken role of human agency, the experimenter and experimental setup, behind the mathematical formalism. Operators (operator valued distributions) are treated as independent active entities in their own right which somehow decide to "act" on fields. The glaring shortcoming is that there is no clear criteria of demarcation between the human observer the what is observed - nature.  Can the measurement process itself be considered a natural process when considered and observed externally by a third observer ? Are Hermitian operators really then descriptions of something objective happening to the system, the external observed observer "zapping" or collapsing the system? And should not this whole process itself be capable of superposition?

This most curious situation: observables must correspond to Hermitian operators - this can be deduced by the requirements of measurement in a probabilistic framework. Also, the unperturbed evolution of a system corresponds to unitary operators (or in the Heisenberg picture conjugation of observables by unitary operators). But what a coincidence that - for a finite discrete approximation - the lie algebra of the unitary group is the space of anti-hermitian operators - itself isomorphic (via multiplication by $i$) to that of hermitian operators. That is, every unitary matrix is can be written $e^J$ for $J$ anti-hermitian or $e^{iH}$ for $H$ hermitian. So measurements correspond to objects in the tangent space of the group of unitary operators - but they are also applied in their own right to the wave function.

Why could not the total energy of the vacuum be infinite? Why could not the total energy of the universe be infinite and yet there be still, in some sense, conservation of energy?  For instance we could have a countable infinite collection of non-communicating finite universes with finite energy and in which the conservation of energy held. Then the total set of universes would be a universe with infinite energy in which there was still conservation of energy in a meaningful sense.  We could even allow communication between the finite components satisfying a conservation law.

It is curious how the discreteness of the energy states is connected to the finitude of the system. 

The vacuum state in QFT is similar to consciousness (to alayavijñana) - and we can argue that classical field theory could never be an adequate representation.

We have discussed before the interest of considering material and energetic constraints in information - and this is precisely the idea behind linear logic (Girard's first papers explicitly mention chemistry), as well as partially already present in the memory management aspect of programming languages. QFT scattering is a lot like communication with material constraints.  The "answer" of the system has to be materially destroyed to be received.

This is certainly a bizarre idea, but could it be that the experiments with LHCs are not teaching us about nature but rather a kind of training process analogous to AI? Nature is changing her habits in conformity to what physicists want to observe? And finally consider how we attempted previously to characterize the massive datasets which allowed LLMs to be trained and perform as they do.  The qualities of the massive data sets in question could they not correspond to fundamental properties of the vacuum or quantum fields in general? Of course the analogy is limited because of the apparent inescapable indeterminism in QFT while LLMs are just deterministic automata.

Type theory / QTF analogy.   Type = Operator, Term inhabiting a type = Vector and application of operator to the vector,  Simply Typed Lambda-Calculus = Quantum Mechanics, Dependent Type Theory = Quantum Field Theory, operators depend on values. Loops, non-termination = infinities. 

Foundationalism and Logic

The point in question concerns the problems of foundationalism involving type theory or term-rewriting systems. In the final part of my Kantian-oriented paper "Analyticity, Computability and the A Priori" I attempt to tackle with this problem (as well as presenting in greater detail my analysis of term-rewriting systems, Turing completeness, the Curry-Howard correspondence and the limits of logic-like formal systems in representing all computable functions and extracts on Hilbert's philosophy taken from a paper by Claire Ortiz Hill). I propose in the end a methodology inspired Piaget's genetic epistemology in which one must effect a sort of regression to relive in a conscious way the stages since early childhood whereby one progressively gained computational competency - centered around the ability to understand, carry out and check the following of rules - and to compare the cognitive structures involved to formal systems and computational models at our disposal. While this cannot lead to the enthroning of any single formal system or model it can, I believe, nevertheless bring to light groups of specific systems and models which are "structurally akin" and "cognitively natural" to consciousness itself. While we cannot enthrone a single system, I believe we can use the language of a given system to express what are in the Kantian terms synthetic a priori principles of the human understanding. For instance when we find a finite derivation in one formal system (the metasystem) and conclude that this derivation "shows" that a certain goal cannot be derived in another system (the object system), which is something that we cannot directly show in the object system because it would require an infinite amount of time. Gödel's incompleteness theorem is (and has to be) formalizable and corresponds to a finite derivation in a system M. But it must be assumed that this finite derivation is sufficient epistemic grounds to conclude something about the infinite set of derivations in Peano Arithmetic, that the sentence G cannot be derived.  

Saturday, July 4, 2026

A thesis on generative AI

We present to following thesis on generative AI.  That to understand fully the essence of generative AI we must first understand the socio-cultural and philosophical essence of the advent of the internet.  Generative AI is only possible not merely because of raw hardware capabilities and certain neural net architectures and training processes, but on a more fundamental level because of the nature of the large data sets employed. Generative AI is only possible because of the previous availability of a very special kind of massive data set - precisely the kind of data sets provided by the internet. Generative AI is simply the natural further development of the same factors at work in the genesis of the internet.  So our main task is to describe the nature of internet data as well as its social, psychological, linguistic and cultural correlates.  This is a difficult task. One should consider and evaluate the following aspects: the democratization of knowledge and expertise (what certain authors once called "the cult of amateurism"), the lessening of the both the physical and semantic volume of content - flattening of layers of semantic depth, connotation, subtext and extra-textual reference, a  massive atomization and repetition with small variants of certain templates, memes and "virality", propagation and reproduction of persistent psycho-linguistic patterns throughout the whole body of the data - all which structurally contribute to forming the kind of atomized, grid-like, decentralized, self-entangled and self-connected  massive data set which is precisely what allows the generative AI technology to produce LLMs which perform as they do. While traditional cultural-linguistic data involved relatively few authors with massive linguistic content, the internet data involves a massive amount of authors with relatively scarce linguistic content each.  Humanity is caught itself in the textual universe of the internet.  The internet data set can be described as an enmeshed chaos of micro cognitive-linguistic units - which we can compare to the set P of partial information used in forcing. If we wish to combat generative AI we need to get at the root of the whole historical-cultural process involved in the genesis of the internet. We need to instigate a revolution regarding authorship, epistemic authority and the nature of the written text. The semantic web project should be revived. Curiously enough the Pali canon is an very early example of large textual data which exhibits some of the characteristics of internet data.

If the internet era was the era of communication, personal development through sharing and community, but now not only has the "internet" as a medium become content itself but it has become dead content, i.e., generative AI. Thus we are in the heroic age in which the human person must again find development and peace in isolation again - so that again there is something to share. The highest form of human knowledge must be global and synthetic, partial analysis has as its ultimate aim furnishing the support for such a knowledge. Global and synthetic knowledge is the only knowledge that frees one from Plato's Cave. 

Can we reverse engineering generative AI using generative AI? Could we train an AI model M on the data D = (T,L) consisting of training data T and a LLM L trained on T, to solve the following problem:

Given a prompt P fed into L and response R, identify the portions of T which can be considered as having (in some mode or another) the largest weight in the generation of R from P.

Can we define the concept of essential dependence of response R to P via L on a portion S of T? Could we train M to return, for a given P, portions of T which have a certain structural similarity to R?  

Wednesday, July 1, 2026

The bridge between logic and geometry - motivating the work of Olivia Caramello

There are several beautiful and profound foundational papers (many from the 1970s) on inituitionistic higher-order logic within the framework of topos theory. Papers by Lawvere, D. Scott, M. Fourman, G. E. Reyes and others which focus on the philosophical aspects of formal presentations of higher order intuitionistic logic inspired by the structure of elementary topoi: partial domains, sorts and types, definite descriptions, definability, non-classical truth values, the interpretation of bounded quantifiers, the axiom of infinity (NNOs), the Russell-Prawitz translation (Scott claims to have discovered this in the 50s), etc.
There is an elegant Hilbert-style formal presentation of intuitionistic higher-order logic employed by Fourman in his paper in the Handbook of Mathematical Logic.

In our paper "Hegel and Modern Topology" we proposed an interpretation of the the Logic of Concept wherein the stages of Subjective Concept and Objective Concept and their integration are interpreted in terms of the duality between theories and models (understood as a geometrically inspired category theoretic framework for general systems theory) and the problem of finding a bridge between the two - something which partakes of the essence of both, perhaps in the style of algebraic logic.

In the paper by Fourman he uses only the most rudimentary notions of category theory. The main result is that any (elementary) topos is equivalent (via a logical morphism) to the topos of a definitionally complete theory E(T) and that any theory T gives rise to a topos E(T). Thus the objects E(T) -  bearing in mind their universal property (theorem 8.9 in the paper by Fourman) - would seem to be a candidate for a bridge between theories and models. E(T) classifies models of T: there is a correspondence between models M of T and logical morphisms E(T) -> M.

But Fourman remarks (he terms it an "embarassement") that this still does not constitute a bridge between (higher-order) logic and geometry (i.e. Objective Concept), between theories and Grothendieck topoi and their geometric morphisms. Fourman mentions a paper by Reyes in which Grothendieck topoi are described in terms of adding to Set a "generic model" for a possibly infinitary first-order theory. 

As I see it some of the main problems with topos theory are the following:

1) Some of the toposes that I find most interesting, such as the Hyland's Effective Topos (a model of higher-order computable mathematics) are not Grothendieck toposes.
2) Even the Effective Topos still depends crucially on the category of sets (it is an enrichment of Set) - so it does not seem to provide in itself an alternative foundations for mathematics. However Fourman and Scott's theory of Omega-sets may provide a different perspective...
3) This needs to be checked, but I think that for a general topos with a Natural Number Object we cannot prove that there is no mono m: P(N) -> N. But for a Grothendieck topos the situation may be different...

A nice application of Grothendieck toposes is provided by Moerdijk and MacLane's treatment of forcing models in Sheaves in Geometry and Logic. I like to think of the underlying poset P as a kind of training data (partial information, not always consistent) and the construction of the sheaf model Sh(P) for the dense topology as analogous to models constructed by machine learning (a kind of passage to the limit, extrapolation and smoothing out of the data of P).

We have written in Ocaml a minimal proof assistant based on the logical system presented by Fourman in his paper The Logic of Topoi:

https://github.com/owl77/Intuitionistic-Higher-Order-Logic-and-Topos-Theory

Investigations into the Idris2 proof assistant and some formalizations

Is there a proof assistant which combines the best aspects of Coq/Rocq and Agda? We would like the construction of proof-terms be done in a ...