ReasonBase

Brief: Reasoned debate with formal semantics
Jump To: Parent Description
Code: GitHub

  • How many times has it been that arguments have hinged on tiny oversights? The process of reasoning, the dialectic is good, but armchair philosophy is an indulgence to argue unsoundly and socially, as a game. Even the excuse that it improves rhetoric skills is misleading, as it corrupts them more than it improves them.

    Anyone who is seriously interested in improving objective conditions, and therefore in understanding the truth, and therefore in conducting arguments by proof should be thrilled by the prospect of formalizing the semantics of everyday arguments, discussions and questions. This is after all the result of the greatest achievements in logic of the 20th century - the formalization, via the reduction to syntactic operations, of the proof and truth predicates. Furthermore, we now have the relative ability to implement such a system, by extending currently existing software systems. Accordingly, we can collectively engage in a large analytical effort proving or refuting certain key questions, with a complete and formally verified proof.

    We can eliminate an entire class of problems by reducing arguments to formally verifiable statements. In other words, there can be no more disputes because people simply agree to which ever axioms they want. What you take as axiomatic is, when the axioms are independent of reasonbase's theories, highly subjective, but certain axiomatizations cannot be held as they are provably inconsistent.

    reasonbase grows because people take pride in forming correct arguments about topics they are interested in. In fact, a "Socratic" measure should be created to reward the most intellectually capable of these individuals. Therefore, reasonbase can be expected to grow rapidly.

    An essential feature of reasonbase is the alignment of text to axioms - facilitating the rapid formalization of written subject matter. This benefits from the same tools as the Textbook Knowledge Formation project.

    Thankfully, the work has in large part been accomplished. There are numerous projects that when combined will produce the desired capabilities. The opencyc project has done exactly what we purport to do, they have assembled a team of knowledgeable philosophers, logicians, mathematics, programmers, and subject matter experts, and constructed exactly such a project. This will thus give us a strong foundation to get started on the process of completely formalizing existing arguments.

    Not only will people cease to argue about meaningless misunderstandings once we have a formal basis for argument, but the knowledge inherent in the system can then be applied towards automatically reasoning towards solutions in other cases, thus creating intelligent software as an automatic b y product.

    Interestingly, it also necessarily finds use in counter-rhetoric applications, to both identify carefully planted assumptions and methods and to utilize them to expedite the process of acquainting people with the truth and to help them satisfy their goals, in the sense mentioned in Aristotle s Rhetoric:

    Rhetoric is useful (1) because things that are true and things that are just have a natural tendency to prevail over their opposites, so that if the decisions of judges are not what they ought to be, the defeat must be due to the speakers themselves, and they must be blamed accordingly. Moreover, (2) before some audiences not even the possession of the exactest knowledge will make it easy for what we say to produce conviction. For argument based on knowledge implies instruction, and there are people whom one cannot instruct. Here, then, we must use, as our modes of persuasion and argument, notions possessed by everybody, as we observed in the Topics when dealing with the way to handle a popular audience. Further, (3) we must be able to employ persuasion, just as strict reasoning can be employed, on opposite sides of a question, not in order that we may in practice employ it in both ways (for we must not make people believe what is wrong), but in order that we may see clearly what the facts are, and that, if another man argues unfairly, we on our part may be able to confute him. No other of the arts draws opposite conclusions: dialectic and rhetoric alone do this. Both these arts draw opposite conclusions impartially. Nevertheless, the underlying facts do not lend themselves equally well to the contrary views. No; things that are true and things that are better are, by their nature, practically always easier to prove and easier to believe in. Again, (4) it is absurd to hold that a man ought to be ashamed of being unable to defend himself with his limbs, but not of being unable to defend himself with speech and reason, when the use of rational speech is more distinctive of a human being than the use of his limbs. And if it be objected that one who uses such power of speech unjustly might do great harm, that is a charge which may be made in common against all good things except virtue, and above all against the things that are most useful, as strength, health, wealth, generalship. A man can confer the greatest of benefits by a right use of these, and inflict the greatest of injuries by using them wrongly.

    It becomes easy to work on reasonbase. We will use CELT to bootstrap our natural language to logic translation service. We will then use vampire as our theorem prover.