Are there deduction systems, which judge propositions by their proofs?

I always found consistency to be highly overrated, even long before I knew of things like paraconsistent logic and the principle of explosion. The formalisms I've encountered so far are still different from my ideas however, and so I want to ask if anyone knows if something like it has been studied, or maybe if there is a flaw. The questions are down below.

My thinking went like this:

A main motivation for the development of logic and its formalization was the wish to be able to devise convincing arguments, because if you're skilled in logic, which often involves drawing conclusions by truth value preserving deduction steps, you might have an advantage in a discussion. But I figure in reality

• All real discussions have finite length (people want to sleep, have to work, are frustrated from the discussion, die of age etc.).
• Like in academia, to “win an argument” essentially means to convince the others that you're right (in fact, we could probably make the definition even weaker).

Moreover, in such a discussion, the principles of argumentation (the derivation rules, the formal proof system, if you will) are essentially never fixed beforehand. And the question whether or not the principles of argumentation are consistent is probably even more difficult to show than any issue of interest itself. Now let's consider a speaker whose main motivation it is to win an argument. My point is this:

• In general, a proof of a statement is structurally different from a potential proof of its negation.
• How simple it is to take a statement and show it implies absurdum depends on the statement.

Now if you can show a statement but it's very difficult to show the opposite or not at all obvious how it leads to a contradiction, then you might have already won the argument! In practice, for the speaker, it might not even matter if he believes in the statement itself. Or whether or not it even has a truth value. Given how we can often distinguish syntactic and semantic notions, I figure someone must have though about how to lie with mathematical efficiency.

Given the motivation above, I think it's natural to study argumentation rules, whether they are consistent or not. For example, consider a thing you want to discuss (given in the object language), choose your favorite proof system (possibly inconsistent), proof a statement and/or its negation and (formally this might mean we deal with a two-level proof system), choose the statement whose proof was shorter. Given the finite time, there is no reason for the cunning speaker to use an argument of which he knows the opposition will not find a counter argument. And taking the length of the proofs into account is only one option. You can consider a proof system (possibly inconsistent) and only allow proofs in which every $\beta$-reduced expression appears only once. You might such meta rules which drop proofs for negation of statement you don't like.

Given fixed premises, can there be significant differences between the complexity classes of proofs of a statement and its negation? Are there consideration of how the complexity of taking a statement to absurdum depend on the statement. And is this essentially the same for different deduction rules?

Are there considerations of (possibly inconsistent) derivation rules together with meta rules, which make quantitative statements about the associated proofs of a statement and its negation? E.g., like my idea above: take an inconsistent deduction system, but augment it with higher rules which assign values to the propositions via reasoning about their proofs.

I've seen deduction systems where you get any statement from absurdum in one step. But of course you need absurdum in the first place. There is the informal sentence “If ZFC, the common axiomatization of set theory, is inconsistent, then you can proof anything from it.”

To what extend is the above literally true? Must a proof of the inconsistency of a theory like ZFC necessarily provide you with, e.g., a proof for a statement and its negation, so that you can actually show anything? Or does showing inconsistency of this system only show that there is such a proof.

• Btw. the idea of watching out which propositions are used how often reminds me of linear logic. – Nikolaj-K Jun 30 '13 at 20:02
• What does one do if the proof of a statement and it's negation are the same legnth? – Baby Dragon Jul 11 '13 at 21:50

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:

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.

1. So it has a universal set, and Cantor's paradox is now a theorem.

2. 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).

3. It disarms both of Gödel's theorems that derailed Hilbert's programme, so that programme can be revived and completed.

4. 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.