It should then be possible to get a marked-up version of any document with highlighting for “proven” claims.
Sure, it’s not perfect, but I think it would be an interesting way to apply the rigor that used to be the job of publications.
It should then be possible to get a marked-up version of any document with highlighting for “proven” claims.
Sure, it’s not perfect, but I think it would be an interesting way to apply the rigor that used to be the job of publications.
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)
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.
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
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!
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.
I think you'd be better served by a tool for calculating chains of Bayesian reasoning. I've seen a tool that does this for numerical estimations.
[0] https://en.m.wikipedia.org/wiki/Gottlob_Frege#Political_view...
I found I got much better at writing non-fiction after having math at uni. I would help proof-read essays and other hand-ins by my SO and sister, and apply similar rigor as you mention. Stuff like "you show C follows from B here, but you haven't actually given an argument for why B follows A, so you can't then claim C follows from A".
It's tempting to say that with LLMs this seems like a plausible task to turn it into a program, but the hallucination issue puts a damper on that scheme.
Alas, things like this aren't logic proofs.
It bothers me to my core when I see this idea. Sometimes at FAANG. Blissfully management learned to...not promote...them.
I work with RAG pipelines all day, and the idea that hallucination isn't an ongoing major issue doesn't match my experience _at all_. Possibly a skill issue on my part, but, also on the part of everyone I ever talk to in the same space too.
If you're sneaky about it it will read like a logical conclusion when in fact X and Y are only loosely related contextually, and there is no logical chain at all.
A standard political trick is to blame X on something emotive and irrelevant, and offer Y as a false solution which distracts from the real causes of the problem.
This is used so often it's become a core driver of policy across multiple domains.
Although it's very effective, it's a crude way to use this. There are more subtle ways - like using X to insinuate criticism of a target when Y is already self-evident.
Point being, a lot of persuasive non-fiction, especially in politics, law, religion, and marketing, uses tricks like these. And many others.
They work because they work in the domain of narrative logic - persuading through stories and parables with embedded emotional triggers and credible-sounding but fake explanations, where the bar of "That sounds plausible" is very low.
LLMs already know some of this. You can ask ChatGPT to make any text more persuasive, and it will give you some ideas. You can also ask it to read a text, pull out the rhetorical tricks, and find the logical flaws.
It won't do as good a job as someone who uses rhetoric for a living. But it will do a far better job than the average reader, who is completely unaware of rhetoric.
An example tree for the statement "God exists": https://www.kialo.com/god-exists-3491?path=3491.0~3491.1
To do that you first need a definition of the concept God.
And then you realize that all the people making arguments in the past were using their own unspoken and incompatible definitions.
(Although I wouldn't be surprised if somebody had already recreated something like Prolog in Lean with a tactic that does more or less what the Prolog interpreter does)
E.g. lets say the statement is about a presidents promise to end a conflict within 24 hours after coming into office. One could get to a conclusion pretty quickly when the conflict hasn't been ended after 24 hours when they entered the office.
But what does "end the conflict" mean exactly? If the conflict ended how long does it need to remain ended to achieve the label "ended"? What if said president has a history that recontextualizes the meaning of that seemingly simple claim because he is known to define the word "ended" a little different than the rest of us, do you now judge by his or by our definition? What if the conflict is ended but there is a small nest of conflict remaining, after which size do we consider the conflict going on?
I know some of that has official definitions, but not everything has. In the end a lot of that will require interpretation and which definition to chose. But yeah I support your idea, just spelling it out and having a machine-readable chain of thought might help already.
https://www.microsoft.com/en-us/research/blog/claimify-extra...
Basically crowd-sourced statements, rebuttals, agreements, etc, in a nice interface.
We need that nowadays.
A simple scenario would be reading a news article about american politics. You see an unusual claim made, so you start tracing it and find that the journalist got it from person X who got it from person Y who got it from donald trump. Trump is famous for lying constantly, so unless there's a second source making the claim, you could disregard it with a high probability.
But you might find a historical/journalistic/investigative angle more profitable.
I heard a software product pitch from a small law practice who were outside investigators for abuse/policy-violation claims in a unionized workforce. They had a solid procedure: start with the main event. Interview all witnesses, and identify other interesting events. Then cross-reference all witnesses against all alleged/interesting events. That gives you a full matrix to identify who is a reliable witness, what sort of motivations are in play, and what stories are being told, patterns of behaviour, etc. Their final report might actually focus on another event entirely that had better evidence around it.
In that sort of historical investigation, a single obviously false claim undermines all claims from that witness. Pure logic doesn't have that bi-directionality of inference. Sometimes your sources just flat out lie! That's half the work.
The key difference is between a full matrix of claims vs sources/evidence, while good math is all about carefully plotting a sparse inference graph that traverses the space. What is called "penetrating minimalism" in math is called "cherry picking" in history or journalism.
We passed on the pitch. Didn't see how it scaled to a product worth building, but their process was appealing. Much better than the an internal popularity-contest or witch-hunt. Probably better than the average police investigation too.
Completely impossible but still interesting and fun to explore.
But you don't need the power of Lean to do something like this. I would recommend starting with something like Prolog or RDF triples