Logic without truth

Pi is wrong! But so what? It is neither new, nor complicated enough to count as real math! And suggestions that 2\pi i or \pi/2 might be even better show that it not clear-cut either.

I recently invested sufficient energy into some logical questions to make real progress. But while telling friends and fellow logicians about it, I realized how irrelevant all my results and conclusions will be. I will have to publish them in an appropriate journal nevertheless, since they continue David Ellerman’s work on partition logic. Not publishing them would be dismissive towards the value of David Ellerman’s work, and he really invested lots of effort into it, and believes in its value. I won’t talk about those results here, since I don’t know how it would impact my ability to publish them.

Let’s have some fun instead, stay extremely close to classical logic, and still demonstrate a logic without truth. And let’s get back to Gerhard Gentzen.

Partial truths

I am fond of partial functions. For a partial function p:X\to Y, we have

  • p^{-1}(A\cap B)=p^{-1}(A)\cap p^{-1}(B)
  • p^{-1}(A\cup B)=p^{-1}(A)\cup p^{-1}(B)
  • p^{-1}(A {}\setminus{} B)=p^{-1}(A) {}\setminus{} p^{-1}(B)
  • p^{-1}(A \Delta B)=p^{-1}(A) \Delta p^{-1}(B) where A \Delta B := (A {}\setminus{} B) \cup (B {}\setminus{} A)

But p^{-1}(Y)=X is only true if p is a total function. Especially p^{-1}(A^c)=p^{-1}(A)^c is only true (even for specific A) if p is total, since otherwise
p^{-1}(Y)=p^{-1}(A\cup A^c)=p^{-1}(A)\cup p^{-1}(A^c) \quad = \quad p^{-1}(A)\cup p^{-1}(A)^c=X
Let’s also prove one of the other claims:
x {}\in{} p^{-1}(A {}\setminus{} B)  \Leftrightarrow p(x) {}\in{} A {}\setminus{} B \Leftrightarrow p(x) {}\in{} A \land  p(x) {}\notin{} B \Leftrightarrow x {}\in{} p^{-1}(A) {}\setminus{} p^{-1}(B)

Note that A {}\setminus{} B = A \triangle (A \cap B). So the preserved operations are “and”, “or”, and “xor” if interpreted from a logical perspective. It would be nice if implication were preserved too. This seems hopeless, since A \to A is always true, and truth is not preserved. But we do have A \subseteq B \Rightarrow p^{-1}(A) \subseteq p^{-1}(B), which means that the external implication given by the order is preserved. So we should be able to turn this into a logic, where internal truth is not preserved under context morphisms.

Gerhard Gentzen’s sequent calculus

The sequent calculus is a proof calculus with significant practical and theoretical advantages compared to more obvious proof calculus systems. It works with sequents A_{1},\ldots,A_{r}\vdash B_{1},\ldots,B_{s}. The propositions A_i (and B_j) could be logical formulas like S(x)=S(y) \to x = y (the 4-th Peano axiom). They can also be interpreted as subsets of some universe set X, which is sufficient for understanding the basics of the sequent calculus. Then the sequent itself is interpreted as [A_{1}]\cap\ldots\cap [A_{r}]\ \subseteq\ [B_{1}]\cup\ldots\cup [B_{s}].

Left structural rules Right structural rules
\begin{array}{c} \Gamma\vdash\Delta\\ \hline \Gamma,A\vdash\Delta \end{array}(WL) \begin{array}{c} \Gamma\vdash\Delta\\ \hline \Gamma\vdash A,\Delta \end{array}(WR)
\begin{array}{c} \Gamma,A,A\vdash\Delta\\ \hline \Gamma,A\vdash\Delta \end{array}(CL) \begin{array}{c} \Gamma\vdash A,A,\Delta\\ \hline \Gamma\vdash A,\Delta \end{array}(CR)
\begin{array}{c} \Gamma_{1},A,B,\Gamma_{2}\vdash\Delta\\ \hline \Gamma_{1},B,A,\Gamma_{2}\vdash\Delta \end{array}(PL) \begin{array}{c} \Gamma\vdash\Delta_{1},A,B,\Delta_{2}\\ \hline \Gamma\vdash\Delta_{1},B,A,\Delta_{2} \end{array}(PR)

