Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

1. • CommentRowNumber1.
   • CommentAuthorjesse
   • CommentTimeSep 6th 2016
   • PermaLink
   Author: jesse
   Format: MarkdownItexI've expanded Urs's entry on [[interpretation]]: models of theories in $\mathbf{C}$ are interpretations of theories in the [[internal logic]] of $\mathbf{C}$ are ([[cartesian logic|cartesian]], [[regular logic|regular]], [[coherent logic|coherent]], [[first-order logic|first-order]], [[geometric logic|geometric]]) functors out of the [[syntactic categories]] of those theories. I also mention a _concrete_ notion of interpretation (of models---of possibly different theories---in each other) that came into use among model theorists in the 80s and 90s, when people were trying to reconstruct $\omega$-categorical theories from the automorphism groups of the countable model. I then mention some facts (I have proofs spelled out somewhere, but I'm sure they're folklore) linking these concrete interpretations to the first notion of interpretation. If I recall correctly, there isn't a unified treatment in the various pages under the contexts of [[type theory]] and [[categorical logic]] treating the adjunction between taking [[syntactic categories]] and [[internal logic|internal logics]]. I'll try to get all that down in a single page in the future.

   I’ve expanded Urs’s entry on interpretation: models of theories in $\mathbf{C}$ are interpretations of theories in the internal logic of $\mathbf{C}$ are (cartesian, regular, coherent, first-order, geometric) functors out of the syntactic categories of those theories. I also mention a concrete notion of interpretation (of models—of possibly different theories—in each other) that came into use among model theorists in the 80s and 90s, when people were trying to reconstruct $\omega$-categorical theories from the automorphism groups of the countable model. I then mention some facts (I have proofs spelled out somewhere, but I’m sure they’re folklore) linking these concrete interpretations to the first notion of interpretation.

   If I recall correctly, there isn’t a unified treatment in the various pages under the contexts of type theory and categorical logic treating the adjunction between taking syntactic categories and internal logics. I’ll try to get all that down in a single page in the future.

2. • CommentRowNumber2.
   • CommentAuthorDavid_Corfield
   • CommentTimeSep 6th 2016
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexPerhaps we should have there something on Olivia Caramello's bi-interpretation, e.g., as mentioned [here](https://nforum.ncatlab.org/discussion/4834/morita-equivalence/?Focus=52603#Comment_52603). And the concept there of a 'bimodel'.

   Perhaps we should have there something on Olivia Caramello’s bi-interpretation, e.g., as mentioned here. And the concept there of a ’bimodel’.

3. • CommentRowNumber3.
   • CommentAuthortonyjones
   • CommentTimeSep 6th 2016
   • PermaLink
   Author: tonyjones
   Format: MarkdownItexWasn't sure where to post this. Dimitris Tsementzis has a paper out on Homotopy Model Theory: [Homotopy Model Theory I: Syntax and Semantics](https://arxiv.org/abs/1603.03092) ''A model theory in the framework of Univalent Foundations requires a logic that allows us to define structures on homotopy (n-)types, similar to how first-order logic can define structures on sets. We define such an "n-level" logic for finite n. The syntax is based on a generalization of Makkai's FOLDS, obtained by an operation that allows us to add equality sorts to FOLDS-signatures. We then give both a set-theoretic and a homotopy type-theoretic semantics for this logic and prove soundness for both with respect to an appropriate deductive system. As an application, we prove that univalent categories are axiomatizable in 1-logic.'' Brice Halimi is also working on a related approach. He has some slides on his website, but the paper isn't available yet: [Homotopy Model Theory](https://bhalimi.u-paris10.fr/wp-content/uploads/2014/07/homotopy_model_theory_LC.pdf) Halimi has also been doing some work connecting modal logic and differential geometry which David might be interested in: [Geometric Model Logic](https://bhalimi.u-paris10.fr/wp-content/uploads/2014/07/BCAP_geometric_modal_logic.pdf) [Fibred Structures for Modal Logic](https://bhalimi.u-paris10.fr/wp-content/uploads/2014/07/fibered_structures12_cippmi.pdf) Finally, Halvorson and Tsementzis et al. have a series of papers on applications of category theory to question such as theoretical equivalence in philosophy of science: [Scientific Theories](http://philsci-archive.pitt.edu/11347/1/sci-theories.pdf) [Categories of Scientific Theories](http://philsci-archive.pitt.edu/11596/1/categories-scientific-theories-4.pdf) [Morita Equivalence](http://arxiv.org/pdf/1506.04675) [Glymour and Quine on Theoretical Equivalence](http://philsci-archive.pitt.edu/11341/1/glymour%26quine.pdf) [Theoretical Equivalence in Classical Mechanics and its Relationship to Duality](http://philsci-archive.pitt.edu/11695/1/theoretical-equivalence-classical_(1).pdf)

   Wasn’t sure where to post this. Dimitris Tsementzis has a paper out on Homotopy Model Theory: Homotopy Model Theory I: Syntax and Semantics

   ”A model theory in the framework of Univalent Foundations requires a logic that allows us to define structures on homotopy (n-)types, similar to how first-order logic can define structures on sets. We define such an “n-level” logic for finite n. The syntax is based on a generalization of Makkai’s FOLDS, obtained by an operation that allows us to add equality sorts to FOLDS-signatures. We then give both a set-theoretic and a homotopy type-theoretic semantics for this logic and prove soundness for both with respect to an appropriate deductive system. As an application, we prove that univalent categories are axiomatizable in 1-logic.”

   Brice Halimi is also working on a related approach. He has some slides on his website, but the paper isn’t available yet:

   Homotopy Model Theory

   Halimi has also been doing some work connecting modal logic and differential geometry which David might be interested in:

   Geometric Model Logic

   Fibred Structures for Modal Logic

   Finally, Halvorson and Tsementzis et al. have a series of papers on applications of category theory to question such as theoretical equivalence in philosophy of science:

   Scientific Theories

   Categories of Scientific Theories

   Morita Equivalence

   Glymour and Quine on Theoretical Equivalence

   Theoretical Equivalence in Classical Mechanics and its Relationship to Duality

