David A. Wheeler wrote: > But I don't see how to match proof tools to this problem at this time. > I'd be delighted to be proven wrong :-).
One way may be to develop a really huge set of propositions, which are "medically true" (maybe using a combination of modal logic, deontic logic, and many other logical systems at the same time). For example, (1) If the patient has a bacterial infection and the patient is not allergic to antibiotics then it should take antibiotics. Using (1) we cannot prescribe antibiotics as a treatment to a person who is infected by a virus and has no symptoms of bacterial infection. There are many people out there who do not know this and think that COVID-19 can be cure using penicillin. Using a proof assistant with a set of "medically true" propositions these people can not derive the fake statement: (2) If the patient has COVID-19 then the patient should take antibiotics. Of course, there are cases when COVID-19 and is accompanied by a bacterial infection, but this is not the same as (2). One of the goals of a proof assistant is to avoid writing stupidity and for many people, including myself, it is easy to write stupidity about medicine, because it is beyond our field of expertise. So, having a proof assistant with a really huge library of medically true statements may be the only way to guide us in the absence of a medical doctor as in the current situation (as a Millenial, I think that I am young enough to survive the COVID-19 if I get it in the near future, but it is important to think about the boomers out there). Another medically true proposition may be: (3) If the patient is secreting green fluid by his/her nose, then the patient has a bacterial infection. Using (1) and (3) the patient can deduce by himself/herself: (4) If the patient is secreting green fluid by his/her nose, then the patient should take antibiotics. I am not claiming that this approach is scalable. This is just brainstorming. Kind regards, José M. -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAA8xVUgr%3DfRxRiyfGN2PaUALfVK%2B_sTwnD4U3hU%3DAa4tEeWVZw%40mail.gmail.com.
