Leibniz's mathesis universalis, characteristica universalis and calculus ratiocinator are more than dreams or utopias. Nor is talk of formal philosophy mere metaphilosophical speculation and wishful thinking.
Zalta's Object Logic in its three degrees of unfolding (each subsuming the previous one) offers a non-trivial axiomatization and formal proofs of some interesting aspects of three great systems of ontology: Plato, Leibniz and Frege. Both the series of Object Logics and the series of these three ontologies can be given a Hegelian interpretation.
Furthermore this axiomatic metaphysics can be embedded and expressed in dependent-type theory. Here are some examples in Coq.
Plato:
https://github.com/owl77/CoqFormalisations/blob/main/zalta2.v
Leibniz:
https://github.com/owl77/CoqFormalisations/blob/main/zalta3.v
Frege (for now just an embedding of modal typed object logic)
https://github.com/owl77/CoqFormalisations/blob/main/zalta4.v
No comments:
Post a Comment