Formal proofs

There are many ways to organize formal proofs of typed formulas, e.g. natural deduction, the sequent calculus, or its dual, tableauxtableaux proof, or Hilbert style systems to name a few. We choose a sequent calculus presented in a top-down fashion (as with tableaux). We call this a refinement logicrefinement logic (RL). The choice is motivated by the advantages sequents provide for automation and display.¹⁸ Here is what a simple proof looks like for $A \in Type$, $P \in A \rightarrow Prop$; only the relevant hypotheses are mentioned and only the first time they are generated.

	$\vdash \forall x: A.\: (\forall y: A.\: P(y) \Rightarrow \exists x: A.\: P(x))$	by $\forall R$
1.	$x:A \vdash \forall y: A.\: P(y) \Rightarrow \exists x:A.\: P(x)$	by $\Rightarrow\!\!R$
1.1	$f: (\forall y : A.\: P(y)) \vdash \exists x:A.\: P(x)$	by $\forall L$ on f with x
1.1.1	$l: P(x) \vdash \exists x: A.\: P(x)$	by $\exists R$with x
	1.1.1.1 $\vdash P(x)$	by $hyp\; l$
	1.1.1.2 $\vdash x \in A$	by $hyp\; x$
1.1.2	$\vdash x \in A$	by $hyp\; x$

The schematic tree structure with path names is

	$\vdash G$
	|
	1.    $H_1 \vdash G_1$
	|
	1.1     $H_2 \vdash G_2$
	$\left / \ \right \backslash$
	1.1.1     $H_3 \vdash G_2$      1.1.2     $H_2 \vdash G_3$
	$/ \ \backslash$
	1.1.1.1     $H_3 \vdash G_4$     1.1.1.2     $H_3 \vdash G_3$