This is a powerful technique that can prove consistency, conservativity (that a statement about a small system
which is a theorem in a more expressive one was already a theorem of the smaller one) etc. Applied to programming languages, it can show that if the result of a program in its denotational semantics is a number (as opposed to undefined) then when you run the program it is guaranteed to terminate (maybe after the Sun has gone supernova) and return that number.
It works by tying the syntax and the semantics together in lock-step, so that (maybe easy) observations about the semantic structure have direct consequences for the existence of a proof.
See
Section 7.7 in my book "Practical Foundations of Mathematics" for one categorical treatment, although there is a vast literature in theoretical computer science about this.
Of course, the construction uses structural recursion over the syntax. Amongst its consequences are consistency results. For anyone aware of Godel's incompleteness theorem, this should set some alarm bells ringing.
The solution is that the semantic structure (often a Grothendieck topos) is logically much stronger than the syntactic one. If, for example, the latter is the logic of an elementary topos then the former must enjoy (some fragment of) the axiom-scheme of replacement.
PS The actual categorical construction is extremely simple. The "lock-step" property has to be proved as a theorem for each type constructor (eg function-spaces)
and is valid in many cases, although not higher order logic.
No comments:
Post a Comment