Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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.


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}


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}


\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.

share|improve this question
I can't say I understand the first two rules. The premises in both rules, and the conclusion in rule one have more than one disjunct, and thus are not wffs. For instance, for A v A v D do you mean (A v D) v A or A v (D v A)? I don't see how you can assume these equivalent in proof theory since you can't assume anything about truth values, and disjunction "v" does not automatically associate in all logical systems. For example, disjunction "v" does not associate in any three-valued logic where v goes 0v0=0, 0v.5=0, 0v1=1, .5v0=.5, .5v.5=.5, .5v1=0, 1v0=1, 1v.5=0, 1v1=1. –  Doug Spoonwood Jul 7 '11 at 0:27
The statement "This process can end only with a rule A or with a De Morgan rule." seems to exclude the possibility that the subformula could occur in one of the axioms -- is anything being assumed about the axioms? Or are the axioms given? –  joriki Jul 7 '11 at 0:34
that had, as proper axioms, those closed atomic formulas that he called "correct" and the negations of the closed atomic formula that he called "uncorrect". Since this new language had a lot of features of PA (for example the same individual constant $0$ as PA), the correct formulas are those closed atomic formulas $s=t$ that, when we evaluate $s$ and $t$ according to the usual recursion laws for $+$ and $\cdot$, we obtain the same "value" for $s$ and $t$. For example, a correct formula is the following: $$0''\cdot 0'' + 0'' = 0'''\cdot 0''$$ –  lie.teller Jul 7 '11 at 3:17
@ Doug: Yes, right observation. Parentheses are eliminated by left association i.e. $(((a \vee b) \vee c) \vee d)$ is $a \vee b \vee c \vee d$. I don't know much about many valued logics, but obviously at the moment we can consider it a purely syntactic calculus, and this one was originally made to be interpreted on usual bivalent logic. @ joriki: I believe you can take the axioms as given. A bit of history: this calculus was set to give a proof of the consistency of FO arithmetic. Schutte gave the definition of a new language (not entirely formalizable as FOL) –  lie.teller Jul 7 '11 at 3:17
@lie.teller: You're a new user, so it is quite understandable that you're not familiar with how this site works; I will explain. What you had posted before was an answer to your question, not a comment - we want to separate those things out, so I deleted your post from the answer area and converted it to the two comments above. In the future, to add a comment, click the "add comment" button on the lower left of the list of comments so far (it is in light grey text). Also, you had created a second account when you posted your answer; I merged it into the account you used to ask the question. –  Zev Chonoles Jul 7 '11 at 5:40
show 2 more comments

1 Answer

up vote 1 down vote accepted

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$.

share|improve this answer
add comment

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

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