Here \Gamma,\Delta, ... stand for arbitrary finite sequences of propositions. The structural rules may be relatively boring. The following global rules are slightly more interesting

Axiom Cut
\begin{array}{c} \ \\ \hline A\vdash A \end{array}(I) \begin{array}{c} \Gamma\vdash\Delta,A\quad A,\Sigma\vdash\Pi\\ \hline \Gamma,\Sigma\vdash\Delta,\Pi \end{array}(Cut)

None of the rules up to now has used any logical constant or connective. They can be verified directly for the subset interpretation. The following logical rules can only be verified after the (intended) interpretation of the logical connectives has been fixed.

Left logical rules Right logical rules
\begin{array}{c} \Gamma,A,B\vdash\Delta\\ \hline \Gamma,A\land B\vdash\Delta \end{array}(\land L) \begin{array}{c} \Gamma\vdash A,B,\Delta\\ \hline \Gamma\vdash A\lor B,\Delta \end{array}(\lor R)
\begin{array}{c} \ \\ \hline \bot\vdash\Delta \end{array}(\bot L) \begin{array}{c} \ \\ \hline \Gamma\vdash\top \end{array}(\top R)
\begin{array}{c} \Gamma,A\vdash\Delta\quad\Sigma,B\vdash\Pi\\ \hline \Gamma,\Sigma,A\lor B\vdash\Delta,\Pi \end{array}(\lor L) \begin{array}{c} \Gamma\vdash A,\Delta\quad \Sigma\vdash B,\Pi\\ \hline \Gamma,\Sigma\vdash A\land B,\Delta,\Pi \end{array}(\land R)
\begin{array}{c} \Gamma\vdash A,\Delta\quad\Sigma,B\vdash\Pi\\ \hline \Gamma,\Sigma,A\to B\vdash\Delta,\Pi \end{array}(\to L) \begin{array}{c} \Gamma,A\vdash B,\Delta\\ \hline \Gamma\vdash A\to B,\Delta \end{array}(\to R)

One possible interpretation for these connectives in terms of subsets would be [\bot]:=\emptyset, [\top]:=X, [A\land B]:=[A]\cap [B], [A\lor B]:=[A]\cup [B], and [A\to B]:=[A]^c\cup [B].

But it may be more instructive to see an interpretation where one of the classical logical rules is violated. So let us use [A\to B]:=\mathrm{int}([A]^c\cup [B]) instead, where \mathrm{int} is the interior operator of some topological space. The propositions A_i (and B_j) are interpreted as open subsets in this case. The rule \begin{array}{c} \Gamma,A\vdash B,\Delta\\ \hline \Gamma\vdash A\to B,\Delta \end{array}(\to R) is violated now, and has to be replaced by the rule \begin{array}{c} \Gamma,A\vdash B\\ \hline \Gamma\vdash A\to B \end{array}(\to R_J). This gives us the intuitionistic sequent calculus, which exactly characterizes the valid conclusions of intuitionistic logic.

To see that (\to R) is violated, let \Gamma=\top, A correspond to [A]=(0,\infty), B=\bot, and \Delta = A. Above the line we have \mathbb R \cap (0,\infty) \subseteq \emptyset \cup (0,\infty), which is true. Below the line we have \mathbb R \subseteq \mathrm{int}((-\infty,0])\cup (0,\infty), which is false.

An evil twin of sequent calculus

Note that implication satisfies C\land A \vdash B \Leftrightarrow C \vdash (A\to B) or rather [C]\cap [A] \subseteq [B] \Leftrightarrow [C] \subseteq [A\to B]. Let us replace implication by minus. Note that minus satisfies [A] \subseteq [B]\cup [C] \Leftrightarrow [A-B] \subseteq [C] with [A-B]:=[A]{}\setminus{}[B]. Then we get the following two rules instead of (\to L) and (\to R).

