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.
   • CommentAuthorDavid_Corfield
   • CommentTimeMar 1st 2013
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexIf, as Peirce showed us, predicate logic can represented by his Beta system of existential graphs, and if predicate logic is some kind of truncation of dependent type theory, should there not be a diagrammatic calculus for the latter too? Recall that the Beta graphs proved useful for representing [indexed monoidal categories](http://golem.ph.utexas.edu/category/2011/11/traces_in_indexed_monoidal_cat.html). When Peirce represents the negation of a proposition, $P$, by writing $P$ enclosed in a circle, are we seeing a representation of the type $[P, \emptyset]$, as though we're looking through $P$ to a symbol of absurdity? It looks like we'd want to take an intuitionistic version of Peirce, perhaps something like the one constructed by [Oostra](http://matematicas.uniandes.edu.co/eventos/SLALM2012/slides/arnold_oostra.pdf).

   If, as Peirce showed us, predicate logic can represented by his Beta system of existential graphs, and if predicate logic is some kind of truncation of dependent type theory, should there not be a diagrammatic calculus for the latter too? Recall that the Beta graphs proved useful for representing indexed monoidal categories.

   When Peirce represents the negation of a proposition, $P$, by writing $P$ enclosed in a circle, are we seeing a representation of the type $[P, \emptyset]$, as though we’re looking through $P$ to a symbol of absurdity? It looks like we’d want to take an intuitionistic version of Peirce, perhaps something like the one constructed by Oostra.

2. • CommentRowNumber2.
   • CommentAuthorTodd_Trimble
   • CommentTimeMar 1st 2013
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexThose are great questions, David. All I can say for the moment is that the "line of separation" was, for Peirce, a threshold so that passing into the circle was akin to entering a hypothetical world. There are glimmers of the same idea that one can use when dealing with lax natural transformations, where one passes through a semi-permeable membrane. Peirce's original laws for Beta have to be teased apart to get workable versions for intuitionistic logic. I've never considered such a calculus for dependent types (although I have, a bit, for higher-order logic). That would be an interesting project, I think.

   Those are great questions, David. All I can say for the moment is that the “line of separation” was, for Peirce, a threshold so that passing into the circle was akin to entering a hypothetical world. There are glimmers of the same idea that one can use when dealing with lax natural transformations, where one passes through a semi-permeable membrane.

   Peirce’s original laws for Beta have to be teased apart to get workable versions for intuitionistic logic. I’ve never considered such a calculus for dependent types (although I have, a bit, for higher-order logic). That would be an interesting project, I think.

3. • CommentRowNumber3.
   • CommentAuthorDavid_Corfield
   • CommentTimeMar 2nd 2013
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexOne step would be to think about how dependent product truncates into universal quantification and then implication. I wonder how one might handle the difference between term and type. Presumably there would need to be something as sophisticated as ways of representing, say, beta reduction from the lambda calculus. That points to things like [sharing graphs](http://repository.upenn.edu/cgi/viewcontent.cgi?article=1080&context=ircs_reports).

   One step would be to think about how dependent product truncates into universal quantification and then implication. I wonder how one might handle the difference between term and type. Presumably there would need to be something as sophisticated as ways of representing, say, beta reduction from the lambda calculus. That points to things like sharing graphs.