Can proof assistants reflect the informal notion of a “theory” as the formally logical notion of a “theory”?

Question

Let us say that I wish to study and understand gauge symmetry using a formally verified mathematical programming language like Lean or Coq.

Lean has many libraries you can import to express mathematical concepts from a certain field of math, like set theory, logic, and others like topology and differential geometry and so on, I assume.

I am wondering if something like the “theory” of gauge symmetry could be seen as the same thing as the word “theory” in logic - the collection of all true statements resulting from some axioms.

So, in order to “study gauge symmetry”, it would actually be a matter of identifying what essential rudimentary logical statements are necessary to derive the important concepts and theorems in gauge symmetry (and those axioms being precise enough to exclude theorems from other fields.)

In other words, if we enumerated all sentences of some logic (say, first order logic), I assume all the theorems about gauge symmetry would be in there, but they would be too “hard to find”. Therefore, the actual task is adding certain axioms to first order logic, and only studying the theorems that come directly from enumerating all true statements coming directly from those axioms.

Is this possible? Is this a reasonable approach? What would come closest or be most similar?

---

For example:

A gauge symmetry of a Lagrangian $L$ is defined as a differential operator on some vector bundle $E$ taking its values in the linear space of (variational or exact) symmetries of $L$.

(Wikipedia)

Assuming we can define a Lagrangian system in the programming language (a pair $(Y, L)$, consisting of a smooth fiber bundle $Y \rightarrow X$ and a Lagrangian density $L$), and a gauge symmetry, would it be standard to try to constrain an automated theorem prover to only enumerate new theorems which make use of an initial statement (e.g., the definition of a gauge symmetry), combined with the formation rules of the logic? Does this count as a “fragment” of the logic, since we aimed to generate only a subset of the theory of the enclosing logic?

Answer 1

Your question is unclear. If your question is about practical concerns, I'm not exactly sure what you are asking. Can you define gauge symmetry in Lean or Coq? Almost certainly yes! It shouldn't be harder than any other similar area of mathematics.

Can you enumerate the theorems that mention your new concept GaugeSymmetry? I guess, but you would get a bunch of junk like GaugeSymmetry = GaugeSymmetry and ∀ (x : GaugeSymmetry), 1=0 -> True. And even without stuff quite so silly, I would be surprised if you find a good solution to this combinatorial explosion.

But more importantly, I don't understand what you are looking to do here. Why do you want this?

---

I think there is some confusion on the terminology of "theory", or of how Lean or Coq is typically used.

In its most general form, a "theory" in mathematics is when we have stumbled upon the right definitions. In the theory of topology, we have the definitions of topology, open, closed, compact, limit, and so forth. This "theory" forms the basis for a whole new understanding of other areas of mathematics. It sounds like gauge symmetry already has that. So you certainly should be able to write the definition of gauge symmetry in Lean and formalize theorems about it, but I don't think doing that is going to give you any brilliant new insights, except possibly as a way to systematize and record all the known knowledge in this field.

Another use case of the terminology "theory" is when one has a completely formal semantics of some mathematical notion. A recent example of this is homotopy type theory, which is a formal language for working directly in something like the infinity groupoid formed by homotopy spaces (I'm probably messing this up). This allows one to do synthetic homotopy theory, proving things about say the homotopy groups of the sphere without having to first go through topological spaces, etc. But, working in a formal system like Lean or Coq doesn't automatically give you a synthetic version of your field. Indeed, despite Lean's foundations being based on dependent type theory, just like homotopy theory, the proofs of Lean's homotopy theoretic results follow similar proofs to those found in the informal literature.

Finally, in logic, "theory" can sometimes mean a very particular thing, namely the set of all statements in some specific logical vocabulary, usually in first-order logic, which holds of a class of objects. Sometimes these theories uniquely classify that family of mathematical objects, like the theory of groups. Other times, they only get as close as you can get in first-order logic, like the first-order theory of the real numbers, which gives rise to the more general notion of a real-closed field. But in both examples, there are lots of important properties that are not expressible in first-order logic, like cyclic groups or the Archemidian property of the reals. Knowing which properties are first-order definable and which aren't is important since the former are preserved by logical gadgets like ultra-products. Also, the first-order theory of the reals is a decidable theory with nice properties like quantifier elimination.

But a first-order theory is usually not the place to prove theorems. You can't do modern group theory in the first-order theory of groups, nor can you do analysis in the first-order theory of the real numbers. It just is not powerful or expressive enough. You can't prove (or even state) Bolzano–Weierstrass in the theory of real-closed fields. For that, you need to bring in all sorts of objects outside of first-order group theory like the integers, set theory, and the like.

You can, however, prove Bolzano–Weierstrass, and most all other theorems of mathematics, in ZFC (which is also a first-order theory) because ZFC is a more powerful and expressive theory, but without the nice properties of say the theory of real-closed fields. Working in Lean (which is not a first-order logic) is more like working in ZFC. It isn't used for its nice metatheory properties but for its expressiveness and practicality. We don't make a distinction between the Lean or Coq statements that concern, say, groups and those that concern topological spaces. Indeed, it is important that we can talk about both in the same theorem so that we can talk about topological groups for example. Similarly, if you developed gauge symmetry in Lean or Coq, you would have access to all of Lean's or Coq's theorems and definitions for other related fields of mathematics.