nLab Sandbox2

---

This can be illustrated using string diagrams, as follows. The companion and conjoint of $f$ are the horizontal arrows

equipped with 2-cells

---

Spider lemma (corrected)

---

metric	Minkowski	Schwartzschild	Kerr
$g_{tt}$	-1	$-1 + 2 \frac{m}{r}$	$-1 + 2 \frac{mr}{\rho^2}$
$g_{rr}$	+1	$\frac{r}{r - 2m}$	$\frac{\rho^2}{\triangle}$
$g_{\theta\theta}$	$r^2$	$r^2$	$\rho^2$
$g_{\phi\phi}$	$r^2 \sin^2(\theta)$	$r^2 \sin^2(\theta)$	$(r^2 + a^2 + \frac{2 m r a^2 \sin^2(\theta)}{\rho^2}) \sin^2{\theta}$
$g_{ij}$ $i \neq j$	all zero	all zero	all zero except $g_{t \phi} = g_{\phi t} = - \frac{2 m r a \sin^2(\theta)}{\rho^2}$

---

Substractive logic is an extension of (propositional or first order) intuitionistic logic with a new connective, subtraction, dual to implication, such that each sentence $A$ have a “dual” $\overline{A}$ verifying $A \vdash_{\text{SL}} B$ if and only if $\overline{B} \vdash_{\text{SL}} \overline{A}$. Propositional substractive logic is a conservative extension over propositional intuitionistic logic, but it is not the case for the first order case.

Syntax and idea

In the following and to the rest of the articles, uppercases letters $A, B, C, D$ will denote sentences.

We start with (a slightly modified) Gentzen's LJ sequent calculus, whose rules are as follow:

Axioms:

$$\frac{}{A \vdash_{\text{SL}} A} \; \text{ax} \qquad \frac{}{\bot \vdash_{\text{SL}} A}\;\text{ax} \qquad \frac{}{A \vdash_{\text{SL}} \top}\; \text{ax}$$

Cut:

$$\frac{A \vdash_{\text{SL}} C \quad C \vdash_{\text{SL}} B}{A \vdash_{\text{SL}} B} \; \text{cut}$$

Rules of conjonctions:

$$\frac{}{A \wedge B \vdash_{\text{SL}} A} \;\text{elim-}\wedge_1 \qquad \frac{}{A \wedge B \vdash_{\text{SL}} B} \;\text{elim-}\wedge_2 \qquad \frac{A \vdash_{\text{SL}} B \quad A \vdash_{\text{SL}} C}{A \vdash_{\text{SL}} B \wedge C} \;\text{intro-}\wedge$$

Rules of disjonctions:

$$\frac{}{A \vdash_{\text{SL}} A \vee B} \;\text{intro-}\vee_1 \qquad \frac{}{B \vdash_{\text{SL}} A \vee B} \;\text{intro-}\vee_2 \qquad \frac{A \vdash_{\text{SL}} C \quad B \vdash_{\text{SL}} C}{A \vee B \vdash_{\text{SL}} C} \;\text{elim-}\vee$$

Notice that rules for conjonctions and disjonctions are eerly similar, in particular if $A$ and $B$ are composed only of conjonctions, disjonctions and atoms, noting by $\overline{A}$ and $\overline{B}$ the same formulas but replacing each conjonctions by disjonctions and disjonctions by conjonctions simultaneously, then $A \vdash_{\text{SL}} B$ if and only if $\overline{B} \vdash_{\text{SL}} \overline{A}$. That is what we mean by saying that conjonctions and disjonctions are dual. In the same vein, top and bottom are duals.

Rules of implications:

$$\frac{}{(A \implies B) \wedge A \vdash_{\text{SL}} B}\;\text{elim-}\implies \qquad \frac{A \wedge B \vdash_{\text{SL}} C}{A \vdash_{\text{SL}} B \implies C}\;\text{intro-}\implies$$

This rule usually do not have a dual in intuitionistic logic, but we’ll just create one written $A - B$, rules of substractions:

$$\frac{}{B \vdash_{\text{SL}} (A \implies B) \vee A}\;\text{elim-}\text{sub} \qquad \frac{C \vdash_{\text{SL}} A \vee B}{B - C\vdash_{\text{SL}} A}\;\text{intro-}\text{sub}$$

Giving the syntax of propositional substractive logic, to make it first order, it suffice to add the existential operator and its dual, the forall operator (where $x$ does not occur free in $C$):

$$\frac{A \vdash_{\text{SL}} C}{\exists x.A \vdash_{\text{SL}} C}\;\text{elim-}\exists \qquad \frac{A \vdash_{\text{SL}} B[t/x]}{A \vdash_{\text{SL}} \exists x. B}\;\text{intro-}\exists$$

and

$$\frac{C \vdash_{\text{SL}} A}{C \vdash_{\text{SL}} \forall x. A}\;\text{intro-}\forall \qquad \frac{B[t/x] \vdash_{\text{SL}} A}{\forall x. B \vdash_{\text{SL}} A}\;\text{elim-}\forall$$

Definition

The dual of a sentence $A$ is another sentence $\overline{A}$ defined by structural induction on the syntax of the sentence by $\begin{cases} A & \,\text{if}\, A \,\text{is an atom}\\ \bot & \,\text{if}\, A = \top \\ \top & \,\text{if}\, A = \bot \\ \overline{C} \vee \overline{B} & \,\text{if}\, A = B \wedge C \\ \overline{C} \wedge \overline{B} & \,\text{if}\, A = B \vee C \\ \overline{C} \implies \overline{B} & \,\text{if}\, A = B - C \\ \overline{C} - \overline{B} & \,\text{if}\, A = B \implies C \\ \exists x. \overline{B} & \,\text{if}\, A = \forall x. B\\ \forall x. \overline{B} & \,\text{if}\, A = \exists x. B \end{itemize} \end{cases}$.

– comment ? // comment ? {-# comment ? #-}