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.