We give an example of proving scheme derivability. We will also use a module
for outputting natural deduction trees as \LaTeX.

\AgdaHide{
\begin{code}

open import Agda.Builtin.Nat renaming (Nat to ℕ) hiding (_-_)
open import Agda.Builtin.Sigma
open import Agda.Builtin.String

open import Decidable hiding (⊥ ; ¬_)
open import Deduction
open import Ensemble
open import Formula
open import List
open import Scheme
open import Vec

\end{code}
}

\begin{code}

open import Texify

\end{code}
The code for this is entirely computational, and can be found in the appendix.

First, some syntactic sugar. The \inline{pattern} notation causes Adga to
recognise the notation in places where their values would be used in pattern
matching, and moreover will use the notation in proofs created by proof search.
Note that we are no longer using \inline{⊥} and \inline{¬} as defined
previously for decidable predicates in the metalanguage; here they are in the
language of formulae.
\begin{code}

pattern ⊥ = atom (rel zero zero) []

pattern ¬  α = α ⇒ ⊥
pattern ¬¬ α = ¬ (¬ α)

\end{code}
Fix some variables.
\begin{code}

pattern xvar = var zero
pattern yvar = var (suc zero)

x y : Term
x = varterm xvar
y = varterm yvar

pattern  ∀x  Φ = Λ xvar Φ
pattern  ∃x  Φ = V xvar Φ
pattern ¬∀x  Φ = ¬(∀x Φ)
pattern ¬∃x  Φ = ¬(∃x Φ)
pattern  ∀x¬ Φ = ∀x (¬ Φ)
pattern  ∃x¬ Φ = ∃x (¬ Φ)

\end{code}
Define a nullary and a unary predicate (in the language of formulae), which
will be used to instantiate the scheme proofs for output as proof trees in
\LaTeX.
\begin{code}

pattern Arel = rel 1 0
pattern A    = atom Arel []

pattern Prel = rel 5 1
pattern P t  = atom Prel (t ∷ [])

\end{code}
The indices used for $x$, $y$, $\bot$, $A$, and $P$ are arbitrary, but
correspond to those used internally by the texify module, so they will be
outputted with the appropriate names.

Define the schemes DNE (double negation elimination), EFQ (ex falso quodlibet),
DP (the drinker paradox), and H$\epsilon$ (the dual of the drinker paradox).
The latter two schemes will be described and examined in more detail in the
next chapter.
\begin{code}

dne efq dp hε : Formula → Formula
dne Φ  = ¬¬ Φ ⇒ Φ
efq Φ  = ⊥ ⇒ Φ
dp  Φx = ∃x(Φx ⇒ ∀x Φx)
hε  Φx = ∃x(∃x Φx ⇒ Φx)

DNE EFQ DP Hε : Scheme
DNE = unaryscheme "DNE"          dne
EFQ = unaryscheme "EFQ"          efq
DP  = unaryscheme "DP"           dp
Hε  = unaryscheme "H$\\epsilon$" hε

\end{code}

The natural deduction system used to define \inline{_⊢_} is for minimal logic.
This can be extended to classical logic with the classical $\bot$ rule.
\begin{code}

⊥c-rule : Set₁
⊥c-rule = ∀{Γ} → ∀ α
          →      Γ ⊢ ⊥
            --------------- ⊥c
          →  Γ - (¬ α) ⊢ α

\end{code}
Similarly, the intuitionistic $\bot$ rule
\begin{code}

⊥i-rule : Set₁
⊥i-rule = ∀{Γ} → ∀ α
          →      Γ ⊢ ⊥
                ------- ⊥i
          →      Γ ⊢ α

\end{code}
gives an extension to intuitionistic logic.

\begin{proposition}
The classical bottom rule holds if and only if DNE is derivable.
\end{proposition}
\begin{proof}
$ $
\begin{code}

dne→⊥c-rule : ⊢₁ dne → ⊥c-rule
\end{code}
\begin{prooftree}
  \AxiomC{}
  \RightLabel{DNE}
  \UnaryInfC{$\lnot\lnot\alpha \rightarrow \alpha$}
      \AxiomC{$\Gamma$,\, [$\lnot\alpha$]}
      \noLine\UnaryInfC{$\vdots$}\noLine
      \UnaryInfC{$\bot$}
      \RightLabel{$\rightarrow^+$}
      \UnaryInfC{$\lnot\lnot\alpha$}
    \RightLabel{$\rightarrow^-$}
    \BinaryInfC{$\alpha$}
