11

You are correct, there is an error in that paper, and the rule should indeed read: $$\frac{\Gamma\vdash M:\Delta}{\Gamma\vdash M\cong M} $$ the use of jugements of this style for equality (sometimes called "typed equality") originates already in Martin-Löf, I think (see here for example). It's often replaced with an untyped operational definition in modern ...


5

There is a paper by Beyersdorff and Chew on the proof complexity of calculi for non-monotonic logic. In the references of this paper you will find links to the papers where these calculi are defined.


4

The fact that a system is complete for proving valid formulas without the cut rule doesn't mean you can derive the cut rule from other rules. In fact it is not difficult to construct counter-examples. Consider $\Rightarrow A \rightarrow B$ and $\Rightarrow A$. From these assumptions it would follow that $\Rightarrow B$. But you cannot derive it without ...


3

Yes, backtracking in focused proof search may be necessary due to a wrong choice of focus formula. Consider the provable sequent $$\vdash p\otimes q, (p^\bot\mathrel{\wp} q^\bot)\otimes r, r^\bot.$$ Choosing to focus on $p\otimes q$ leads to a dead end, because however you "split" the context you end up with an atom ($p$ or $q$) without matching ...


2

Showing that from two cut-free derivations $\Gamma \vdash A$ and $\Gamma, A \vdash C$ you can produce a cut-free derivation of $\Gamma \vdash C$ is called cut admissibility. Admissibility of cut is actually equivalent to showing that cut can be eliminated. If you have cut-elimination, you just cut the two derivations together and then eliminate the cut. On ...


Only top voted, non community-wiki answers of a minimum length are eligible