News for hackers. Stuff that matters.
Re:Roger Penrose – Is Mathematics Invented or Discovered? [v... by mikorym on Saturday April 18, 2020 @01:48PM (#22909537)
You can always generate substructures with closure properties. The subobject structure comes from all the subobjects—so it is the default logic of the topos. Of course you can do the same thing here as you mentioned since it is a Heyting algebra at the least.

My point is something else: I don't know of a way to have a intuitionistic exterior logic and a classical internal logic.

There are no comments on this comment yet.