# rzach/forallx-yyc forked from OpenLogicProject/forallx-cam

changed some examples, all I's to we's, shall's to will's

 @@ -1,7 +1,7 @@ %!TEX root = forallxyyc.tex \chapter{Alternative proof systems} -In formulating my natural deduction system, I treated certain rules of natural deduction as \emph{basic}, and others as \emph{derived}. However, I could equally well have taken various different rules as basic or derived. I shall illustrate this point by considering some alternative treatments of disjunction, negation, and the quantifiers. I shall also explain why I have made the choices that I have. +In formulating our natural deduction system, we treated certain rules of natural deduction as \emph{basic}, and others as \emph{derived}. However, we could equally well have taken various different rules as basic or derived. We will illustrate this point by considering some alternative treatments of disjunction, negation, and the quantifiers. We will also explain why we have made the choices that we have. \section{Alternative disjunction elimination} @@ -35,7 +35,7 @@ \section{Alternative disjunction elimination} \close \have{con}{\meta{C}}\tnd{c-c1, nc-c3} \end{proof} -So why did I choose to take $\eor$E as basic, rather than DS?\footnote{P.D.\ Magnus's original version of this book went the other way.} My reasoning is that DS involves the use of $\enot$' in the statement of the rule. It is in some sense cleaner' for our disjunction elimination rule to avoid mentioning \emph{other} connectives. +So why did we choose to take $\eor$E as basic, rather than DS?\footnote{P.D.\ Magnus's original version of this book went the other way.} Our reasoning is that DS involves the use of $\enot$' in the statement of the rule. It is in some sense cleaner' for our disjunction elimination rule to avoid mentioning \emph{other} connectives. \section{Alternative negation rules} @@ -59,11 +59,11 @@ \section{Alternative negation rules} \end{proof} Using these two rules, we could have derived all of the rules governing negation and contradiction that we have taken as basic (i.e.\ $\ered$I, $\ered$E, $\enot$I and TND). Indeed, we could have avoided all use of the symbol $\ered$' altogether. Negation would have had a single introduction and elimination rule, and would have behaved much more like the other connectives. -The resulting system would have had fewer rules than ours. So why did I chose to separate out contradiction, and to use an explicit rule TND?\footnote{Again, P.D.\ Magnus's original version of this book went the other way.} +The resulting system would have had fewer rules than ours. So why did we chose to separate out contradiction, and to use an explicit rule TND?\footnote{Again, P.D.\ Magnus's original version of this book went the other way.} -My first reason is that adding the symbol $\ered$' to our natural deduction system makes proofs considerably easier to work with. +Our first reason is that adding the symbol $\ered$' to our natural deduction system makes proofs considerably easier to work with. -My second reason is that a lot of fascinating philosophical discussion has focussed on the acceptability or otherwise of \emph{tertium non datur} (i.e.\ TND) and \emph{ex falso quodlibet} (i.e.\ $\ered$E). By treating these as separate rules in the proof system, we will be in a better position to engage with that philosophical discussion. In particular: having invoked these rules explicitly, it will be much easier for us to know what a system which lacked these rules would look like. +Our second reason is that a lot of fascinating philosophical discussion has focussed on the acceptability or otherwise of \emph{tertium non datur} (i.e.\ TND) and \emph{ex falso quodlibet} (i.e.\ $\ered$E). By treating these as separate rules in the proof system, we will be in a better position to engage with that philosophical discussion. In particular: having invoked these rules explicitly, it will be much easier for us to know what a system which lacked these rules would look like. @@ -119,8 +119,8 @@ \section{Alternative quantification rules} Armed with these derived rules, we could now go on to derive the two remaining CQ rules, exactly as in \S\ref{s:DerivedFOL}. -So, why did I start with all of the quantifier rules as basic, and then derive the CQ rules? +So, why did we start with all of the quantifier rules as basic, and then derive the CQ rules? -My first reason is that it seems more intuitive to treat the quantifiers as on a par with one another, giving them their own basic rules for introduction and elimination. +Our first reason is that it seems more intuitive to treat the quantifiers as on a par with one another, giving them their own basic rules for introduction and elimination. -My second reason relates to the discussion of alternative negation rules. In the derivations of the rules of $\exists$I and $\exists$E that I have offered in this section, I invoked DNE. This is a derived rule, whose derivation essentially depends upon the use of TND. But, as I mentioned earlier, TND is a contentious rule. So, if we want to move to a system which abandons TND, but which still allows us to use existential quantifiers, we shall want to take the introduction and elimination rules for the quantifiers as basic, and take the CQ rules as derived. (Indeed, in a system without TND, we shall be \emph{unable} to derive the CQ rule which moves from $\enot \forall \meta{x} \meta{A}$ to $\exists \meta{x} \enot \meta{A}$.) +Our second reason relates to the discussion of alternative negation rules. In the derivations of the rules of $\exists$I and $\exists$E that we have offered in this section, we invoked DNE. This is a derived rule, whose derivation essentially depends upon the use of TND. But, as we mentioned earlier, TND is a contentious rule. So, if we want to move to a system which abandons TND, but which still allows us to use existential quantifiers, we will want to take the introduction and elimination rules for the quantifiers as basic, and take the CQ rules as derived. (Indeed, in a system without TND, we will be \emph{unable} to derive the CQ rule which moves from $\enot \forall \meta{x} \meta{A}$ to $\exists \meta{x} \enot \meta{A}$.)