Formalizations that take big chunks of arguments as black boxes are not that useful. Formalizations that instead map all of an argument’s moving parts are very hard.
The reason that specialists learn formalizations for domain-specific arguments only is because formalizing truly general arguments[FN1] is an extremely difficult problem—difficult to design and difficult to use. This is why mathematicians work largely in natural language, even though their arguments could (usually or always) be described in formal logic. Specialized formal languages are possible and useful only because they describe radically stripped-down models of the world.
Overall, this means that—while moves like the example in the post probably are helpful—we shouldn’t expect to go much further in this direction.
[FN1]To be precise, formalizing truly general arguments in a way that simplifies and clarifies is hard. There is a trivial formalization for every argument, since the class of arguments is equinumerous with the natural numbers; the decision process can be a symbolic representation of a bunch of experts’ brains or something like that.
Formalizations that take big chunks of arguments as black boxes are not that useful. Formalizations that instead map all of an argument’s moving parts are very hard.
The reason that specialists learn formalizations for domain-specific arguments only is because formalizing truly general arguments[FN1] is an extremely difficult problem—difficult to design and difficult to use. This is why mathematicians work largely in natural language, even though their arguments could (usually or always) be described in formal logic. Specialized formal languages are possible and useful only because they describe radically stripped-down models of the world.
Overall, this means that—while moves like the example in the post probably are helpful—we shouldn’t expect to go much further in this direction.
[FN1]To be precise, formalizing truly general arguments in a way that simplifies and clarifies is hard. There is a trivial formalization for every argument, since the class of arguments is equinumerous with the natural numbers; the decision process can be a symbolic representation of a bunch of experts’ brains or something like that.