Unfortunately, I’m talking about Dana Scott the logician — of Scott’s Trick fame — not the incredibly attractive lawyer from world-renowned TV show Suits.
Dana Scott is famous for many things, but, first of all, for “Scottery”, the breathtakingly beautiful theory of domains for denotational semantics, see e.g. https://en.wikipedia.org/wiki/Scott_continuity.
The informal idea is that a model is a sheaf over topological space X, the “possible worlds” are stalks growing from points x of X, and statement P is necessarily true about the world growing from a base point x if and only if there is an open set U containing x, such that for every point u from U, P is true about the world growing from u.
So the statement is necessarily true about a world if and only if this statement is true about all worlds sufficiently close to the world in question.
This kind of model is a nice mathematical “multiverse”, and one can try to ponder what the statement and the steps of the proof mean in that “multiverse”.
We’ll see if I can follow through and actually understand this proof :-)
I tend to find Kripke semantics easier fwiw. But if you’ve done a bunch of sheaf theory then this perspective also seems reasonable (though I will say it seems somewhat overkill to me, but what can I say, I’m no sheaf theorist).
Also I somewhat prefer to have the image of Dana Scott from Suits in mind when I think about Scott! It’s a lie I tell myself that makes me happy. But thanks for showing the man himself—a truly brilliant logician!
Yeah, I just have an entirely unreasonable love for continuity :-)
These days, of course, we are not surprised seeing maps from spaces of programs to continuous spaces (with all these Turing complete neural machines around us). But back then what Scott did was a revelation, the “semantic mapping” from lambda terms of lambda calculus to a topological space homeomorphic to the space of its own continuous transformations.
Dana Scott is famous for many things, but, first of all, for “Scottery”, the breathtakingly beautiful theory of domains for denotational semantics, see e.g. https://en.wikipedia.org/wiki/Scott_continuity.
:-) And he looked approximately like this when he created that theory: https://logic-forall.blogspot.com/2015/06/advice-on-constructive-modal-logic.html :-)
Now, speaking about what I should do to try to “grok” this proof...
And considering that I don’t usually go by “syntax” in formal logic, and that I tend to somewhat distrust purely syntax-based transformations...
For me, the way to try to understand this would be to try to understand what this means in terms of “topological sheaf-based semantics for modal logic” in the style of, let’s say, Steve Awodey and Kohei Kishida, https://www.andrew.cmu.edu/user/awodey/preprints/FoS4.phil.pdf 2007 paper (journal publication in 2008: https://www.cambridge.org/core/journals/review-of-symbolic-logic/article/abs/topology-and-modality-the-topological-interpretation-of-firstorder-modal-logic/03DE9E8150EE26B26D794B857FF44647).
The informal idea is that a model is a sheaf over topological space X, the “possible worlds” are stalks growing from points x of X, and statement P is necessarily true about the world growing from a base point x if and only if there is an open set U containing x, such that for every point u from U, P is true about the world growing from u.
So the statement is necessarily true about a world if and only if this statement is true about all worlds sufficiently close to the world in question.
This kind of model is a nice mathematical “multiverse”, and one can try to ponder what the statement and the steps of the proof mean in that “multiverse”.
We’ll see if I can follow through and actually understand this proof :-)
I tend to find Kripke semantics easier fwiw. But if you’ve done a bunch of sheaf theory then this perspective also seems reasonable (though I will say it seems somewhat overkill to me, but what can I say, I’m no sheaf theorist).
Also I somewhat prefer to have the image of Dana Scott from Suits in mind when I think about Scott! It’s a lie I tell myself that makes me happy. But thanks for showing the man himself—a truly brilliant logician!
Yeah, I just have an entirely unreasonable love for continuity :-)
These days, of course, we are not surprised seeing maps from spaces of programs to continuous spaces (with all these Turing complete neural machines around us). But back then what Scott did was a revelation, the “semantic mapping” from lambda terms of lambda calculus to a topological space homeomorphic to the space of its own continuous transformations.