I was excited by the initial direction of the article, but somewhat disappointed with how it unfolded.
In terms of Leibniz’s hope for a universal formal language we may be closer to that. The new book Modal Homotopy Type Theory (2020 by David Corfield) argues that much of the disappointment with formal languages among philosophers and linguists stems from the fact that through the 20th century most attempts to formalize natural language did so with first-order predicate logic or other logics that lacked dependent types. Yet, dependent types are natural in both mathematical discourse and ordinary language.
Martin-Lof developed the theory of dependent types in the 1970s and now Homotopy Type Theory has been developed on top of that to serve as a computation-friendly foundation for mathematics. Corfield argues that such type theories offer new hope for the possibility of formalizing the semantic structure of natural language.
Of course, this hasn’t been accomplished yet, but it’s exciting to think that Leibniz’s dream may be realized in our century.
I was excited by the initial direction of the article, but somewhat disappointed with how it unfolded.
In terms of Leibniz’s hope for a universal formal language we may be closer to that. The new book Modal Homotopy Type Theory (2020 by David Corfield) argues that much of the disappointment with formal languages among philosophers and linguists stems from the fact that through the 20th century most attempts to formalize natural language did so with first-order predicate logic or other logics that lacked dependent types. Yet, dependent types are natural in both mathematical discourse and ordinary language.
Martin-Lof developed the theory of dependent types in the 1970s and now Homotopy Type Theory has been developed on top of that to serve as a computation-friendly foundation for mathematics. Corfield argues that such type theories offer new hope for the possibility of formalizing the semantic structure of natural language.
Of course, this hasn’t been accomplished yet, but it’s exciting to think that Leibniz’s dream may be realized in our century.