Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-22 17:10:47 -0800 (Tue, 22 Nov 2005)
Revision: 8199
Log message:
Working on meta-implies. Still working on the meta_dT tactic.
Questions:
1. We had thought to limit the meta-logic to third order.
We can still do it, but is it worth it?
2. I plan to add the meta-structural rules for
cut, thinning, and copy.
High-level arguments that these are conservative extensions.
cut: prove cut-elimination. For each use of the cut rule
S1 --> ... --> Sn --> R
S1 --> ... --> Sn --> R --> T
-----------------------------
S1 --> ... --> Sn --> T
prove the 2 upper rules as separate theorems.
thinning: state the rule without the thinned assumption
and prove that instead. The unthinned rule follows
trivially.
higher-order rules: reduce an order n inference to
order n-1 by stating the introduction and elimination
rules as separate theorems.
For example, consider the following elimination rule.
S1 --> ... --> Sn --> R1
S1 --> ... --> Sn --> R2 --> T
---------------------------------------
S1 --> ... --> Sn --> (R1 --> R2) --> T
Suppose we have a proof of the lower rule.
For each use of the elimination rule, prove 3
separate theorems.
... --> R1
... --> R1 --> R2
... --> R2 --> T
Also, the proof that teleportation is a conservative extension is
the same. Suppose we proved a theorem without contexts, but
we used teleportation in the argument. For each use of the
teleportation rule on a sequence of hyps of length n,
prove (n + 1) theorems, including the base case and n
step theorems.