\end{prooftree}
\begin{code}
dne→⊥c-rule ⊢dne α Γ⊢⊥ = close
                          (assembled-context (arrowintro (¬ α) Γ⊢⊥))
                          (λ x₁ z₁ z₂
                           → z₂ (λ z₃ → z₁ (λ z₄ → z₄) (λ z₄ → z₄ z₃)))
                          (arrowelim
                           (⊢dne α)
                           (arrowintro (¬ α)
                            Γ⊢⊥))

⊥c-rule→dne : ⊥c-rule → ⊢₁ dne
\end{code}
\begin{prooftree}
  \AxiomC{[$\lnot\lnot\alpha$]}
      \AxiomC{[$\lnot\alpha$]}
    \RightLabel{$\rightarrow^-$}
    \BinaryInfC{$\bot$}
    \RightLabel{$\bot_\text{c}$}
    \UnaryInfC{$\alpha$}
    \RightLabel{$\rightarrow^+$}
    \UnaryInfC{$\lnot\lnot\alpha \rightarrow \alpha$}
\end{prooftree}
\begin{code}
⊥c-rule→dne ⊢⊥c-rule α = close
                          from∅
                          (λ x₁ z₁ z₂
                           → z₂ (z₁ (λ z₃ z₄ → z₄ (λ z₅ z₆ → z₆ z₃ z₅))))
                          (arrowintro (¬¬ α)
                           (⊢⊥c-rule α
                            (arrowelim
                             (assume (¬¬ α))
                             (assume (¬ α)))))

\end{code}
\codeqed
\end{proof}

\begin{proposition}
The intuitionistic bottom rule holds if and only if EFQ is derivable.
\end{proposition}
\begin{proof}
$ $
\begin{code}

efq→⊥i-rule : ⊢₁ efq → ⊥i-rule
\end{code}
\begin{prooftree}
  \AxiomC{}
  \RightLabel{EFQ}
  \UnaryInfC{$\bot \rightarrow \alpha$}
      \AxiomC{$\Gamma$}
      \noLine\UnaryInfC{$\vdots$}\noLine
      \UnaryInfC{$\bot$}
    \RightLabel{$\rightarrow^-$}
    \BinaryInfC{$\alpha$}
\end{prooftree}
\begin{code}
efq→⊥i-rule ⊢efq α Γ⊢⊥ = close
                          (assembled-context Γ⊢⊥)
                          (λ x₁ z₁ → z₁ (λ z₂ → z₂))
                          (arrowelim
                           (⊢efq α)
                           Γ⊢⊥)

⊥i-rule→dne : ⊥i-rule → ⊢₁ efq
\end{code}
\begin{prooftree}
  \AxiomC{[$\bot$]}
  \RightLabel{$\bot_\text{i}$}
  \UnaryInfC{$\alpha$}
  \RightLabel{$\rightarrow^+$}
  \UnaryInfC{$\bot \rightarrow \alpha$}
\end{prooftree}
\begin{code}
⊥i-rule→dne ⊢⊥i-rule α = close
                          from∅
                          (λ x₁ z₁ z₂ → z₂ (z₁ (λ z₃ → z₃)))
                          (arrowintro ⊥
                           (⊢⊥i-rule α
                            (assume ⊥)))

\end{code}
\codeqed
\end{proof}

\begin{proposition}
DP holds in classical logic.
\end{proposition}
\begin{proof}
We show that if DNE is derivable then DP is derivable, meaning that DP is
weaker than DNE. For illustrative purposes, lines given by Agda's proof search
are marked with \inline{{- Auto -}} in the next proof. The remainder of the
proof, with the exception of the \inline{close} function call, corresponds
exactly to doing natural deduction by hand, from the bottom up. As the
proof tree is developed, Agda displays the subgoal of each hole in the
deduction, and will accept valid subproofs and formulae only. In this way, Agda
not only verifies the deduction after it has been completed, but also acts as a
proof assistant for natural deduction.
\begin{code}

