BoxProver Guide

• Introduction
• Tutorial
  • A simple example
  • Temporary assumptions
  • Interactive proving
  • Advanced holes
• Syntax
  • Variables
  • Formulas
  • Sequents
  • Proofs
    • Proof lines
    • Assumptions/premises
    • Boxes
    • Chaining proofs together
• Rule reference
• Idioms and avanced usage
  • Lemmas

Introduction

BoxProver is a userfriendly front-end to the Twelf proof assistant, and provides a simple way to encode and verify natural deduction proofs in propositional and first-order logic using Fitch-style notation. Although all proofs will be specified in the language of Twelf, no knowledge of this language is required from the user. Besides verification, BoxProver also has facilities for producing visual representations of proofs, closely following the style and notation of the book Logic in Computer Science, 2nd edition by Huth & Ryan (henceforth referred to as H&R).

The following section gives a quick crash-course in BoxProver. If this is the first time you are using BoxProver, start by reading that. The sections on syntax and rules contains details on the syntactic structure and proof rules.

Tutorial

Every BoxProver script must follow this general format:

%abbrev
proof_name : {p1}{p2} ... {pn} proof ( ... sequent ... ) =
[p1][p2] ... [pn]

 ... proof body ...

.

This will declare a proof named proof_name which proves a given sequent about propositions p₁, p₂, ..., p_n. We will explain this in more detail in the following using a concrete example.

A simple example

Let us consider Example 1.6 from H&R:

The box proof above has been produced by BoxProver from the following formal proof script (click the button on the right to open the script in BoxProver):

%abbrev
ex1-6 : {p}{q}{r}{s}{t}
        proof ((p /\ q) /\ r , s /\ t , |- q /\ s) =
[p][q][r][s][t]
(p /\ q) /\ r       assumption;    [l1]
s /\ t              assumption;    [l2]
p /\ q              by con_e1 l1 ; [l3]
q                   by con_e2 l3 ; [l4]
s                   by con_e1 l2 ; [l5]
q /\ s              by con_i l4 l5
.

The proof script language is intentionally designed to resemble Fitch-style notation as much as possible. As can be seen, the proof script is also written line-by-line with a formula on each line accompanied by the rule justifying it. Unlike Fitch-proofs, lines are not referenced by their number, but are instead given a name. The names are written in square brackets in the rightmost column, and are intentionally chosen to resemble the original line numbering scheme.

The %abbrev declaration on the first line is required by Twelf and is unrelated to the proof that we are formalizing. It changes the way Twelf does type-checking and is required when we want to develop proofs in a more interactive fashion. For this particular example we can actually remove it, but since it never results in an error to include it, it is safest just to keep it in all your proofs.

The formal proof language require that we explicitly write down the sequent that we want to prove as well as the names of all propositions that we will be referring to. This information is provided in the preamble in lines 2-4. Line 2 defines the name of our proof to be ex1-6 and defines the names p, q, r, s, t as propositions such that they can be used in the statement of the proof sequent in Line 3. Each name must be put in curly braces, and BoxProver figures out by itself that each name stands for a proposition based on how it is used. A more verbose, but equivalent, way to express the same would be by the line

{p:prop}{q:prop}{r:prop}{s:prop}{t:prop}

The sequent is followed by an equals sign which marks the beginning of the proof body. The first thing we must do in the proof body is to repeat the declarations of the propositions that we intend to use, but this time enclosed in square brackets instead of curly braces. Then follows the actual proof body which is terminated by a single dot (.).

A proof line is justified either by an introduction rule or a general rule. The rule assignment; (note that the semicolon is part of the name) is an introduction rule, and requires that the line it appears on is given a name. The meaning of the rule is to take an assumption from the list of premises and make it available to the rest of the proof body. The line

p /\ q by con_e1 l1

Proof lines are combined using the ; (semicolon) operator. The semicolon must be surrounded by whitespace and be followed by a line name enclosed in square brackets. This has the effect of giving a name to the conclusion of the rule to the left, which can then be referenced by later rules.

Temporary assumptions

Fitch-proofs uses boxes to demarcate temporary assumptions. The BoxProver encoding of temporary assumptions also closely resemble the Fitch notation, which we will demonstrate with another example. Consider Example 1.14 from H&R:

%abbrev
ex1-14 : {p}{q}{r}
  proof (p => (q => r)
        , |- p /\ q => r) =
