Next: About this document
Defining Refinement Logic
Before presenting the solution to problem 1 in assignment 3, let us fix some compact terminology. We will fix the name Refinement Logic (RL) to include the set of rules which uses single goals, considers 
as a list, and which is ``complete'' for Intuitionistic logic along with Magic, Cut and Lemma. We will also agree to treat 
as the defined connective meaning 
. This means that we include True and False as constants in Refinement Logic.
Class Theorem 1. For all lists of formulas 
and 
and for all formulas 
if 
by a Modified Block Tableau of Smullyan (called also Gentzen tableau), then 
in Refinement Logic where 
is 
.
Proof: We use induction on the depth of the Tableau proof, and we show how to simulate each Tableau proof step by a Refinement Logic step.
Base case: Suppose that 
is of depth 1. Then it must be an axiom, i.e. some 
is the same as 
, as in 
We need to show 
, i.e. 
The method is very direct, we use the appropriate 
rule and a Refinement axiom. In the example we use
by right
by axiom.
It might be necessary to arrange such that the goal is of the right form, say arranging 
into 
This can be done using the associative and commutative properties of 
as lemmas. So we need lemmas of the form
and
.
These are simple to prove in Refinement Logic.
Induction case: Assume that for all 
and all Tableau deductions of depth 
of 
, we can find a Refinement Logic proof of 
. We show that we can convert a Tableau proof of depth 
. We proceed by cases on the first rule used in the Tableau proof. We show how to simulate each Tableau rule application by a Refinement Rule.
(subcase of 
The first rule of 
is 
, so the deduction is essentially
We must show 
in 
.
1. 
2. 
By the induction hypothesis applied to subproofs 1 and 2, we can show in
. 
. 
This means that we can prove 
in using its 
rule. To finish the proof we must show 
. We see that this follows from the following implication
which is a simple distributive law which we prove as a lemma-in Refinement Logic, of course!
Note, we did not use Magic.
Now we prove:
by cut 
1. 
by cut Lemma_for
Lemma_for 
use 
on the Lemma, details omitted.
2. 
use the proof by and ,
Note, just as in the base case, we might need to rearrange by associativity and commutativity to place 
at the end.
case continued (subcase of 
)
The first rule of 
is . So, the deduction is
by
1. 
We know by induction that we can prove . 
So in with the same rule, , we prove 
as required.
end of case
We see from the case that the is trivial and that all the Left rule cases will be similar. This simplifies the proof considerably. So we look only at the 
cases and 
.
Suppose the first rule applied is .
We need to prove 
1. 
By the induction hypothesis applied to 1. 
, we have an proof of 
By associativity this is 
case
Suppose the first Tableau rules is 
. Then the proof is:
We try to prove 
By the induction hypothesis, there is an proof of 
, so we can prove 
in . Now we use this lemma mentioned in lecture.
Now just as the case, we cut in this lemma and prove the result.
end of case
case
Suppose that the first Tableau rule is 
Our goal is to prove 
.
If 
contains 
, then this is an instance of 
. In that case we prove 
by Magic.
If 
does not contain , then since is 
, we proceed as in the case of and prove 
By the way, it is sufficient to use this second analysis even in the case of proving 
. Our lemma for shows that we can convert a proof of 
into a proof of 
.
end of case
Qed
Next: About this document