3

A given theory, say Intuitionistic Propositional Calculus, can have multiple semantics. E.g, we have Heyting Algebras, Kripke models, topoi, etc. For each of this semantics, we have then a different meaning of $\Gamma \vDash \varphi$. Is there any way to relate these different meanings of $\vDash$? Maybe some sort or category, though it's not clear what the morphisms would be.

Fernando Chu
  • 2,511
  • 8
  • 22
  • Why do you say we have different meanings of $\Gamma \models \phi$? Isn't the point that we have many ways of defining $\Gamma \models \phi$, but they all give the same result? – Rob Arthan Jan 05 '24 at 22:35
  • 2
    Well, I guess depends on what 'meaning' means. If you expect that soundness and completeness holds, then $\Gamma \vDash_{1} \phi \iff \Gamma \vDash_{2} \phi$. But I don't think it's a good idea to make such a restriction. For example, one can use 3-valued truth tables to "model" intuitionistic logic, and show that LEM does not follow in IPC, but then this $\vDash$ does not satisfies completeness. – Fernando Chu Jan 05 '24 at 22:42
  • Even if we require $\Gamma \vDash_{1} \phi \iff \Gamma \vDash_{2} \phi$, I would think we should differentiate them somehow. For example modelling classical propositional logic, the truth-tables semantics seem more minimal (terminal?) than the boolean algebras approach. – Fernando Chu Jan 05 '24 at 22:47
  • I think it would make more sense to phrase your question in terms of models rather than notions of what $\models$ means. You then do get a category of models of the language of propositional calculus, following the usual approach of universal algebra, with Heyting algebras, boolean algebras and things like your 3-valued algebras all playing their part. With Kripke models, you have to do some work to extract the algebraic view of a model. – Rob Arthan Jan 05 '24 at 22:57
  • @FernandoChu could you give a reference – Julián Jan 05 '24 at 23:05
  • @RobArthan Could you elaborate on that category please? That sounds like the answer I'm looking for. – Fernando Chu Jan 05 '24 at 23:10
  • @Julián for which part? You can find references for the semantics I mentioned (except topoi) in wikipedia. – Fernando Chu Jan 05 '24 at 23:10
  • 1
    Probably worth mentioning that topoi (toposes) are a generalization of the others mentioned, so one could just work in the category of toposes and geometric morphisms, at least for the given examples. – cody Jan 05 '24 at 23:21
  • @FernandoChu Excuse me, I didn't notice I had sent that comment, I hadn't finished writing. I never saw that 3-valued truth tables you speak of. Is it this https://en.wikipedia.org/wiki/Three-valued_logic ? – Julián Jan 05 '24 at 23:22
  • 1
    @Julián I found it here. – Fernando Chu Jan 05 '24 at 23:28
  • @cody: good point. Does topos theory embrace wilder examples of semantics for propositional logic like the multiplicative fragment of linear logic? – Rob Arthan Jan 05 '24 at 23:31
  • 2
    Kripke models in particular are a special case of internal logic - specifically, the internal logic of the topos of presheaves on a poset. Complete Heyting algebras can be identified with the corresponding localic topos. For Heyting algebras in general, the connection to toposes is a bit more indirect, but we can still build an appropriate topos with the same semantics. – Mark Saving Jan 06 '24 at 00:52
  • To my knowledge toposes are coarser than linear logic, as the underlying structure of the subobject classifier is a heyting algebra. – cody Jan 07 '24 at 03:05

1 Answers1

3

From the comments, I think it is fair to treat this question as a reference request. One category that is well worth considering is the category of structures for the signature $(\bot, \top, \lnot, \land, \lor)$ of propositional logic in the sense of universal algebra. That Wiki page may not be very informative, but the book on Universal Algebra by Burris and Sankappanavar that it references is a a great introduction to the subject.

Rob Arthan
  • 48,577
  • Oh right, I didn't think of that. However this doesn't work with FOL, though then it just turns into model theory. Plus, one loses the data of each $\vDash$ semantics being some sort of unified collection. I'll think and wait a bit before marking this as the solution. – Fernando Chu Jan 05 '24 at 23:33
  • Complementing a bit: so different semantics, say HAs, are the usual universal algebra/model theoretic $\vDash$ but restricted to some set of structures. Hence, why completeness may fail. Conversely, if the set of structures has the classifying structure (the lindebaum algebra in this case), then it will be complete. Very obvious in retrospective. Thanks for pointing this out! – Fernando Chu Jan 05 '24 at 23:51