4. • CommentRowNumber4.
   • CommentAuthorUrs
   • CommentTimeSep 6th 2016
   • PermaLink
   Author: Urs
   Format: MarkdownItex> Wasn't sure where to post this. In such cases I just try to put these References into aticles in a way that would help me myself to find them again later. Specifically regarding _[[homotopy model theory]]_, why not simply create this entry, cross-link both with [[homtopy typpe theory]] and with [[model theory]] and then record the references there. Anyway, thanks for collecting all this!

   Wasn’t sure where to post this.

   In such cases I just try to put these References into aticles in a way that would help me myself to find them again later. Specifically regarding homotopy model theory, why not simply create this entry, cross-link both with homtopy typpe theory and with model theory and then record the references there.

   Anyway, thanks for collecting all this!

5. • CommentRowNumber5.
   • CommentAuthorTim_Porter
   • CommentTimeSep 6th 2016
   • (edited Sep 6th 2016)
   • PermaLink
   Author: Tim_Porter
   Format: MarkdownItexI have created a web page for [[Brice Halimi]] as I know him slightly. One of his papers is in the Annales .... de Toulouse (Proceedings of a Conf. on homotopy and philosophy). I will put links on the new page.

   I have created a web page for Brice Halimi as I know him slightly. One of his papers is in the Annales …. de Toulouse (Proceedings of a Conf. on homotopy and philosophy). I will put links on the new page.

6. • CommentRowNumber6.
   • CommentAuthortonyjones
   • CommentTimeSep 6th 2016
   • PermaLink
   Author: tonyjones
   Format: MarkdownItexSome of Tsementzis' slides relating to the work cited above: [A Syntactic Characterisation of Morita Equivalence, at Leeds University, Logic Colloquium 2016, Tuesday, August 2, 2016](http://scholar.princeton.edu/sites/default/files/dtsement/files/tmor.iff_.jmor_.talk__0.pdf) [Homotopy Model Theory, at Leeds University, Workshop on Categorical Logic and Univalent Foundations, Thursday, July 28, 2016](http://scholar.princeton.edu/sites/default/files/dtsement/files/hmt.online.version.pdf)

   Some of Tsementzis’ slides relating to the work cited above:

   A Syntactic Characterisation of Morita Equivalence, at Leeds University, Logic Colloquium 2016, Tuesday, August 2, 2016

   Homotopy Model Theory, at Leeds University, Workshop on Categorical Logic and Univalent Foundations, Thursday, July 28, 2016

7. • CommentRowNumber7.
   • CommentAuthorjesse
   • CommentTimeSep 6th 2016
   • PermaLink
   Author: jesse
   Format: MarkdownItex> Perhaps we should have there something on Olivia Caramello's bi-interpretation, e.g., as mentioned [here](https://nforum.ncatlab.org/discussion/4834/morita-equivalence/?Focus=52603#Comment_52603). And the concept there of a 'bimodel'. @David: the notion of interpretation and bi-interpretation defined by Olivia at the end of her 6.3 seems to be precisely the notion of [[interpretation]] in the entry. If I'm reading the linked thread correctly, a 'bimodel' describes a situation where, given an interpretation $T_1 \to T_2$, we can take the reduct of any model $M$ of $T_2$ to obtain a model $M|_{T_1}$ of $T_1$ (i.e. precomposing the logical functor $M : \mathbf{Def}(T_2) \to \mathbf{Set}$ by the logical functor $\mathbf{Def}(T_1) \to \mathbf{Def}(T_2)$.) Is that right?

   Perhaps we should have there something on Olivia Caramello’s bi-interpretation, e.g., as mentioned here. And the concept there of a ’bimodel’.

   @David: the notion of interpretation and bi-interpretation defined by Olivia at the end of her 6.3 seems to be precisely the notion of interpretation in the entry.

   If I’m reading the linked thread correctly, a ’bimodel’ describes a situation where, given an interpretation $T_1 \to T_2$, we can take the reduct of any model $M$ of $T_2$ to obtain a model $M|_{T_1}$ of $T_1$ (i.e. precomposing the logical functor $M : \mathbf{Def}(T_2) \to \mathbf{Set}$ by the logical functor $\mathbf{Def}(T_1) \to \mathbf{Def}(T_2)$.) Is that right?

8. • CommentRowNumber8.
   • CommentAuthorDavid_Corfield
   • CommentTimeSep 7th 2016
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexJesse, there are people here who know much more than I do, but I think there can be a bimodel without there being an interpretation between theories, just as the existence of a bimodule between two rings doesn't indicate a morphism between them.

   Jesse, there are people here who know much more than I do, but I think there can be a bimodel without there being an interpretation between theories, just as the existence of a bimodule between two rings doesn’t indicate a morphism between them.

9. • CommentRowNumber9.
   • CommentAuthorjesse
   • CommentTimeMay 25th 2017
   • (edited May 25th 2017)
   • PermaLink
   Author: jesse
   Format: MarkdownItexI added a brief remark (which was oddly missing) that interpretations of theories are the inverse image parts of [[geometric morphisms]] between their [[classifying toposes]] (up to [[Morleyization]] and taking [[pretopos completion|pretopos completions]] of the syntactic sites.)

   I added a brief remark (which was oddly missing) that interpretations of theories are the inverse image parts of geometric morphisms between their classifying toposes (up to Morleyization and taking pretopos completions of the syntactic sites.)