0
$\begingroup$

As I understand, a derivable rule of inference is supposed to be eliminable and admissible (though eliminability implies admissiblity).

Definition: Let $\mathcal{S}$ be a formal system. The rule $$\frac{\Gamma}{C}$$ is a derivable rule in $\mathcal{S}$ iff $\Gamma \vdash_{\mathcal{S}} C$.

Source of the definition:

  1. https://www.irif.fr/~roziere/admiss/mscs93.pdf See definition 1.2.1
  2. http://www.few.vu.nl/~cgr600/linkedfiles/abstract_csl03.pdf See second line.

Other definitions:

  1. $\Gamma \vdash_\mathcal{S} C$ means there is a proof of $C$ from $\Gamma$ in $\mathcal{S}$.
  2. For definition of a proof I'm using the one on wikipedia:

    A formal proof or derivation is a finite sequence of sentences (called well-formed formulas in the case of a formal language), each of which is an axiom, an assumption, or follows from the preceding sentences in the sequence by a rule of inference.

Let's say $\mathcal{S}$ is classical propositional logic. And we want to add this derivable rule (actually a rule schema):

$$\frac{A \wedge \neg B}{\neg (A \to B)}$$

Now I can use the following derivation to satisfy the definition:

Derivation

Questions:

  1. The formulas in the above derivation mix metavariables and symbols of the object language. The formal system only defines the notion of a derivation at the object language level (each line must be a wff of object language). How could it be used at the meta level to derive the rule schema (each line is not a wff of the object language as it contains metavariables)? Isn't this a problem with the above definition?

  2. How would we show that this definition of a derivable rule satisfies the criteria of eliminability? I'm guessing we'd need a notion of transforming a derivation with derivable rules into a derivation with only primitive rules, and using it to prove the theorem:

    Let $\mathcal{S}$ be a formal system and $\mathcal{S}^+$ be $\mathcal{S}$ augmented with derivable rules. Then $\Gamma \vdash_{\mathcal{S}^+} \phi$ implies $\Gamma \vdash_{\mathcal{S}} \phi$.

    How do I do this?

    Also this theorem is what shows eliminability implies admissibility.

$\endgroup$
  • $\begingroup$ "The formulas in the above derivation mix metavariables and symbols of the object language" Why ? You can express ND rules as schemas. $\endgroup$ – Mauro ALLEGRANZA Apr 13 at 9:26
  • $\begingroup$ @MauroALLEGRANZA But schemas are supposed to be statements in the metalaguage, and their metavariables are supposed to be replaced with wffs from object language. In the case of the derivation above, the metavariables in the inference rules (used to justify proof steps) are replaced by other metavariables. No? $\endgroup$ – stranger Apr 13 at 9:33
  • $\begingroup$ @MauroALLEGRANZA I added some more explanation to question 1 about what I mean. $\endgroup$ – stranger Apr 13 at 9:38
  • 1
    $\begingroup$ The definition of derivation is obviously expressed in the meta-language: what else ? See e.g. Chiswell & Hodges page 7 : a sequent is an expression $(Γ \vdash ψ)$, and so on... $\endgroup$ – Mauro ALLEGRANZA Apr 13 at 9:43
  • $\begingroup$ An inference rule is expressed in the meta-language: it is an "instruction" how to manage formulas (i.e. expressions of the object language). We can easily express them using only natural language: "In a derivation whatever, from every a pair of formulas occurring into the derivation we can derive a new formula written with the first formula followed by the simbol for conjunction followed by the second formula". It is quite natural the benefits of using meta-variables (schematic letters). $\endgroup$ – Mauro ALLEGRANZA Apr 13 at 12:46
1
$\begingroup$

Note to self: The "rule" here is defined as only composed of WFFs of $\mathcal{S}$. Am I right here?

  1. Technically, the theorem you proved using the derivation in the question is:

    All rules of the form $$\frac{A \wedge \neg B}{\neg (A \to B)}$$ (where $A,B$ are any WFF in $\mathcal{S}$) are derivable in $\mathcal{S}$.

The derivation in the question then serves as the "template proof" for the derivability of all instances of the rule schema; substitute any WFF on all meta-variables in that proof, and you get a formal derivation (as defined) of a rule.

Regarding Rob Arthan's comment on "metavariables v. object variables isn't really relevant...", you can work with propositional logic/s without any rule schema EXCEPT the substitution rule schema $\frac{A}{A[p\mapsto B]}$ where $A,B$ are any WFF, $p$ is an atomic proposition, and $A[p\mapsto B]$ means "The WFF after replacing every $p$ in $A$ by $B$." This means that atomic propositions themselves can be replaced by any WFF. This rule schema makes meta-variables and object variables(atomic propositions) "the same".

  1. EDIT: Your idea of "transforming" the derivation is correct. Just look on the definition of proof: that it is a finite sequence of WFFs. When the proof of $\Gamma \vdash_{\mathcal{S}^+} \phi$ requires derivable rules, for all lines of proof wherein any derivable rule is used, insert between the premises WFFs and the conclusion WFF, the "middle" lines (i.e. the lines that are not the premises and the conclusion) of the proof of derivability of that derivable rule.
$\endgroup$
  • $\begingroup$ Thanks. Regarding your question: "The "rule" here is defined as only composed of WFFs of $\mathcal{S}$. Am I right here?" Yes that is what I meant. Regarding question 2, I understand it intuitively, I just needed help defining the notion of eliminability and showing derivable rules (as defined) are eliminable. $\endgroup$ – stranger Apr 14 at 7:23
  • $\begingroup$ continued... I was thinking for eliminability, we'd define it as: Any sequent provable in the augmented formal system is also provable in the primitive formal system. $\endgroup$ – stranger Apr 14 at 7:36
  • $\begingroup$ continued... To show a derivable rule is eliminable then, we would have to show in any proof step where it is used, that line can be replaced with a derivation using only primitive rules. This last step is where I'm having issues. $\endgroup$ – stranger Apr 14 at 7:44
  • $\begingroup$ I edited my answer (for question 2). The meanings of "rule" and "proof" still apply. $\endgroup$ – Poypoyan Apr 14 at 8:40

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.