dne→dp : ⊢₁ dne → ⊢₁ dp
dne→dp ⊢dne α = close
  {- Auto -}     from∅
  {- Auto -}     (λ x₁ z₁ z₂ → z₂ (z₁ (λ z₃ → z₃) (λ z₃ → z₃ (λ z₄ z₅ → z₅ z₄
  {- Auto -}      (λ z₆ → z₆ (λ _ z₇ → z₇ (λ z₈ → z₈) (λ z₈ → z₈ (λ z₉ z₁₀
  {- Auto -}       → z₁₀ z₄ (λ z₁₁ → z₁₁ (λ z₁₂ z₁₃ → z₁₃ (λ z₁₄ → z₁₄)
  {- Auto -}        (λ z₁₄ → z₁₄ (λ _ z₁₅ → z₁₅ z₉ z₁₂))))))))))))
                 (arrowelim
                  (⊢dne (dp α))
                  (arrowintro (¬ (dp α))
                   (arrowelim
                    (assume (¬ (dp α)))
                    (existintro x xvar
  {- Auto -}         (ident (α ⇒ ∀x α) xvar)
                     (arrowintro α
                      (univintro xvar
  {- Auto -}           (all∅ all∪ (all- (all⟨ V↓ xvar (α ⇒ ∀x α) ⇒ atom [] ⟩
  {- Auto -}            all∪ (all- (all∅ all∪ (all- (all⟨- ¬∀x α ∷ (α ∷
  {- Auto -}             [ refl ]) ⟩ all∪ all⟨- ¬∀x α ∷ [ refl ] ⟩)))))))
                       (arrowelim
                        (⊢dne α)
                        (arrowintro (¬ α)
                         (arrowelim
                          (assume (¬ (dp α)))
                          (existintro x xvar
  {- Auto -}               (ident (α ⇒ ∀x α) xvar)
                           (arrowintro α
                            (arrowelim
                             (⊢dne (∀x α))
                             (arrowintro (¬∀x α)
                              (arrowelim
                               (assume (¬ α))
                               (assume α)))))))))))))))

