4
$\begingroup$

like very much this site.

Let's consider the following rules of a deduction system (due to Sch\"{u}tte). I'll write them all, but some of them may not be useful.


WEAK RULES

Rule 1: \begin{equation} \frac{C \vee A \vee B \vee D}{C \vee B \vee A \vee D} \end{equation}

Rule 2: \begin{equation} \frac{A \vee A \vee D}{A \vee D} \end{equation}

STRONG RULES

rule A: \begin{equation} \frac{D}{A \vee D}\quad\text{(where $A$ is a closed wff)} \end{equation}

De Morgan rule: \begin{equation} \frac{\neg A \vee D \quad \neg B\vee D}{\neg(A \vee B)\vee D} \end{equation}

Negation: \begin{equation} \frac{A \vee D }{\neg\neg A \vee D} \end{equation}

Quantification: \begin{equation} \frac{\neg A(t)\vee D}{(\neg(x)A(x))\vee D} \end{equation}

Infinite Induction: \begin{equation} \frac{A(\bar{n}) \vee D\quad \text{for all natural numbers n}}{((x)A(x))\vee D} \quad \text{($\bar{n}$ is a numeral)} \end{equation}

CUT RULE

\begin{equation} \frac{C \vee A \quad \neg A\vee D}{C \vee D} \end{equation}

Formulas C and D are called auxiliary formulas. We can remove them (except in rule A) obtaining other instances of the rules.


I need to prove that from a proof of a formula that is a consequence of some premises using one of those rules (for example De Morgan rule), it is possible to obtain a proof of the premises. The proof in question is obtained by working on the original one. There is a description of how it is done, but I don't understand it. I'll try to explain.

Suppose that a formula $A$ is obtained by DeMorgan rule and then it is of the form $\neg(B \vee E) \vee D$. Taking a proof of $A$, we can consider all the subformulas $\neg(B \vee E)$ of the proof tree obtained starting with $\neg(B \vee E)$ in $A$ and climbing back along the proof tree. (Here it is not clear to me what is the real meaning.) This process (what process?) continues through the weak rules used and through the strong rules used in which $\neg(B \vee E)$ is a subformula of an auxiliary wff. This process can end only with a rule A or with a De Morgan rule. The set of all occurrencies of $\neg(B \vee E)$ is called \emph{history} of $\neg(B \vee E)$. Now replace all the occurrencies of $\neg(B \vee E)$ in its history with $\neg B$. Then we obtain another proof tree (after removing all those formulas that are not necessary) whose terminal formula is just $\neg B \vee D$ (that is, one of the premises in De Morgan rule). Substitution with $\neg E$ yields a proof of $\neg E \vee D$ (the other premise).

What method we precisely use to build that new proof tree? Can you show me an example of how to prove premises for De Morgan rule using the method described above?

Thank you very much.

  • 0
    @lie.teller The following seems purely an aside, but perhaps you'll find it interesting. If you "translate" formulas involving just one logical operation like a v b v ... v n, under that convention into prefix notation, the formula consists of a sequence of n instances of that operation, followed by a sequence of n+1 logical variables (in other words, the formula has two consecutive substrings... the first of only operation symbols, and the second of only variables). In suffix notation we have one variable, followed by a pattern alternating between a variable symbol and an operation symbol.2011-07-08

1 Answers 1

1

I'm assuming that the last long paragraph in the question is, except for your insertions in parentheses, something you quoted and are trying to understand. (If so, I suggest you make that explicit to make the question easier to understand.)

From your comments, it seems that the axioms are only atomic formulas and negated atomic formulas, i.e. they don't contain any logical connectives. In that case the quoted paragraph makes sense, though it skips over some non-trivial details. The idea is that in a proof tree of a formula of the form $\neg(B \vee E) \vee D$, the subformula $\neg(B \vee E)$ must have originated from an application of either rule A or the De Morgan rule.

It cannot have originated from one of the axioms, since the axioms don't contain logical connectives. So let's go through the rules and check which ones might produce the subformula $\neg(B \vee E)$ if it wasn't already in one of the premises. These are precisely the strong rules; the weak rules and the cut rule only remove subformulas.

Now, going through the rules again, we find that there is no rule that reduces the number of quantifiers or negations in front of a subformula. That means that the subformula $\neg(B \vee E)$ cannot have been derived from a formula where it was preceded by a quantifier or additional negations. But that means that it cannot have been produced by the negation, quantification or infinite induction rules, since each of these can only produce something where $\neg(B \vee E)$ would be preceded by at least one quantifier or additional negation.

That leaves only rule A and the De Morgan rule by which $\neg(B \vee E)$ could have been introduced into the proof tree. But in both cases, we can replace $\neg(B \vee E)$ by $\neg B$ or by $\neg E$; in the case of rule A because we can introduce any $A$ we like, and in the case of the De Morgan rule because that turns the conclusion into one of the two premises.

Summing up, if we modify the proof tree by replacing all occurrences of $\neg(B \vee E)$ by $\neg B$, it will still be a valid proof tree, but now it will be a proof tree for $\neg B \lor D$ (and the same for $\neg E$ and $\neg B \lor E$). Thus, any proof of $\neg(B \vee E) \vee D$ can be used to produce proofs of both $\neg B \vee D$ and $\neg E \vee D$.