Prev: The Money Part [Civic Networking]
Next: But Yo, I'm making money, See ["Are Blogs Soviets?"]
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.
 | 
Pages: 1
Prev: The Money Part [Civic Networking]
Next: But Yo, I'm making money, See ["Are Blogs Soviets?"]