Lambda Calc, Peano Axioms, & Recreating Maths

bluebaritone21 · January 12, 2024, 3:21pm

Okay. Thanks! I'll think about that...

bluebaritone21 · January 17, 2024, 7:45pm

Like this?

bh · January 17, 2024, 9:40pm

I guess... does it work?

My solution is a little simpler; I think my hint misled you.

bluebaritone21 · January 17, 2024, 9:49pm

Oh! Mine just reported nothing. That makes so much more sense!

bluebaritone21 · January 17, 2024, 9:57pm

On to zero?!

bluebaritone21 · April 8, 2024, 6:09pm

I'm not sure if this is necroposting, but I'm working on a new λ-Calculus Program, and I want to implement ZERO?. Could someone give me tips?

Here's the project:

bh · April 8, 2024, 7:01pm

0: λf . λx . x
1: λf . λx . f x
2: λf . λx . f f x
3: λf . λx . f f f x

What's special about zero?

bluebaritone21 · April 8, 2024, 7:02pm

It's the identity function, and the only one that doesn't call $$f$$. Ooh, Let's see if I can make it...

I'm not sure that the problem is:

It works fine with 0 replaced with (SUCCESSOR 0).