\end{code}
\codeqed
\end{proof}
The above is a general derivation of an arbitrary instance of DP using
instances of DNE. We use this proof to construct the scheme relation
`$\supset$', for outputting as \LaTeX.
\begin{code}

DNE⊃DP : DNE ∷ [] ⊃ DP
DNE⊃DP ⊢lhs (α ∷ []) = dne→dp (descheme₁ (⊢lhs DNE [ refl ])) α
dp-prooftree = texreduce DP (P x ∷ []) DNE⊃DP

\end{code}
The final line gets the deduction tree for the instance $\text{DP}({Px})$,
which is shown below, with instances of DP abbreviated, and split into two, due
to page constraints.

\begin{prooftree}
  \AxiomC{$\left[\lnot{\exists{x}\left(P{x} \rightarrow \forall{x}P{x}\right)}\right]$}
    \AxiomC{}
    \RightLabel{DNE}
    \UnaryInfC{$\lnot{\lnot{\forall{x}P{x}}} \rightarrow \forall{x}P{x}$}
      \AxiomC{$\left[\lnot{P{x}}\right]$}
        \AxiomC{$\left[P{x}\right]$}
      \RightLabel{$\rightarrow^-$}
      \BinaryInfC{$\bot$}
      \RightLabel{$\rightarrow^+$}
      \UnaryInfC{$\lnot{\lnot{\forall{x}P{x}}}$}
    \RightLabel{$\rightarrow^-$}
    \BinaryInfC{$\forall{x}P{x}$}
    \RightLabel{$\rightarrow^+$}
    \UnaryInfC{$P{x} \rightarrow \forall{x}P{x}$}
    \RightLabel{$\exists^+$}
    \UnaryInfC{$\exists{x}\left(P{x} \rightarrow \forall{x}P{x}\right)$}
  \RightLabel{$\rightarrow^-$}
  \BinaryInfC{$\bot$}
  \UnaryInfC{$\vdots$}
\end{prooftree}
\begin{prooftree}
\AxiomC{}
\RightLabel{DNE}
\UnaryInfC{$\lnot{\lnot{\text{DP}({Px})}} \rightarrow \text{DP}({Px})$}
    \AxiomC{$\left[\lnot{\exists{x}\left(P{x} \rightarrow \forall{x}P{x}\right)}\right]$}
      \AxiomC{}
      \RightLabel{DNE}
      \UnaryInfC{$\lnot{\lnot{P{x}}} \rightarrow P{x}$}
        \AxiomC{$\vdots$}
        \UnaryInfC{$\bot$}
        \RightLabel{$\rightarrow^+$}
        \UnaryInfC{$\lnot{\lnot{P{x}}}$}
      \RightLabel{$\rightarrow^-$}
      \BinaryInfC{$P{x}$}
      \RightLabel{$\forall^+$}
      \UnaryInfC{$\forall{x}P{x}$}
      \RightLabel{$\rightarrow^+$}
      \UnaryInfC{$P{x} \rightarrow \forall{x}P{x}$}
      \RightLabel{$\exists^+$}
      \UnaryInfC{$\exists{x}\left(P{x} \rightarrow \forall{x}P{x}\right)$}
    \RightLabel{$\rightarrow^-$}
    \BinaryInfC{$\bot$}
    \RightLabel{$\rightarrow^+$}
    \UnaryInfC{$\lnot{\lnot{\exists{x}\left(P{x} \rightarrow \forall{x}P{x}\right)}}$}
  \RightLabel{$\rightarrow^-$}
  \BinaryInfC{$\exists{x}\left(P{x} \rightarrow \forall{x}P{x}\right)$}
\end{prooftree}
\vspace{\baselineskip}

\begin{proposition}
The dual of the drinker paradox also holds in classical logic.
\end{proposition}
\begin{proof}
$ $
\begin{code}

dne→hε : ⊢₁ dne → ⊢₁ hε
dne→hε ⊢dne α = close
                 from∅
                 (λ x₁ z₁ z₂ → z₂ (z₁ (λ z₃ → z₃) (λ z₃ → z₃ (λ z₄ z₅ → z₅ z₄
                  (λ z₆ → z₆ (λ z₇ z₈ → z₈ (λ z₉ → z₉) (λ z₉ → z₉ (λ _ z₁₀
                   → z₁₀ z₇ (λ z₁₁ → z₁₁ (λ z₁₂ z₁₃ → z₁₃ z₄ (λ z₁₄ → z₁₄
                    (λ _ → z₁₂))))))))))))
                 (arrowelim
                  (⊢dne (hε α))
                  (arrowintro (¬ (hε α))
                   (arrowelim
                    (assume (¬ (hε α)))
                    (existintro x xvar (ident (∃x α ⇒ α) xvar)
                     (arrowintro (∃x α)
                      (arrowelim
                       (⊢dne α)
                       (arrowintro (¬ α)
                        (existelim
                         (all⟨ atom [] ⟩ all∪ (all- (all⟨ V↓ xvar (∃x α ⇒ α)
                          ⇒ atom [] ⟩ all∪ (all- all⟨- ∃x α ∷ [ refl ] ⟩))))
                         (assume (∃x α))
                         (arrowelim
                          (assume (¬ (hε α)))
                          (existintro x xvar (ident (∃x α ⇒ α) xvar)
                           (arrowintro (∃x α)
                            (assume α))))))))))))
\end{code}
\codeqed
\end{proof}

We extract the proof tree for H$\epsilon(Px)$.
\begin{code}

DNE⊃Hε : DNE ∷ [] ⊃ Hε
DNE⊃Hε ⊢lhs (α ∷ []) = dne→hε (descheme₁ (⊢lhs DNE [ refl ])) α
hε-prooftree = texreduce Hε (P x ∷ []) DNE⊃Hε

\end{code}

\begin{prooftree}
  \AxiomC{$\left[\exists{x}P{x}\right]$}
    \AxiomC{$\left[\lnot{\exists{x}\left(\exists{x}P{x} \rightarrow P{x}\right)}\right]$}
      \AxiomC{$\left[P{x}\right]$}
      \RightLabel{$\rightarrow^+$}
      \UnaryInfC{$\exists{x}P{x} \rightarrow P{x}$}
      \RightLabel{$\exists^+$}
      \UnaryInfC{$\exists{x}\left(\exists{x}P{x} \rightarrow P{x}\right)$}
    \RightLabel{$\rightarrow^-$}
    \BinaryInfC{$\bot$}
  \RightLabel{$\exists^-$}
  \BinaryInfC{$\bot$}
  \UnaryInfC{$\vdots$}
\end{prooftree}

\begin{prooftree}
\AxiomC{}
\RightLabel{DNE}
\UnaryInfC{$\lnot{\lnot{\text{H$\epsilon$}(Px)}} \rightarrow \text{H$\epsilon$}(Px)$}
  \AxiomC{$\left[\lnot{\exists{x}\left(\exists{x}P{x} \rightarrow P{x}\right)}\right]$}
    \AxiomC{}
    \RightLabel{DNE}
    \UnaryInfC{$\lnot{\lnot{P{x}}} \rightarrow P{x}$}
      \AxiomC{$\vdots$}
      \UnaryInfC{$\bot$}
      \RightLabel{$\rightarrow^+$}
      \UnaryInfC{$\lnot{\lnot{P{x}}}$}
    \RightLabel{$\rightarrow^-$}
    \BinaryInfC{$P{x}$}
    \RightLabel{$\rightarrow^+$}
    \UnaryInfC{$\exists{x}P{x} \rightarrow P{x}$}
    \RightLabel{$\exists^+$}
    \UnaryInfC{$\exists{x}\left(\exists{x}P{x} \rightarrow P{x}\right)$}
  \RightLabel{$\rightarrow^-$}
  \BinaryInfC{$\bot$}
  \RightLabel{$\rightarrow^+$}

  \UnaryInfC{$\lnot{\lnot{\exists{x}\left(\exists{x}P{x} \rightarrow P{x}\right)}}$}
\RightLabel{$\rightarrow^-$}
\BinaryInfC{$\exists{x}\left(\exists{x}P{x} \rightarrow P{x}\right)$}
\end{prooftree}
\vspace{\baselineskip}

As a final example, consider the law of excluded middle, and a general form of
the limited principle of omniscience.\footnote{This is general in the sense that
it is not over a binary sequence, like that of \citet{varieties}, but rather
over a predicate which may not be decidable.}
\begin{code}

lem glpo : Formula → Formula
lem  Φ = Φ ∨ (¬ Φ)
glpo Φ = ∀x (¬ Φ) ∨ ∃x Φ

LEM GLPO : Scheme
LEM  = unaryscheme "LEM"  lem
GLPO = unaryscheme "GLPO" glpo

\end{code}
Recall that equivalent formulae are equivalently derivable, so from GLPO we may
derive a form with any other quantifying variable. Therefore while the variable
$x$ is fixed, it can be expected that LEM and GPO are equivalent with respect
to derivability.  That is, in an extension of minimal logic where one is
derivable, the other should also be derivable. The former leads to the latter
in a straightforward manner. The other direction is more complicated, since
$\Phi$ could have $x$ free.

We show first that when deriving $\text{LEM}(\Phi)$, we may assume without
loss of generality that $x$ is not free in $\Phi$, by showing that if LEM is
derivable in this restricted case then it is derivable in general.

\begin{proof}
Given any formula $\alpha$, there is a fresh variable $\omega$ which appears
nowhere in $\alpha$ and which differs from $x$. Then $\alpha[x/\omega]$ exists,
with $x$ not free, and $\alpha[x/\omega][\omega/x] = \alpha$. Now if LEM holds
for $\alpha[x/\omega]$ then it holds for $\alpha$, by the following proof tree.
\begin{prooftree}
  \AxiomC{}
  \UnaryInfC{$\alpha[x/\omega] \lor \lnot\alpha[x/\omega]$}
  \RightLabel{$\forall^+$}
  \UnaryInfC{$\forall\omega \left(\alpha[x/\omega] \lor \lnot\alpha[x/\omega]\right)$}
  \RightLabel{$\forall^-$}
  \UnaryInfC{$\alpha \lor \lnot\alpha$}
\end{prooftree}
Hence we may derive LEM by deriving it only for formulae for which $x$ is not
free.  This is formalised in Agda as follows.
\begin{code}

wlog-lem : (∀ α → xvar NotFreeIn α → ⊢ (lem α)) → ⊢₁ lem
wlog-lem ⊢nflem α = close
                     from∅
                     (λ x₁ z₁ z₂ → z₂ z₁)
                     (univelim x lemαω[ω/x]≡lemα
                      (univintro ωvar all∅
                       (⊢nflem αω x∉αω)))
  where
\end{code}
Compute the fresh variable, and use its construction to get that it is fresh in
$\alpha$ and not equal to $x$.
\begin{code}
    ω,ωFresh,x≢ω : Σ Variable (λ ω → Σ (ω FreshIn α) (λ _ → xvar ≢ ω))
    ω,ωFresh,x≢ω with fresh (∀x α)
    ...          | ω , Λ x≢ω ωFrα = ω , ωFrα , x≢ω
\end{code}
We therefore have a variable $\omega$ which is not free in $\alpha$, which is
free for $x$ in $\alpha$, and which differs from $x$.
\begin{code}
    ωvar          : Variable
    ω∉α           : ωvar NotFreeIn α
    ωFreeForxInα  : (varterm ωvar) FreeFor xvar In α
    x≢ω           : xvar ≢ ωvar
    ωvar          = fst ω,ωFresh,x≢ω
    ω∉α           = freshNotFree (fst (snd ω,ωFresh,x≢ω))
    ωFreeForxInα  = freshFreeFor (fst (snd ω,ωFresh,x≢ω)) xvar
    x≢ω           = snd (snd ω,ωFresh,x≢ω)
\end{code}
Now, compute $\alpha_\omega = \alpha[x/\omega]$.
\begin{code}
    αω        : Formula
    α[x/ω]≡αω : α [ xvar / _ ]≡ αω
    αω        = fst (α [ xvar / ωFreeForxInα ])
    α[x/ω]≡αω = snd (α [ xvar / ωFreeForxInα ])
\end{code}
By the construction of $\omega$, the substitution is reversible, so
$\text{LEM}(\alpha_\omega)[\omega/x] = \text{LEM}(\alpha)$.
\begin{code}
    lemαω[ω/x]≡lemα : (lem αω) [ ωvar / _ ]≡ (lem α)
    lemαω[ω/x]≡lemα = subInverse
                       (ω∉α ∨ (ω∉α ⇒ atom []))
                       (α[x/ω]≡αω ∨ (α[x/ω]≡αω ⇒ notfree (atom [])))
\end{code}
Finally, $x$ will not be free after it has been substituted out of $\alpha$.
\begin{code}
    x∉αω : xvar NotFreeIn αω
    x∉αω = subNotFree (varterm x≢ω) α[x/ω]≡αω

\end{code}
\codeqed
\end{proof}

We can now show that GLPO is stronger than LEM, without worrying about the
quantifier variable.
\begin{code}

glpo→xnf→lem : ⊢₁ glpo → ∀ α → xvar NotFreeIn α → ⊢ (lem α)
glpo→xnf→lem ⊢glpo α x∉α = close
                            from∅
                            (λ x₁ z₁ z₂ → z₂ (z₁ (λ z₃ → z₃) (λ z₃ → z₃
                             (λ z₄ → z₄ (λ z₅ → z₅)) (λ z₄ → z₄ (λ z₅ z₆ → z₆
                              z₅ (λ z₇ → z₇ (λ z₈ → z₈)))))))
                            (disjelim
                             (⊢glpo α)
                             (disjintro₂ α
                              (univelim x (ident (¬ α) xvar)
                               (assume (∀x¬ α))))
                             (disjintro₁ (¬ α)
                              (existelim (all⟨ x∉α ⟩ all∪ (all- all⟨ x∉α ⟩))
                               (assume (∃x α))
                               (assume α))))

\end{code}
Now, LEM can be obtained directly from GLPO. The proof tree for the restricted
form of LEM is inserted into the proof tree from \inline{wlog-lem}.
\begin{code}

glpo→lem : ⊢₁ glpo → ⊢₁ lem
glpo→lem ⊢glpo = wlog-lem (glpo→xnf→lem ⊢glpo)

GLPO⊃LEM : GLPO ∷ [] ⊃ LEM
GLPO⊃LEM ⊢lhs (α ∷ []) = glpo→lem (descheme₁ (⊢lhs GLPO [ refl ])) α

\end{code}
No computation of a fresh variable has occurred yet, since the variable depends
on the instance of LEM we want to derive. Extracting the proof tree for
$\text{LEM}(Px)$, the \inline{fresh} function computes that $y$ is fresh, and
so the proof tree below is produced.
\begin{code}

glpo→lem-prooftree = texreduce LEM (P x ∷ []) GLPO⊃LEM

\end{code}

\begin{prooftree}
\AxiomC{}
\RightLabel{GLPO}
\UnaryInfC{$\forall{x}\lnot{P{y}} \lor \exists{x}P{y}$}
  \AxiomC{$\left[\forall{x}\lnot{P{y}}\right]$}
  \RightLabel{$\forall^-$}
  \UnaryInfC{$\lnot{P{y}}$}
  \RightLabel{$\lor^+$}
  \UnaryInfC{$P{y} \lor \lnot{P{y}}$}
    \AxiomC{$\left[\exists{x}P{y}\right]$}
      \AxiomC{$\left[P{y}\right]$}
    \RightLabel{$\exists^-$}
    \BinaryInfC{$P{y}$}
    \RightLabel{$\lor^+$}
    \UnaryInfC{$P{y} \lor \lnot{P{y}}$}
\RightLabel{$\lor^-$}
\TrinaryInfC{$P{y} \lor \lnot{P{y}}$}
\RightLabel{$\forall^+$}
\UnaryInfC{$\forall{y}\left(P{y} \lor \lnot{P{y}}\right)$}
\RightLabel{$\forall^-$}
\UnaryInfC{$P{x} \lor \lnot{P{x}}$}
\end{prooftree}

