Cut Elimination for Gödel Logic with an Operator Adding a Constant

Abstract

We consider an extension of propositional Gödel logic by an unary operator that enables the addition of a positive real to truth values. We provide a suitable calculus of relations and show completeness and cut elimination.

Partially supported by FWF grants P-26976-N25, I-1897-N25, I-2671-N35, and W1255-N23.

Appendix

Proof of Lemma 14. The end-segment of the proof will be of the form

where $C < \circ A$ and $\circ A < D$ are inferred, respectively, at the hypersequents $\mathcal {G}| C < \circ A$ and $\mathcal {F}| \circ A < D$. We proceed according to which inferences were used above $\mathcal {G}| C < \circ A$ and $\mathcal {F}| \circ A < D$.

• 1. If the inferences were respectively $\circ _1$ or $\circ _2$, so that the proof is

  

  then replace it with

  

• 2. If the inferences were both $\circ _2$, so that the proof is

  

  then replace it with

  

• 3. If the inference on the left-hand side is $\circ _1$ and the inference on the right-hand side is an internal weakening, the proof will be of the form

  

  Replace it with

  

• 4. If the inference on the left-hand side is $\circ _2$ and the inference on the right-hand side is an internal weakening, the proof will be of the form

  

  Replace it with

  

• 5. If the inference on the right-hand side is $\circ _2$ and the inference on the left-hand side is an internal weakening, the proof will be of the form

  

  Replace it with

  

• 6. The final case is that both inferences are internal weakenings:

  

  Replace it with

  

$\quad \square$