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 Id 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. Heres 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, theres a very obvious variant the extensional lambda calculus which adds an axiom: Ive already been through the basic meaning of lambda expressions in the Montague Grammar posts (soon to return, as Im 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 multi-step 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 aspect-dependent: their evaluation follows the same path no matter what is being evaluated, and I think its pretty clear that this referential transparency is a perfectly legitimate extension of extensionality as it applies to truth-functional propositional logic. Does extensionality imply decidability? Again, I would answer yes, although the reason I labeled this comment as a conjecture is that Im less sure of this point. People often think of first-order logic as extensional because it is not conceived of as modal, but the logical cognoscenti will tell you that even the ordinary first-order quantifiers cant really be viewed as truth-functional: 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 its 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 first-order logic are consequently not extensional). At this point Ill 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.  |