Formalising natural language statements is a minefield of difficulties, for (imo) essentially the same reasons that writing code which interacts with the real world is so difficult. Concepts you take for granted like identity, time, causality... all of that stuff needs to be fleshed out carefully and precisely in the formalism for facts to be relatable to each other (or even expressible in the first place).
Not to discourage you - it's a cool problem! OpenCog comes to mind as a project that tried to take this all the way, and there's a field devoted to this stuff in academia called KRR (knowledge representation and reasoning). The IJCAI journal is full of research on similar topics.
(also see all the different logics philosophers use to formalise different kinds of argument involving time/modality/probability - there are a lot, but they aren't very "modular" and can't easily be mixed unless someone has solved that since I last looked into it)
> Concepts you take for granted like identity, time, causality... all of that stuff needs to be fleshed out carefully and precisely in the formalism for facts to be relatable to each other (or even expressible in the first place).
Yes, and different formalisations of identity apply in different contexts.
Eg remember the famous line about not being able to step in the same river twice.
> logics philosophers use .. aren't very "modular" and can't easily be mixed
Not sure if the model-checking communities would agree with you there. For example CTL-star [0] mixes tree-logic and linear-temporal, then PCTL adds probability on top. Knowledge, belief, and strategy-logics are also mixed pretty freely in at least some model checkers. Using mixed combinations of different-flavored logic does seem to be going OK in practice, but I guess this works best when those diverse logics can all be reduced towards the same primitive data structures that you want to actually crunch (like binary decision diagrams, or whatever).
If no primitive/fast/generic structure can really be shared between logics, then you may be stuck with some irreconcilable continuous-vs-discrete or deterministic-vs-probabilistic disconnect, and then require multiple model-checkers for different pieces of one problem. So even if mixing different flavors of logics is already routine.. there's lots of improvements to hope for if practically everything can be directly represented in one place like lean. Just like mathematicians don't worry much about switching back and forth from geometry/algebra, less friction between representations would be great.
Speaking of CTL, shout out to Emerson[1], who won a Turing award. If he hadn't died recently, I think he'd be surprised to hear anyone suggest he was a philosopher instead of a computer scientist ;)
[0]: https://en.wikipedia.org/wiki/CTL* [1]: https://en.wikipedia.org/wiki/E._Allen_Emerson
Yeah, not suggesting philosophers are the only people using logics, but they've certainly been using them the longest!
Indeed, I've seen various attempts to tackle the problem including what you are suggesting - expressing the semantics of different logics in some base formalism like FOL in such a way that they can interplay with each other. In my experience the issue is that it's not always clear how two "sublogics" should interact, and in most cases people just pick some reasonable choice of semantics depending on the situation you are trying to model. So you end up with the same issue of having to construct a new logic for every novel situation you encounter, if that makes sense?
Logics for computing are a good example - generally you use them to formalise and prove properties of a program or spec, so they are heavily geared towards expressing stuff like liveness, consistency invariants and termination properties.
I haven't read about CTL though, thanks! I'll check it out. Hopefully I didn't write too much nonsense here =)
> Just like mathematicians don't worry much about switching back and forth from geometry/algebra [...]
As an ex-mathematician I think we worry a lot about transitioning between viewpoints like that. Some of the most interesting modern work on foundations is about finding the right language for unifying them - have a look at Schulze's work on condensed mathematics, for example, or basically all of Grothendieck's algebraic geometry work. It's super deep stuff.
> then you may be stuck with some irreconcilable continuous-vs-discrete or deterministic-vs-probabilistic disconnect
Agreed, I think this is one of the cruxes, and lately I'm starting to feel that maybe strict formal systems aren't the way to go for general-purpose modelling. Perhaps we need to take some inspiration from nature - completely non-deterministic, very messy, and nevertheless capable of reasoning about the universe around it!
> (also see all the different logics philosophers use to formalise different kinds of argument involving time/modality/probability - there are a lot, but they aren't very "modular" and can't easily be mixed unless someone has solved that since I last looked into it)
From a logic-as-types perspective, modalities turn out to be monads. So the problem of "mixing" modalities is quite similar to the problem of composing monads in programming languages.
Oh, wow, that's quite a cool connection. Will look into that, thanks!