Negation rules in natural deductive systems

This question concerns the block of text at the bottom, which is from Teller's Logic Primer, Chapter 5 (page 72).

(I must mention that there is a rule called Negation Introduction. It says that when given a premise $X$ if we can derive both $Y$ and $\neg Y$, than we can introduce $\neg X$.)

First of all, what does the author mean by "if you restrict yourself to the rule "$X$. Therefore $\neg \neg X$ for negation introduction"? Does it mean "if we substitute our previous rule for negation introduction with this one" or it means "if we add this rule to our system"?

Second of all, when is a system of natural deduction complete? Is it when given a set of premises we can, using the rules, derive all possible conclusions with which the argument will be valid?

Third of all, why can't I construct the argument that he presents as an example from $\neg A$? Given $\neg A$ I use Distinction Introduction rule to derive $\neg A \lor \neg B$ and then I use De Morgan's law to convert it to $\neg (A \land B)$. Or we can't use De Morgan's laws in natural deductive systems?

What does the author mean by "if you restrict yourself to the rule "$X$. Therefore $\neg \neg X$ for negation introduction"? Does it mean "if we substitute our previous rule for negation introduction with this one" or it means "if we add this rule to our system"?

I think he means your first option, from the two negation 'rules', you keep only $X \therefore \neg \neg X$. You end up with all the other rules you have so far, plus $X \therefore \neg \neg X$ and not $\neg \neg X \therefore X$. But even if he means your second option, nothing changes as the rule $\neg \neg X\therefore X$ is irrelevant to the example and to the rest of this answer.

Why can't I construct the argument that he presents as an example from $\neg A$? Given $\neg A$ I use Distinction Introduction rule to derive $\neg A \lor \neg B$ and then I use De Morgan's law to convert it to $\neg (A \land B)$. Or we can't use De Morgan's laws in natural deductive systems?

You can't use De Morgan's laws without proving them (or in the text's terminology, without deriving them) and to prove them you need a rule which you don't have yet, namely that if from a premise $P$ you derive contradiction (denoted by $\bot$), you can infer $\neg P$. This rule is what will end up being the negation introduction rule in your system. Without this rule the example given can't be proven, nor can De Morgan's laws. A formal proof of the example, informally, goes something like this: $\neg A$ is a premise. Assume $A\land B$, by $\land\text{-Elim}$ infer $A$. From the premise and from $A$ deduce $\bot$. (It was proved that from $A\land B$ one derives $\bot$). Therefore by $\neg\text{-Introduction}$ one concludes $\neg (A\land B)$.

When is a system of natural deduction complete? Is it when given a set of premises we can, using the rules, derive all possible conclusions with which the argument will be valid?

Suppose you have only one of the typical deduction rules, say $\lor\text{-Elim}$. Then, given some premises, what would you call "all possible conclusions"? I'd say all possible conclusions are exactly the ones you can deduce from $\lor\text{-Elim}$. But this isn't what is meant when it is said that the system complete.

Given a statement, say $A\land B$, you have a notion of truth about it. Sometimes it is true, sometimes it isn't, (this is called a contingency, by the way). Contingencies aren't provable in your system (without premises) because they aren't always true.

A formal system is said to be complete, if whenever the premises are all true entails that the conclusion is true, then the conclusion can be proved from the premises (and deduction rules). For example, consider a tautology, for instance $\neg A\lor A$ (it doesn't really matter what tautology it is). Since this statement is always true, a complete system will ensure that you can prove $\neg A\lor A$ from an empty set of premises. In the given example, a complete system will allow you to deduce $\neg (A\land B)$ from $\neg A$, because whenever $\neg A$ is true, so is $\neg (A\land B)$.

In case you aren't aware, a statement is said to be true if it is true in the sense of the truth tables. It is said to prove provable if you can infer it using the deduction rules. A complete system says that any true statement is provable. This isn't always the case, in fact, in $\sf ZFC$, where most mathematics is done, we don't have completeness, see the incompleteness theorem.

• Question: Are you counting an axiom as a premise here? Also, as a note, there's a certain inelegance of language here. It does come as possible to have a single axiom along with a single rule of inference and still have a complete system. May 23, 2014 at 0:37
• @DougSpoonwood No, I am not. Thank you for a very good point. I will fix that part. May 23, 2014 at 0:40
• It's worth noting that there are two notions of completeness that come up in this context. When one theorem seems to be a negation of another, you really have to wonder whether this is an effective choice of terminology. May 23, 2014 at 11:03
• Comment, down voter? May 17, 2015 at 10:18

He means your second option, from the two negation 'rules', you keep only $X \therefore \neg \neg X$. You end up with all the other rules you have so far, plus $X \therefore \neg \neg X$ and not $\neg \neg X \therefore X$.

This I don’t understand. It seems to me Teller means the first option, namely imagine that we keep the Neg Elim rule $\neg \neg X \therefore X$ but for Neg Intro we use $X \therefore \neg \neg X$, instead of the rule that if from $X$ we can derive both $Y$ and $\neg Y$, than we can introduce $\neg X$. Teller's point is that if we go this route, then we then don't end up with "all the other rules." We come up short.

You can't use De Morgan's laws without proving them and to prove them you need a rule which you don't have yet, namely that if from a premise $P$ you derive contradiction (denoted by $\bot$), you can infer $\neg P$. This rule is what will end up being the negation introduction rule in your system. Without this rule the example given can't be proven, nor can De Morgan's laws.

To be clear: you do in fact have this rule; it’s that rule about introducing $\neg X$ by deriving both $Y$ and $\neg Y$ from $X$. And with that rule you can get the De Morgan laws, and once you’ve derived them you can use them freely. But if, with Teller, we suppose that you’ve replaced that rule with $X \therefore \neg \neg X$, then you can’t derive the De Morgan laws.

Maybe a simple way to see the issue is to note that if your Negation rules are $X \therefore \neg \neg X$ and $\neg \neg X \therefore X$, then you can only introduce or eliminate $\neg$'s two at a time. It's as if all you have is two rules for a connective written "$\neg\neg$," but no rule for $\neg$.

• In the first point you mean the OP's second option. It is me who means the first. I misread the OP's question. May 23, 2014 at 0:53