Does this outwit Rosser's trick?

Question

Reading about Rosser's trick made me instantly curious about the following question: Can we devise a logic (which semantically encapsulates useful maths - define that as you will) in which for any theorem $T$, the shortest proof of $T$ is the same length as the shortest proof of the negation of $T$ EDIT: ...if that negation is provable in T?

A side reason why I'm interested in this is that philosophically I'm a big believer in Heraclites equality of opposites. A starting point of the above logic could be that the definition of the universe is the same as the definition of the empty set. This may seem counterintuitive but it's really quite beautiful because it means that any set is equivalent to its complement in the universe. The implication of this is that objects are not so much the contents of their boundaries, rather they are their boundaries. The boundary can be thought of as the unity of what is inside and outside and therefore all defined things are in identity with their definition. Seeing Rosser's trick earlier today appealed to this concept somewhat because in this universe, I think Rosser's trick would not be possible.

Does that check out in a formal way or is it just nonsense? Does it outwit the supposed theorem: "Any consistent, recursively axiomatized theory T in the language of arithmetic which extends Q is incomplete."?

Answer 1

I know nothing about the logic part, but you might be interested in Kolmogorov complexity theory. It is not related to logic, but has a very similar concept to what you describe.

If by a "theorem" you would mean any finite string $S$ of bits, and by a "proof", a program in an arbitrary but fixed "programming language" $L$ that produces it (the complexity is then the proof length), then the result $\tau(S)$ of an arbitrary algorithmic transformation $\tau$ has about the same complexity ($+O(1)$ that does not depend on $S$, only on $\tau$). Surprisingly, this impreciseness still allows to build a large theory that does not depend on the choice of $L$, and this "invariance" (asymptotical) under algorithmic transformations is one of its cornerstones.

You can convert a theorem $T$ (a string of symbols) to a bit string by rewriting it in $\LaTeX$ and encoding it in ASCII, and recover $T$ vice versa. Under this process, $T \mapsto \neg(T)$ clearly corresponds to an algorithmic transformation of bit strings.

Answer 2

You said:

Can we devise a logic in which for any theorem $$, the shortest proof of $T$ is the same length as the shortest proof of the negation of $$

Then you asked specifically:

Does it outwit the supposed theorem: "Any consistent … theory …”

The standard definition of “consistent” is that, there is no $T$ for which both $T$ and its negation are provable. Since you want both $T$ and its negation to be provable for all $T$, your theory is not consistent, and Rosser has nothing to say about it.

Inconsistent theories are generally disregarded because, except in very unusual contexts, they are practically useless. The reason we study logic and construct proofs is because we hope to gain some assurance that the theorems we prove are true. An inconsistent system provides easy proofs of all statements, both the true ones and the false ones. This is not of any conceivable use.

---

Consider this example. The engineering firm we work for has contracted to design a bridge. I determine that our bridge will collapse if its dead weight exceeds 14 million tonnes. I ask you to calculate the bridge's dead weight and compare it with 14,000,000 tonnes. This you do, and you come back to me saying:

I have proved that the bridge's weight does not exceed 14,000,000 tonnes.

I am pleased, but then you continue:

But I have also proved that the bridge's weight does exceed 14,000,000 tonnes, and moreover the two proofs are exactly the same length!

Do this enough and management will invite you to pursue the Heracleitan equality of opposites on your own time.