[p][q][r]
p => (q => r)   premise; [@prem]
(   p /\ q      assumption; [@assump]
    p           by con_e1 @assump ; [@p]
    q           by con_e2 @assump ; [@q]
    q => r      by imp_e @p @prem ; [@qr]
    r           by imp_e @q @qr
)               ; [#box]
p /\ q => r     by imp_i #box.

Local assumptions are simply represented by parentheses, with the caveat that the closing parenthesis must be followed by a semicolon and a name in brackets. All line references introduced inside the parentheses are invisible outside the parentheses (effictively introducing a nested scope similarly to scoping in programming languages), including the assumption made on Line 2. The name #box becomes a reference to the whole box and can be used in rules expecting a "box" premise.

To understand precisely how line references work, it might be instructive to see how the fully annotated proof script looks. This assigns a "type" to every line reference which is used to check that it is used correctly:

%abbrev
ex1-14 : {p}{q}{r}
  proof (p => (q => r)
        , |- p /\ q => r) =
[p][q][r]
p => (q => r) premise;            [@prem   : ref (|- p => q => r)]
(   p /\ q    assumption;         [@assump : ref (|- p /\ q)]
    p         by con_e1 @assump ; [@p      : ref (|- p)]
    q         by con_e2 @assump ; [@q      : ref (|- q)]
    q => r    by imp_e @p @prem ; [@qr     : ref (|- q => r)]
    r         by imp_e @q @qr
)             ;                   [#box    : ref (p /\ q , |- r)]
p /\ q => r   by imp_i #box.

Note that every reference is typed by a sequent which for every single-line reference has no premises, and which for the "box" reference has a single premise. That is, the annotation #box : ref (p /\ q , |- r) indicates that lines 2 to 6 forms a valid proof of the sequent p ∧ q ⊢ r.

Interactive proving

If you are writing a large proof, you may want to check if your steps up until now are sound. BoxProver allows you to do this by providing a partial proof with "holes" in it. The system will accept your partial proof if the steps around the hole are sound and if the all references to the hole are consistent. Furthermore, if BoxProver can infer anything about what formula your hole must prove, it will tell you that information.

In order to insert a hole in a proof, you may simply write a single underscore (_) in place of a formula, proof or reference. This is also the easiest way to start a proof and make sure that you have written the proof preamble correctly — simply insert a hole for the entire proof body and ask BoxProver if the rest is correct. For example, let us encode the proof of Example 1.23 in H&R, which proves the sequent (p ∧ ¬q) → r , ¬r , p ⊢ q. We can thus begin our proof script as follows:

%abbrev
ex1-23 : {p}{q}{r}
  proof (p /\ ~ q => r , ~ r , p , |- q) =
[p][q][r]
_
.

If BoxProver accepts this, it means that we did not make any mistakes in the encoding of the sequent. Furthermore, it will render a partial proof that looks as follows:

Alpha#1 is an auto-generated name for the hole, and it tells us that we need to prove q using assumptions/premises p ∧ q → r, ¬r and p. The red color indicates that the proof is not yet finished. Below the proof, BoxProver will also produce an overview of the local assumptions available to the proof that needs to be filled in for the hole. This is especially useful if you have a large proof and you have lost track of what assumptions you have introduced.

Let us go ahead and introduce the three premises, followed by another hole:

%abbrev
ex1-23 : {p}{q}{r}
  proof (p /\ ~ q => r , ~ r , p , |- q) =
[p][q][r]
p /\ ~ q => r       premise; [@prem1]
~ r                 premise; [@prem2]
p                   premise; [@prem3]
_
.

Success! BoxProver accepted our partial proof and replied with an updated rendering. It also correctly inferred that the only thing that we have left is to show q. One way of doing that is to show that ¬q would lead to a contradiction, and from that infer that ¬¬q must hold. Assuming that we can prove that, the last line of our proof must be an invocation of the ¬¬e rule which must make a reference to a proof of ¬¬q. Let us use BoxProver to test if that idea will work, and what work we then have left:

%abbrev
ex1-23 : {p}{q}{r}
  proof (p /\ ~ q => r , ~ r , p , |- q) =
[p][q][r]
p /\ ~ q => r       premise; [@prem1]
~ r                 premise; [@prem2]
p                   premise; [@prem3]
q                   by nne _
.

In the above, we inserted a hole for a reference instead of a proof. Below the rendered proof, BoxProver will tell us that Ref#1 needs to be replaced with a concrete reference to a line concluding ¬¬q.

Our plan is to show ¬¬q using the ¬i rule. This rule invocation must be inserted before the application of ¬¬e, and it must be given a reference to a box which proves ⊥ by assuming ¬q. We insert this line into our proof and put a hole for the reference:

%abbrev
ex1-23 : {p}{q}{r}
  proof (p /\ ~ q => r , ~ r , p , |- q) =
[p][q][r]
p /\ ~ q => r       premise; [@prem1]
~ r                 premise; [@prem2]
p                   premise; [@prem3]
~ ~ q               by neg_i _ ;[@n-n-q]
q                   by nne @n-n-q
.

BoxProver will now tell us that Ref#1 must be a reference to a proof of the sequent ¬q ⊢ ⊥. To produce a proof with an assumption, we need to make a new box. The contents of boxes can also be replaced by holes:

%abbrev
ex1-23 : {p}{q}{r}
  proof (p /\ ~ q => r , ~ r , p , |- q) =
[p][q][r]
p /\ ~ q => r       premise; [@prem1]
~ r                 premise; [@prem2]
p                   premise; [@prem3]
(  _
)                   ; [#box1]  
~ ~ q               by neg_i #box1 ;[@n-n-q]
q                   by nne @n-n-q
.

BoxProver infers that we must prove the sequent ¬q ⊢ ⊥, which required that the first line of the box must be an assumption of ¬q. We insert that and continue:

%abbrev
ex1-23 : {p}{q}{r}
  proof (p /\ ~ q => r , ~ r , p , |- q) =
[p][q][r]
p /\ ~ q => r       premise; [@prem1]
~ r                 premise; [@prem2]
p                   premise; [@prem3]
(  ~ q              assumption; [@n-q]
  _
)                   ; [#box1]  
~ ~ q               by neg_i #box1 ;[@n-n-q]
q                   by nne @n-n-q
.

We now need to produce a proof of ⊥ which will be inserted at line 5. At this point, we can look below the rendered proof to get an overview of the assumptions that will be available to us:

As can easily be verified, this just says that all the conclusions at lines 1,2,3 and 4 are available in line 5. Unfortunately the line names are not provided in the current version of BoxProver — this may change in the future.

The last two assumptions can be used to prove the premise of the implication. The implication can then be eliminated to produce r, and finally we can prove ⊥ since we had ¬r as a premise. We fill out the rest of the proof and check that there are no holes left:

%abbrev
ex1-23 : {p}{q}{r}
  proof (p /\ ~ q => r , ~ r , p , |- q) =
[p][q][r]
p /\ ~ q => r       premise; [@prem1]
~ r                 premise; [@prem2]
p                   premise; [@prem3]
(  ~ q              assumption; [@n-q]
  p /\ ~ q          by con_i @prem3 @n-q ; [@pnq]
  r                 by imp_e @pnq @prem1 ; [@r]
  bot               by neg_e @r @prem2
)                   ; [#box1]  
~ ~ q               by neg_i #box1 ;[@n-n-q]
q                   by nne @n-n-q
.

Dealing with errors

While writing the above proof, I accidentally made a reference to @prem2 instead of @prem3 when trying to prove the formula p /\ ~ q.

%abbrev
ex1-23 : {p}{q}{r}
  proof (p /\ ~ q => r , ~ r , p , |- q) =
[p][q][r]
p /\ ~ q => r       premise; [@prem1]
~ r                 premise; [@prem2]
p                   premise; [@prem3]
(  ~ q              assumption; [@n-q]
                    % The line below is wrong
  p /\ ~ q          by con_i @prem2 @n-q ; [@pnq]
  r                 by imp_e @pnq @prem1 ; [@r]
  bot               by neg_e @r @prem2
)                   ; [#box1]  
~ ~ q               by neg_i #box1 ;[@n-n-q]
q                   by nne @n-n-q
.

Instead of producing a typeset proof, BoxProver will respond with the following error message:

[Opening file /tmp/twelf-input10599613932089018456]
/tmp/twelf-input10599613932089018456:10.24-10.41 Error: 
Type mismatch
Expected: proof (|- p /\ ~ q)
Inferred: proof (|- ~ r /\ ~ q)
Head mismatch
Argument type did not match function domain type
(Index object(s) did not match)
[Closing file /tmp/twelf-input10599613932089018456]
/tmp/twelf-input10599613932089018456:1.2-16.2 Error: 
 1 error found
      

The error messages are generated by Twelf and may sometimes look cryptic. The above one is very helpful though. It tells us that the error occurred on line 10 in our proof script, and that we accidentally proved the formula ¬r ∧ ¬q instead of p ∧ ¬q. Since we have developed our proof interactively, we can just delete what we just wrote and go back to the last working state and try again.

Advanced holes

In the previous example we only inserted holes for proofs whose conclusion was known, and we only inserted one hole at a time. BoxProver allows you to insert any number of holes, however, and it also allows you to insert holes for subproofs that are not referenced anywhere else and whose desired conclusion is hence not known. In the following example, we intend to eliminate the disjunction ¬p ∨ q, so we open two boxes which each start assuming one of the disjuncts. We put three holes in the proof, one for each proof in each box, and one for the remainder of the proof:

%abbrev
adv-holes : {p}{q}{r}
proof (p , q => r
      , ~ p \/ q , |- r) =
[p][q][r]
p           premise; [@p]
q => r      premise; [@qr]
~ p \/ q    premise; [@dis]
(   ~ p     assumption; [@np]
    _
)           ;[#box1]
(   q       assumption; [@q]
    _
)           ;[#box2]
_
.

Since the two boxes are not used anywhere, BoxProver cannot figure out what they are supposed to prove, and thus inserts generic placeholders called Sequent#1 and Sequent#2. The parameters (p, q, r, ...) are lists of propositional variables which the unknown sequents may mention.

If we replace the last hole with a correct invocation of the disjunction elimination rule referencing the two boxes, BoxProver will be able to tell us more specific information:

%abbrev
adv-holes : {p}{q}{r}
proof (p , q => r
      , ~ p \/ q , |- r) =
[p][q][r]
p        premise; [@p]
q => r   premise; [@qr]
~ p \/ q premise; [@dis]
(   ~ p  assumption; [@np]
    _
)        ;[#box1]
(   q    assumption; [@q]
    _
)        ;[#box2]
r        by dis_e @dis #box1 #box2
.

Syntax

The following is a reference of the general syntactic structure of BoxProver scripts.

Variables

A variable is an identifier that is not equal to an existing rule name. A valid identifier consists of any sequence of printable non-whitespace characters, except for the following list of reserved symbols:

This means that BoxProver is very relaxed with regards to what it considers to be a valid identifier. For example, @p\/q=>r is a valid identifier, even though p \/ q => r is a formula. This underlines the fact that whitespace around operators is very important to avoid having them interpreted as identifiers.

By convention, identifiers generally begin with a lower-case letter, except for so-called meta-variables standing for proof holes which begin with an upper-case letter. For proofs in predicate logic, we will also use upper-case letters for predicates.

We recommend the following naming convention to keep your proofs readable:

Formulas

Logical connectives are encoded using ASCII imitations of their looks in "real" math notation. The precedence rules match those of H&R, except for first-order quantifiers which require some explicit parentheses. The table below shows how each logical connective is written in BoxProver:

Note that all operators must be surrounded by white-space, including prefix operators such as negation. For example, ~~q, ~~ q and ~ ~q are not valid, but ~ ~ q is.

Sequents

Proof sequents are written almost exactly as in H&R, with ⊢ written as |-, but with the caveat that the last premise before the turnstile must be followed by a rather awkward-looking comma. The syntax is best explained by a series of examples:

The comma symbol , is actually an operator and must be surrounded by whitespace. Remember to put a comma before the turnstile.

Proofs

Proofs in BoxProver are built from a set of primitives which are then composed in order to form larger proofs. Any proof written in BoxProver proves some sequent Φ ⊢ φ, where Φ is a possibly empty list of assumptions and φ is the conclusion of the proof.

The smallest proofs we can build are individual proof lines which just consists of a propositional formula and a justifying rule. In order to make larger proofs, we can either use the assumption operator to introduce new assumptions, or combine two proofs with the sequence operator. This will be described in more detail in the following.

Proof lines

Proof lines are the smallest proofs you can write. A single proof line follows the following format:

where formula is a formula, rule is a rule identifier, and ref₁ thorugh ref_n are line reference identifiers. Note that line references are separated by whitespace only, no commas or parentheses are required.

Assumptions/premises

Suppose we have written a proof α which proves a sequent φ₁ , ... , φn |- ψ and contains a reference to a proof of |- χ named @ref. The operator assumption; can then be used to turn α into a proof of the sequent χ, φ₁, ..., φn |- ψ as follows:

          χ assumption; [@ref]
          α
        

For a concrete example, let α be equal to the following single-line proof:

This will be a valid proof α : proof (|- ~ ~ p) if we assume that @p : ref (|- p) is available as an assumption. We can then write

        p       assumption; [@p]
        ~ ~ p   by nni @p
      

to obtain a new proof β where β : proof (p |- ~ ~ p). We no longer need to assume that there is a reference @p — β will be a well-formed proof regardless of that.

Boxes

A box is simply represented as a proof enclosed in parentheses:

This underlines the fact that boxes are merely scoping delimiters as in normal programming language syntax. The proof inside the parentheses can use the assumption operator to introduce assumptions. The mechanism for referring to boxes is the same as that for referring to lines and will be introduced in the next subsection.

Chaining proofs together

Suppose we have produced the following two proofs:

          α : proof (Φ |- φ)
          β : proof (Ψ |- χ)
      

Furthermore, β may depend on a reference @ref : ref (Φ |- φ). We can apply the chain operator ; (semicolon) to connect α and β with each other, producing a new proof γ : proof(|- χ):

        α        ; [@ref]
        β
      

The new proof γ : proof (Ψ |- χ) will no longer depend on a variable @ref : ref (Φ |- φ).

We illustrate chaining by two concrete examples. For the first example, let α be the proof

        top     by top_i
      

This depends on no references, and we have α : proof (|- top). We let β be the proof

        top /\ top  by con_i @top @top
      

If we assume that @top : ref (|- top) then we will have β : proof(|- top /\ top). We can chain together these two proofs to obtain a single proof γ : proof (|- top /\ top) which no longer depends on @ref:

        top         by top_i ; [@top]
        top /\ top  by con_i @top @top
      

For the second example, we will let the first proof use local assumptions. Let α : proof (p , |- ~ ~ p) be the proof

      (  p        assumption; [@p]
         ~ ~ p    by nni @p
      )
      

and, let β : proof (|- p => ~ ~ p) be the proof

        p => ~ ~ p  by imp_i #box
      

We can then chain together the two proofs to obtain a proof (α ; [#box] β) : |- p => ~ ~ p as follows:

      (  p        assumption; [@p]
         ~ ~ p    by nni @p
      )           ; [#box]
      p => ~ ~ p  by imp_i #box
      

Rule reference

The following is a table showing the BoxProver names for each rule from H&R. Each rule is accompanied by a minimal example showing its use. The examples are also a good way to get familiar with the notation used for formulas/propositions.

ex : proof (|- top) =
top by top_i.

ex : {p}{q} proof (p , q , |- p /\ q) = [p][q]
p      assumption; [l0]
q      assumption; [l1]
p /\ q by con_i l0 l1.

ex : {p}{q} proof (p /\ q , |- p) = [p][q]
p /\ q assumption; [l0]
p      by con_e1 l0.

ex : {p}{q} proof (p /\ q , |- q) = [p][q]
p /\ q assumption; [l0]
q      by con_e2 l0.

ex : {p}{q} proof (p , |- p \/ q) = [p][q]
p      assumption; [l0]
p \/ q by dis_i1 l0.

ex : {p}{q} proof (q , |- p \/ q) = [p][q]
q      assumption; [l0]
p \/ q by dis_i2 l0.

ex : {p}{q} proof (p \/ q , |- q \/ p) = [p][q]
p \/ q    assumption; [l0]
(  p      assumption; [l1]
   q \/ p by dis_i2 l1
)         ; [case1]
(  q      assumption; [l2]
   q \/ p by dis_i1 l2
)         ; [case2]
q \/ p    by dis_e l0 case1 case2.

ex : {p} proof (|- p => p) = [p]
(  p    assumption; [l0]
   p    by copy l0
)       ; [case1]
p => p  by imp_i case1.

ex : {p}{q} proof (p , p => q , |- q) = [p][q]
p      assumption; [l0]
p => q assumption; [l1]
q      by imp_e l0 l1.

ex : {p} proof (p => bot , |- ~ p) = [p]
p => bot    assumption; [l0]
(  p        assumption; [l1]
   bot      by imp_e l1 l0
)           ; [case1]
~ p         by neg_i case1.

ex : {p} proof (p , ~ p , |- bot) = [p]
p    assumption; [l0]
~ p  assumption; [l1]
bot  by neg_e l0 l1.

ex : {p} proof (bot , |- p /\ ~ p) = [p]
bot      assumption; [l0]
p /\ ~ p by bot_e l0.
          

ex : {p} proof (~ ~ ~ p , |- ~ p) = [p]
~ ~ ~ p  assumption; [l0]
~ p      by nne l0.

ex : {p} proof (|- p \/ ~ p) = [p]
p \/ ~ p  by lem.

%abbrev
ex : {p} proof (p , |- p) = [p]
p       assumption; [l0]
(   ~ p assumption; [l1]
    bot by neg_e l0 l1
)       ; [l1-2]
p       by pbc l1-2.

ex : {p} proof (p , |- ~ ~ p) = [p]
p       assumption; [l0]
~ ~ p   by nni l0.

ex : {p}{q} proof (p => q , ~ q , |- ~ p) = [p][q]
p => q  assumption; [l0]
~ q     assumption; [l1]
~ p     by mt l0 l1.

ex : {P} proof (|- all ([x] top \/ P x)) = [P]
(var [x]
   top               by top_i ; [l0]
   top \/ P x        by dis_i1 l0
)                    ; [case1]
all ([x] top \/ P x) by all_i case1.

ex : {P}{t} proof (all ([x] P x) , |- P t) = [P][t]
all ([x] P x)  assumption; [l0]
P t            by all_e t l0.

ex : {P} proof (tm [t] P t , |- exi ([x] P x)) = [P]
var[t]
P t           assumption; [l0]
exi ([x] P x) by exi_i t l0.

ex : {P} proof (all ([x] P x) , exi ([y] ~ P y)
                              , |- bot) = [P]
all ([x] P x)    assumption; [l0]
exi ([y] ~ P y)  assumption; [l1]
(var[z]
   ~ P z         assumption; [l2]
   P z           by all_e z l0 ; [l3]
   bot           by neg_e l3 l2
)                ; [case1]
bot              by exi_e l1 case1.

ex : {t:term} proof (|- t == t) = [t]
t == t  by eq_i.

ex : {s}{t}{P} proof (s == t , P s , |- P t) =
[s][t][P]
s == t  assumption; [l0]
P s     assumption; [l1]
P t     by eq_e ([x] P x) l1 l0.

Idioms and advanced usage

Lemmas

BoxProver has limited support for defining lemmas, that is, proof blocks that can be reused later in other proofs.

For example, suppose that our proof system came without the PBC rule. We would then like to prove PBC as a theorem which we can then refer to in place of the actual rule. The effect of this is that the PBC theorem gets "inlined" for every invocation, effectively making its use invisible in the final proof.

For technical reasons, BoxProver cannot inline a proof of a sequent. Instead, we must formulate a lemma as a proof which has explicit, named holes for its premises. Whenever we want to use the lemma we must provide it with concrete references which can be inserted. For example, the PBC lemma looks as follows:

%abbrev
pbc-lemma : {p}
  ref (~ p , |- bot) -> proof (|- p) =
[p][@ref]
~ ~ p           by neg_i @ref ; [@nnp]
p               by nne @nnp
.

BoxProver will tell us that we have proved the following:

This should be read as follows: "for all propositions p, if there is a proof of (¬p ⊢ ⊥) then there is a proof of ⊢ p".

The lemma can be used in all proofs declared after it. Simply begin a new proof (remember to prefix it with %abbrev!) and use the lemma as an ordinary rule:

%abbrev
pbc-lemma : {p}
  ref (~ p , |- bot) -> proof (|- p) =
[p][@ref]
~ ~ p           by neg_i @ref ; [@nnp]
p               by nne @nnp
.
%abbrev
lemma-example : {p}{q}
  proof (q , (~ p) /\ q => bot , |- p) =
[p][q]
q               premise; [@q]
~ p /\ q => bot premise; [@imp]
(   ~ p         assumption; [@np]
    ~ p /\ q    by con_i @np @q ; [@con]
    bot         by imp_e @con @imp
)               ; [#box]
p               by pbc-lemma p #box
.

As a caveat, note that pbc-lemma as a rule takes two arguments: the first is the formula which will take the place for the propositional variable p, and the second is a reference to a box proving bot from ~ p. You may replace the first argument with an underscore, since it can almost always be inferred uniquely from the reference.