Vladimir_Nesov comments on Second-Order Logic: The Controversy - LessWrong
You are viewing a comment permalink. View the original post to see all comments and the full post content.
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (188)
Feeling our way into a new formal system is part of our (messy, informal) pebblecraft. Sometimes people propose formal systems starting with their intended semantics (roughly, model theory). Sometimes people propose formal systems starting with introduction and elimination rules (roughly, proof theory). If the latter, people sometimes look for a semantics to go along with the syntax (and vice versa, of course).
For example, lambda calculus started with rules for performing beta reduction. In talking about lambda calculus, people refer to it as "functions from functions to functions". Mathematicians knew that there was no nontrivial set S with a bijection to the set of all functions from S to S. So something else must be going on. Dana Scott invented domain theory partially to solve this problem. Domains have additional structure, such that some domains D do have bijections with the set of all structure-preserving maps from D to D. http://en.wikipedia.org/wiki/Domain_theory Similarly, modal logics started with just proof theory, and then Saul Kripke invented a semantics for them. http://en.wikipedia.org/wiki/Kripke_semantics
There's always a syntactical model which you can construct mechanically from the proof theory (at least, that's my understanding of the downward Lowenheim-Skolem argument) - but Scott and Kripke were not satisfied with that syntactical model, and went looking for something else, more insightful and perspicuous. Adding a "semantic" understanding can increase our (informal) confidence in a formal system - even a formal system that we were already working with. I'm not sure why it helps, but I think it's part of our pebblecraft that it does help.
Perhaps adding a "semantic" understanding is like another bridge between informal and formal reasoning. These bridges are only partly formal - they're also partly informal, the concepts and gesturing around the equations and proofs. Having one bridge is sufficient to go onto the Island of Formality, do some stuff, and come off again, but might be more convenient to have two, or three.
Nice. This seems like a surprisingly well-motivated way of reducing everything to physics: there's just "syntactic" machinery made out of physics, and any semantics that might be attributed to parts of this machinery is merely a partially informal device (i.e. a collection of cognitive skills) that human mathematicians might use as an aid for reasoning about the machinery. Even when the machinery itself might in some sense be said to be semantically reasoning about something or other, this description of the machinery can be traced back to human mathematicians who use it as a partially informal device for understanding the machinery, and so it won't strictly speaking be a property of the machinery itself.
In other words, in this view semantics is an informal art primarily concerned with advancement of human understanding, and it's not fundamental to the operation of intelligence in general, it's not needed for properly designing things, responding to observations or making decisions, any more than curiosity or visual thinking.