Are there deduction systems, which judge propositions by their proofs?
Micah Clark, a colleague of mine, wrote his PhD dissertation on the topic of automated mendacity, i.e., a “lying machine.” It was based on the psychological research that people tend to affirm certain argument structures that are not logically valid. He formalized an argument generator that would find logically valid and invalid arguments for propositions (which themselves may be true or false), and tested experimentally whether people affirmed them or not. Relevant papers to this work include:
- Clark, Micah H. "Mendacity and Deception: Uses and Abuses of Common Ground." 2011 AAAI Fall Symposium Series. 2011.
- Micah H. Clark. 2010. Cognitive Illusions and the Lying Machine: A Blueprint for Sophistic Mendacity. Ph.D. Dissertation. Rensselaer Polytechnic Institute, Troy, NY, USA. Advisor(s) Selmer Bringsjord. AAI3420907. (Note: that link is to a précis of the dissertation.)
Many of the references in those documents will be of interest as well.
Here is an example of inconsistentcy at work - inconsistent set theory:
It allows for a formalisation of naive set theory with the naive expectation that any predicate determines a set. That is, it's another solution to Russell's paradox apart from the theory of types or ZFC.
So it has a universal set, and Cantor's paradox is now a theorem.
This theory proves the axiom of choice, and disproves the continuum hypothesis. (The truth of these two axioms have been a major source of controversy since set theory was concieved).
It disarms both of Gödel's theorems that derailed Hilbert's programme, so that programme can be revived and completed.
Tarski showed that the truth-predicate is not definable in ZFC. In paraconsistent foundations an inconsistent truth-predicate is shown to be definable.
These seem like fairly remarkable achievements to me.