Jeff Rubard
2010-02-06 03:58:17 UTC
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
note 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:
λx.tx≥t
I’ve already been through the basic meaning of lambda expressions; 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.
JDR *camera mundi*
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
note 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:
λx.tx≥t
I’ve already been through the basic meaning of lambda expressions; 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.
JDR *camera mundi*