News for hackers. Stuff that matters.

A comment on Relation Between Type Theory, Category Theory and Logic. Parent comment

Re:Relation Between Type Theory, Category Theory and Logic by noreasonw on Saturday July 11, 2015 @07:06AM (#9869332)
Just reading your comment I was thinking about the closed world assumption in logic (prolog), perhaps there are some middle concept between the Proof by Contradiction and the closed world assumption. In the real world we learn concepts (think about relativity or a non planar world) and then the old question is no longer a two value alternative.

Perhaps something like: In this field a new conception could appear that would invalidate what we consider today to be only two alternatives. Is not about many worlds reality or quantum computation, (3 minutes thinking time out).

[ Parent | on HN ]
Re:Relation Between Type Theory, Category Theory and Logic by gallabytes on Saturday July 11, 2015 @01:29PM (#9870695)
We have something between the two in HoTT - universes of types is stratified by homotopy levels, corresponding to how many dimensions of structure a type has. A space with only points is thus a 0-type, a space with at most 1 point is a -1-type, and a space with only one is a -2-type.

The catch is that univalence is inconsistent with LEM at h-levels greater than -1, but assuming it is perfectly consistent for -1 types, which can be thought of as the "at most true" propositions of classical logic.

[ Parent | on HN ]
Re:Relation Between Type Theory, Category Theory and Logic by igravious on Saturday July 11, 2015 @08:30AM (#9869511)
This is out of my depth but the work of the physicists David Bohm and Basil Hiley (an article with him was recently linked to HN) seems to point in this direction? See, for instance, http://www.amazon.com/The-Undivided-Universe-Ontological-Int...

But like I say, out of my depth! :)

[ Parent | on HN ]