\begin{array}{c} \Gamma,A\vdash B,\Delta\\ \hline \Gamma,A- B\vdash \Delta \end{array}(- L) \begin{array}{c} \Gamma\vdash A,\Delta\quad\Sigma,B\vdash \Pi\\ \hline \Gamma,\Sigma\vdash A-B,\Delta,\Pi \end{array}(- R)

Of course, we also remove \to and \top from the language together with the rule (\top R). This sequent calculus is still as sound and complete as the original sequent calculus. But we no longer reason about implication, but only about minus. Some sort of implication is still present in \vdash, but it is no longer mirrored internal in the language of the logic itself. So this is our logic without truth.

I don’t really know (or understand) whether this sort of context morphism has any sort of relevance, and whether that logic without truth occurs anywhere in the real world. Is there any relation to the fact that it is easier to deny the relevance or truth of a given conclusion than to prove that it is important and true? What I like about that logic is the asymmetry between implication and falsehood, because I wanted to find naturally occurring asymmetries in mathematical hierarchies and logic. Even for the results that I do want to publish, I have the same problem that I don’t really understand the relevance of the corresponding context morphisms, whether there even should be context morphisms, and whether my proposed context morphisms are the correct ones.

Conclusions?

That post initially also contained a logic without falsehood, or rather a logic where falsehood is not used. But it started to get long, and this post is already long enough. Not sure whether this was really a good idea, since the explanation of the sequence calculus was also intended to better understand how such a logic with a reduced set of logical constants and connectives still maintains its main features. Maybe I will manage to create another blog post from the removed material. Or maybe nobody including myself cares anyway, as already indicated at the beginning. Or maybe I should better use my time to finish the paper about the results I wrote about at the beginning, and submit them to…

Advertisements

About gentzen

Logic, Logic, and Logic
This entry was posted in logic, partial functions and tagged , . Bookmark the permalink.

6 Responses to Logic without truth

  1. gentzen says:

    I did a German translation of this post. I didn’t spend too much time on it, but it was a humbling experience. While trying to translate what I wrote, I had to realize that my English writing style is not great. I make too long sentences, which I have to be split into multiple sentences in German. Sometimes I had to fill in more information to form valid German sentences. I started to doubt whether my original sentences were really valid English sentences.

  2. vznvzn says:

    thx for tip on Ellerman work. reminds me, have long suspected there is a local hidden variable variable theory of QM that can be derived from the bell experiment, which is based on the assumptions of “unfair sampling” ie hidden variables control detection probabilities. suspect it may be derived somewhere, but think there is some elegant derivation/ theory waiting to be uncovered here, and it might take nearly a mathematician to do so. involving differential equations possibly… for physicists its a kind of “blind spot”…

    • gentzen says:

      The question is a bit why one wants to have a local hidden variable theory. There might be a sloppily formulated “no free lunch” theorem, which somehow derives too strong conclusions from too few assumptions. If Bohmian mechanics is just considered as a counterexample to von Neumann’s theorem, then it is just perfect.

      I know you have written …, and it has been cited from time to time. I don’t think it is wrong, but I do think that Bell’s theorem is not sloppy. By this I mean that it is not a cheap mathematical trick, but an honest attempt to explain and expose the differences between expectation values arising from quantum mechanics and expectation values arising from typical local hidden parameters.

      The “blind spot” for me is rather the laziness not trying to explain why Bohmian mechanics (and Everett’s original formulation of the many-worlds interpretation) are not great physical interpretations. And by laziness I mean that such explanations should stay concrete and point out specific shortcomings of these interpretations, and not just sweeping claims that no ontological interpretations are possible, or that talking about interpretations at all would be a waste of time and physically meaningless.

      • vznvzn says:

        bells thm is far from sloppy, quite to the contrary its a masterful work of art, its a physicist thinking almost like a mathematician, but think there is a very subtle assumption bordering on hairline flaw that afaik hasnt been totally isolated yet, and think focusing on it can lead to a new theory. it has to do with the fair sampling assumption. note bell himself revised his proof to attempt to deal with that “loophole”.

  3. Pingback: Logic without negation and falsehood | Gentzen translated

  4. Pingback: A subset interpretation (with context morphisms) of the sequent calculus for predicate logic | Gentzen translated

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s