Everything Is Just Functions: 1 week with David Beazley and SICP

I recently came across the notion that you need inductive data types (and can't just use Church encodings) if you want to do theorem proving, like proving that `0 != 1`.

I threw up some content up here: https://intellec7.notion.site/Drinking-SICP-hatorade-and-why... , along with an unrelated criticism of SICP.

I'd like to better understand what the limitations are of "everything is just a function".

I think you could prove 0 ≠ 1 if you had some other concrete fact about inequality to make use of. You could reason from the theorem "f = g -> f x = g x" to create your inequality fact on the right side and then take the contrapositive.

It seems correct to me that you can't directly prove inequality between Church numerals without starting with some other fact about inequality. Whereas with inductive data types, a proof system can directly "observe" the equality or inequality of two concrete instances of the same inductive type, by recursively removing the outermost constructor application from each instance.

fixed link: https://goosetaco.notion.site/Drinking-SICP-hatorade-and-why...

Well for theorem proving you need Sigma and Pi types plus some notion of equality. Can you achieve those with Scott or Church encoding?

Looking at the linked references, I'm not sure what else is being assumed to be available or not available when considering proofs using the Church numerals. I guess that will matter a lot, and I don't know enough to make more general statements about what is or isn't sufficient here.