Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
1 to 23 of 23
Is there likely to be anything (other than working out the details) to stand in the way of reconstruction theorems showing the duality between homotopy type theories and their collections of models?
I was wondering, by the way, because at last there’s some philosophical interest in theory-model duality from a new quarter. People are trying to think of equivalence of scientific theories in terms of equivalence of their categories of models. But given that physics naturally takes place in an -topos, perhaps we need to move up the ladder a little.
at last there’s some philosophical interest in theory-model duality from a new quarter. People are trying to think of equivalence of scientific theories in terms of equivalence of their categories of models.
Which discussion is this alluding to? Do you have a pointer to who these people are and what they are saying?
James Weatherall and Hans Halvorson. If you scroll down the former’s page to ’Category theory in the philosophy of science’. I asked James for a draft of his paper which argues that category theory provides a good way to capture equivalence between theories via equivalence between categories of models.
Thanks!
But one question: does anyone use a sufficiently formalized notion of what a “physical theory” is to even be able to formally ask for a formal duality with the collection of models? I thought finding a good formalization of the notion of “physical theory” is still mostly open. I remember we used to have some semi-heated discussion about this once.
By the way, while looking for the references that you gave, I discovered that we had a hidden stub entry syntax - semantics duality. I have now expanded that ever so slightly and then cross-linked it to a bunch of other entries.
There are still coherence issues that we don’t fully understand in making a correspondence between homotopy type theory and higher categorical models. We don’t know whether the desired categorical models can always be strictified to match extant type theories, or exactly how extant type theories would need to be weakened to match the categorical models. But modulo this, I don’t think there should be any obstacle.
Re #5, good to know. Thanks.
Re #4, right the lack of formalized notion of physical theory is what motivates the thought to look at the collection of models, the so-called “semantic view of theories”. So what if we took the duality seriously and tried to extract a theory from a collection of physical models?
Ah, I see. Hm, but that just leads me to the next question: what are all models of a physical theory? Maybe the duality that is supposed to come to the rescue also prevents me from knowing one without the other?
We need to fix something before we make progress here, it seems to me. Let’s see. After a brief look at Weatheall’s page I get the impression that by “physical theory” he entirely means a system of classical mechanics. Moreover, I suspect that if I followed the links, I would discover that he moreover entirely means a Langrangian incarnation of classical mechanics: a physical theory is the a function on some differentiable space and in particular the critical locus of that function.
If we agree that “a (local) Lagrangian is a physical theory”, then it’s not too hard to formalize this in some evident way and to classify such theories. Physicists do this typically whenever they speak about “two theories being classically equivalent”, which mainly means that two different action functionals on the same or on comparable domains have coinciding critical locus.
But is this a notion “theory” in the sense of logic? What are the models? Is not a given Lagrangian itself rather a model of the theory “physical theories”?
But before we continue with this (if we do) one general question: does anyone of these authors claim to have formalized what a “model of a theory of physics” is, or similar? Can I look at some article to see what precisely is being discussed? Or is this all happening more at a vague level?
Halvorson’s article stays very much in the realm of logic. Still you get a good idea of what has exercised people in debates over the nature of a scientific theory. Whenever I used to look in on the debate, I wished to see some concrete examples of how this approach would work.
In the case of Weatherall’s article we get to see some examples. There’s a comparison of Newtonian gravitation with Newton-Cartan theory, and one of two formulations of electromagnetism. The question then is under which notion of theoretical equivalence do these theories turn out the same.
The models for electromagnetism are
The former form a groupoid with morphisms isometries. The latter groupoid needs the addition of morphisms for gauge equivalence.
The case of Newtonian gravitation has as models: a manifold, compatible space and time metrics, and derivative operator, with mass-momentum field. Then you get the divergence between flat space-time with scalar gravitational field satisfying Poisson’s equation, and the case where the derivative operator is permitted to be curved and the gravitational field is omitted. A similar approach to the groupoid of models with gauge equivalence is adopted.
Thanks. Concerning those examples of “models” I see now what is meant.
But I feel hesitant to follow this use of language. Maybe I should look at their articles first (no time really right now).
Since all this is apparently utterly restricted to classical physics, let’s forget the physics connotation for a second and just isolate the mathematical structure that we are talking about:
Consider the structure given by a differentiable space (configuration space) equipped with a subspace (phase space).
Consider then the structure given by a differentiable space equipped with a differentiable function .
An example of the second structure gives rise to one of the former by sending to the inclusion of the criticial locus of into .
Now: in which sense is the first of these a “theory” while the second is a “model of the theory”?
(Because this seems to be what these authors say.)
Now: in which sense is the first of these a “theory” while the second is a “model of the theory”?
I’m not sure I see why you think the authors would say that the phase space structure is a theory. Wouldn’t they see both the category of s and the category of s as categories of models?
Taking things from your own starting point, given all the work represented at nLab, what can we say about physical theories and their models? Do we have a notion of when theories are equivalent? Is there any hope of seeing cases of theory-model duality in the case of physics?
Wouldn’t you describe what you’re doing here as establishing a certain equivalence between FQFT and AQFT, at least in one direction?
what can we say about physical theories and their models?
I am still not sure if this is the right thing to ask. Is there maybe a risk of being misled by different meanings of the word “theory”?
Notice that physicists frequently say “theory” as well as “model” for “a Lagrangian”. Just compare the standard model. This is a physical theory! :-)
What seems more sensible to me would be to ask for the theory-as-in-logic of which a theory-as-in-physics is a model.
If one wishes, something like this might be extracted from formulation of physics in the axioms of differential cohesion. Here you could say something like “the theory-as-in-logic of theories-as-in-physics is the theory of maps of the form ”. Any given theory-as-in-physics is then a model of this theory-of-physical-theories.
(I am not claiming that this is a very comprehensive notion of theory-of-physical-theories, but it seems to be at least as good as what the authors mentioned above have in mind.)
Do you see what I mean?
Or take, for definiteness, the formulation of quantum field theories as functors on . Are not all these functors models of one single theory-of-QFTs in the sense of logic? What should the distinction that the above authors make between “physical theory” and “model of a physical theory” be in this context?
This is all quite strange for me as one who has been criticised over the years for casting doubt on formal approaches to philosophy, but…
I had noted somewhere that physicists’ use of “theory” and “model” was quite variable, and certainly not as straightforward as the logicians’. After the idea of scientific theory as syntactical theory, and then the ’semantic view’ of theories as collections of models, there came a more realistic third position, which saw models as mediators, intermediate between theories and data. Models could even involve a story-like quality, such as for the bag model in hadron physics.
But I guess here we’re situated at the ’theory’ end of physics, wondering whether we can make sense of these theories as models of a logical theory. So can we form a category of some kind of maps of the form ? Presumably, we can continue to specify the theory-as-in-logic by specifying the or the , or adding other axioms.
I had noted somewhere that physicists’ use of “theory” and “model” was quite variable, and certainly not as straightforward as the logicians’.
I think the crucial difference is that in physics there is a third actor in the game. Called Reality. Just as the logicians say “model” for “something that matches the constraints of a theory”, so the physicists say “model” for “something that matches the constraints of reality”.
But then, once a model matches some list of observed facts about reality, it also induces values of yet un-observed aspects of reality (what physicist call a “prediction”), and hence then it becomes a theory about reality.
So can we form a category of some kind of maps of the form ?
Yes, there are some obvious things one can do. But, fond as I am of this, it is as yet a bit too crude to qualify as a “theory-of-physical-theories”. After all – and we have talked about this several times before – for a full such notion there must be some element that relates these structures to “observation” and then things become really thorny, at least in our present understanding.
Presumably, we can continue to specify the theory-as-in-logic by specifying the or the , or adding other axioms.
Yes.
Oh, I thought I’d added a comment yesterday, but it’s not here. It was just to point out that the story of models in physics is made more complicated by toy models, e.g., the Ising model and critical phenomena in universality classes, and (2+1)-quantum gravity. On the other hand, perhaps the study of ranges of model which are not physical in some way relieves us slightly of the constraints of your third actor – Reality.
Philosophy has tried to extract types of model and arrived at
Probing models, phenomenological models, computational models, developmental models, explanatory models, impoverished models, testing models, idealized models, theoretical models, scale models, heuristic models, caricature models, didactic models, fantasy models, toy models, imaginary models, mathematical models, substitute models, iconic models, formal models, analogue models and instrumental models are but some of the notions that are used to categorize models.
If category theory could help in philosophy of science, you’d think it would be in the area of theory equivalence.
I certainly agree that one commonly and frutifully considers models in physics which are not in fact very closely linked to reality. But in principle I think there still remains a different meaning of the word “model”.
It seems to me that actually the word “model” as used in physics is closer to the original meaning of the word than the way it is used in logic. The word “model”, it seems to me, alludes to “a (small scale) approximation of a phenomenonan that in itself is larger and more detailed”. This is very close to what physical models are.
On the other hand, the idea in formal logic that a structure may be a “model of some axioms” is rather more remote from the intuitive idea of “model”, isn’t it? In particular since such models-as-in-logic have to accurately reflect every single detail of what they are modelling. In logic it is the models that are richer than what they are modelling. In physics and in everyday language, it is the other way around.
On the other hand, the phenomenon in physics that a model is at the same time a theory is also familiar in logic: for every model we can ask for the theory it generates, which has each property of that model as an axiom. This is precisely the way it works in physics: first we measure a (small) set of data points (“physical parameters”), then we construct a model that reproduces these, and then we take all the other properties of the model as the new predictions of a new theory. (And then it iterates: next we measure more, refine the model if necessary, and so ever on.)
It does seem to be true that the logician’s use of “model” is different from, and maybe backwards to, the physicist’s.
At Quantum Physics and Logic 2011 I showed a fictional dialogue between a logician and a physicists, amplifying how they can’t talk to each other. It’s at the beginning of these pdf slides.
The physicist starts out claiming that he has a “theory” and the logician, who is trying to understand which one it is, gets ever more puzzled by the explanations that the physicist offers. It gets only worse when he asks for the models of the theory. (Around slide 30).
Originally I had thought of adding one last line: the logician, almost exhausted, would make a last attempt and ask
I don’t get it. What is even the signature of your theory?
to which the physicist would cry out:
Lorentzian signature!
at which point the logician faints.
Back then I didn’t add this because I was afraid it would be getting too slapstick. But maybe I should really add that last part…
It would be fun if the physicist and logician reappeared at the end. How could they talk to each other then?
Thanks, that’s a good point. I’ll maybe make another copy of the slides, when I find a minute.
Right, so at the end the two could meet again and the logician might say:
Ah, now I get it.
What you called a theory at the beginning is what I would call a class of models, namely models for the theory of cohesive homotopy types equipped with a choice of object , a choice of abelian -group and a choice of map .
Your class of models is that where this arises from an operation of Lie integration of an -algebra with binary invariant polynomial, which I could also formulate as a model of a theory of differential cohesive homotopy types.
What you called a model, finally, I would call a specific model of this class of models.
a model of general relativity is a relativistic spacetime (a smooth four dimensional manifold with a Lorentzian metric). A model of electromagnetism is a Lorentzian manifold with a smooth antisymmetric field satisfying Maxwell’s equations (relative, perhaps, to some source current density).
Why don’t you consider metrics that satisfy Einstein’s equations? Ricci flat metrics for vacuum general relativity, Einstein manifolds for vacuum general relativity with cosmological constant, Einstein-Maxwell spacetimes for Einstein-Maxwell theory, and so on.
Now, it seems to me that models in this sense are not L-structures for some language L.
But the space of all such models is: namely that’s the critical locus of some action functional. This is what you call a “model” above: a point in the solution space of the Euler-Lagrange equations of an action functional.
And critical loci are models of a theory in the sense of logic. Notably in cohesive homotopy type theory, which is particularly well suited for axiomatizing this, critical loci are models of the type theory plus some axioms like this:
the moduli stack of fields is a type , the spacetime is a type , the phase is a type , the action functional is a function type
the variation of the action is the composition with the map (which exists by the axioms of cohesive homotopy type theory)
Finally the critical locus = solution space of the Euler-Lagrange equations of this action functional is the homotopy fiber
formed in the context of the étalification of this map (which exists by the axioms of differential cohesive homotopy type theory).
This is discussed in a bit more detail in section 3.10.8 of my notes differential cohomology in a cohesive topos. Some exposition is also at geometry of physics, though that is lagging behind in terms of writeup a bit.
1 to 23 of 23