Lambda calculus (created in the 1930s by Church) allows identity to be assigned arbitrarily and changed at any time. When we make ontologies / taxinomies that’s also what we do. Naming categories, assigning symbols, it’s all the same act of stating (or asserting equivalence). To prove it? It’s asserted. I think of a first-order prover like so: Similar to creating a maze with each turn a transformation within the logical statement and asking only one question: Can I get back to the entrance from the entrance? If you can it’s proven.

Lambda calculus (created in the 1930s by Church) allows identity to be assigned arbitrarily and changed at any time.
 
When we make ontologies / taxinomies that’s also what we do.
 
Naming categories, assigning symbols, it’s all the same act of stating (or asserting equivalence).
 
To prove it? It’s asserted. I think of a first-order prover like so:
 
Similar to creating a maze with each turn a transformation within the logical statement and asking only one question:
 
Can I get back to the entrance from the entrance?
 
If you can it’s proven.
——–

Leave a comment

Your email address will not be published. Required fields are marked *


1 × nine =

Leave a Reply