<p>Yes. There is for example beta + the rule {s = t | s and t are closed unsolvable terms}. This is as far as I remember not equal to beta-eta, and is consistent. See <a href="http://mathgate.info/cebrown/notes/barendregt.php#4" rel="noreferrer">mathgate</a> for a short description and reference to Barendregt.</p>

CC BY-SA 2.5
2010-08-19T10:03:05.363Z
This is, indeed, a correct answer to my question: beta-eta doesn't equate (\x.x x)(\x.x x x) and (\x.x x)(\x. x x), although they have the same Böhm tree.  I misphrased the question: I'm after observable differences.  I should probably accept this and ask the question I meant to ask...
Charles Stewart
CC BY-SA 2.5
2010-08-22T21:39:43.970Z
I've been thinking about this answer...  this theory isn't generated by new rules (unsolvability is undecidable), and I can't think of any confluent set of rules that generates a subtheory of this theory.  But for all I know, there may be one.  So, a new question: http://cstheory.stackexchange.com/questions/398/characterising-invisible-equivalences-by-confluent-rewrite-rules
Charles Stewart
CC BY-SA 2.5
2010-09-17T09:14:52.057Z
And my answer to that question shows that Evgenij's intuition was sound, and provides combinatory rewrite rules for a subtheory of this.  So accepted.
Charles Stewart
CC BY-SA 2.5
2010-08-18T15:11:04.317Z
2010-08-18T15:11:04.317Z
Evgenij Thorstensen
<p>The beta-eta-theory of the lambda-calculus is Post-complete.  Can additional rules be added to extend the beta-theory of the lambda-calculus to get confluent theories other than the beta-eta theory?</p>

<p><strong>Postscript</strong></p>

<p>This question violated my own rule that questions should explain why the questioner cares.</p>

<p>It struck me one night, not long before this site went into private beta, that because extensionality and the principle of the excluded middle are related, the eta rule is some sort of extensionality rule, and there are intermediate logics between intuitionistic and classical logic, then it would be interesting if there was such a thing as "intermediate eta" theories.</p>

<p>If I has done so, it would have been obvious that Evgenij's answer raises an obvious problem in the way I'd formulated the question, rather than being what I was after.</p>

<lambda-calculus>
Extensions of beta-theory of lambda calculus
Charles Stewart
# Extensions of beta-theory of lambda calculus

(Asked by: username_0 on 2010-08-18)

The beta-eta-theory of the lambda-calculus is Post-complete. Can additional rules be added to extend the beta-theory of the lambda-calculus to get confluent theories other than the beta-eta theory?

**Postscript**

This question violated my own rule that questions should explain why the questioner cares.

It struck me one night, not long before this site went into private beta, that because extensionality and the principle of the excluded middle are related, the eta rule is some sort of extensionality rule, and there are intermediate logics between intuitionistic and classical logic, then it would be interesting if there was such a thing as "intermediate eta" theories.

If I has done so, it would have been obvious that Evgenij's answer raises an obvious problem in the way I'd formulated the question, rather than being what I was after.

**Tags:** lambda-calculus


---

## 1 answers

### Answer by username_1 on 2010-08-18. Score: 8 | Accepted answer

Yes. There is for example beta + the rule {s = t | s and t are closed unsolvable terms}. This is as far as I remember not equal to beta-eta, and is consistent. See [mathgate](http://mathgate.info/cebrown/notes/barendregt.php#4) for a short description and reference to Barendregt.

> **Comments:**
> **username_0**: This is, indeed, a correct answer to my question: beta-eta doesn't equate (\x.x x)(\x.x x x) and (\x.x x)(\x. x x), although they have the same Böhm tree.  I misphrased the question: I'm after observable differences.  I should probably accept this and ask the question I meant to ask...  
> **username_0**: I've been thinking about this answer...  this theory isn't generated by new rules (unsolvability is undecidable), and I can't think of any confluent set of rules that generates a subtheory of this theory.  But for all I know, there may be one.  So, a new question: http://cstheory.stackexchange.com/questions/398/characterising-invisible-equivalences-by-confluent-rewrite-rules  
> **username_0**: And my answer to that question shows that Evgenij's intuition was sound, and provides combinatory rewrite rules for a subtheory of this.  So accepted.  

---

