From: Big Red Jeff Rubard on 9 Aug 2010 15:41 Extensionality is Decidability Now for a purer conjecture I was going to include in the soviet post, but which enthused me enough that I thought Id save it. In my post The Triadic Form I spoke about those old standbys of analytic philosophy of language extensionality and intensionality. A statement where the truth of a statement depends directly on the truth of its components is extensional: a statement whose truth is dependent on the way its components are presented is said to be intensional. Alternative locutions for extensionality and intensionality are referential transparency and referential opacity. Having learned all this many moons ago, I was interested to see more recently that statements in pure functional languages, which have no side effects, are described as referentially transparent. Since pure functional languages are sugared versions of the lambda calculus, a perfectly general model of computation, this got me thinking that perhaps there was a connection between computability/decidability and extensionality. Heres what I can say right now. I think it is quite obviously true that decidability implies extensionality. Although the lambda calculus was not intended as an extensional model of function computation, theres a very obvious variant the extensional lambda calculus which adds an axiom: Ive already been through the basic meaning of lambda expressions in the Montague Grammar posts (soon to return, as Im working on my TeX skills); the wishbone symbol represents reducibility, the ability to compute the result on the right from the result on the left (the line underneath it indicates multistep reduction). Someone whose understanding derives primarily from programming languages may expect this somehow represents the absence of mutable storage, but really it says exactly the opposite: what the lambda extensionality axiom means is that no matter what you apply a function to, the function remains the same (there are no side effects from function application). So statements in the extensional lambda calculus are not aspectdependent: their evaluation follows the same path no matter what is being evaluated, and I think its pretty clear that this referential transparency is a perfectly legitimate extension of extensionality as it applies to truthfunctional propositional logic. Does extensionality imply decidability? Again, I would answer yes, although the reason I labeled this comment as a conjecture is that Im less sure of this point. People often think of firstorder logic as extensional because it is not conceived of as modal, but the logical cognoscenti will tell you that even the ordinary firstorder quantifiers cant really be viewed as truthfunctional: the truth of a quantified statement in a model is not purely syntactic, it depends on the contents of the universe of discourse being quantified over. But I think its an interesting commonplace of model theory that a technique for extensionalizing quantified sentences, quantifier elimination, in most cases automatically produces a decidability result for the theory amenable to that treatment. Quantifier elimination works by systematically converting quantified sentences in a theory to unquantified conjunctions or disjunctions: if quantifier elimination applies to a theory, a sentence involving nested quantifiers can have the quantifiers removed one by one, until only a singly existentially quantified statement applying to one of those conjunctions or disjunctions remains (which can be easily tested). If all and only theories that can go through quantifier elimination are decidable, there is a perfectly concrete sense in which extensionality implies decidability (and undecidable theories like full firstorder logic are consequently not extensional). At this point Ill make the observation that quantifier elimination casts statements and their negations in the form needed in the arithmetical hierarchy for recursive enumerability (no alternation of quantifiers), and when both the set of theorems and the set of nontheorems are recursively enumerable a logic is decidable, and that these theories are extensional in having a model in the extensional lambda calculus, and leave it at that.

Pages: 1 Prev: The Money Part [Civic Networking] Next: But Yo, I'm making money, See ["Are Blogs Soviets?"] 