Definition talk:Natural Deduction/Derived Rules

I haven't got a copy of Lemmon, does he introduce the stuff in this manner explicitly or does this notation originate from your mind? (That is, may I change it to fit Rule of Assumption without endangering the ref. to Lemmon?) --Lord_Farin 10:46, 9 July 2012 (UTC)

Lemmon's words:

"When we argue, we draw or deduce or derive a conclusion from given premisses; in logic we formulate rules, called rules of derivation, whose object is so to control the activity of deduction as to ensure that the conclusion reached is validly reached. ... Roughly, our procedure in setting out arguments will be as follows. Each step will be marked by a new line, and each line will be numbered consecutively. On each line will appear either an assumption of the argument as a whole or a conclusion drawn from propositions at earlier lines and based on these prepositions as premisses. To the right of each proposition will be stated the rule of derivation used to justify its appearance at that stage and (where necessary) the numbers of the premisses used. To the left of each proposition will appear the numbers of the original assumptions on which the argument at that stage depends."

The structure of the natural deduction proofs as provided by me on this site matches closely Lemmon's presentation. It is completely equivalent to that which Huth and Ryan have provided, but the latter is more graphical in its technique and therefore less amenable to rigorous mathematical verification (despite the prettiness of the Huth & Ryan exposition). Besides, it is far easier to present Lemmon's structure in ProofWiki without lots of unnecessarily complicated (and difficult to maintain) $\LaTeX$ constructions.

Ultimately my motivation behind having created this section in the first place was to provide a more-or-less firm foundation to the Axiom of Replacement (or whichever one of the ZFC it is) in order that the whole thundering aeroplane of mathematics can get off the ground in the first place. As such I did not structure it (and at the time, when ProofWiki was in its infancy, there was no detailed vision of how it would pan out, it was "post stuff up and see what evolves") with a view to presenting alternative metaschemas (which are only just evolving now: see the alternative approaches to deriving the natural numbers etc.).

In short, I believe the Lemmon / Huth approach (what's currently up there) should be left as is, and the approach you are suggesting, if (as I believe) it is considerably different from this, should be added as a second, parallel approach.

In the context of the recent modifications to the axioms of natural deduction, the presentation via Lemmon and Huth & Ryan, where you introduce sets of theorems on the left and right, effectively converting $p \vdash p \lor q$ into $P \vdash p \leadsto P \vdash p \lor q$, it might be pointed out that Lemmon's approach (and indeed, Huth & Ryan's, and in fact all the works I have on this subject) uses the axioms in the first format, e.g. $p \vdash p \lor q$, and from them deduces $P \vdash p \leadsto P \vdash p \lor q$ and so on. IMO the former is "more axiomatic" in that it's simpler. My philosophical position is that it is better to have simple axioms rather than complicated ones. --prime mover 11:17, 9 July 2012 (UTC)

One more thing: it's in the plan to revisit the Lemmon citations with the prev/next technique (as I'm gradually working through my books now) and this will of course also result in a certain amount of restructuring from the point of view of 4 years down the line. --prime mover 11:20, 9 July 2012 (UTC)

It is as if I am finally susceptible to reason and start to see the virtue of the original approach. The problem I seem to be having is that the formal ground is currently present (I had to think for quite a bit to be able to admit that) but it is smeared out over the axioms and the tableau proof technique. This anti-modular approach makes it very hard to plug in new modules (like new sets of axioms or new proof systems) because the sequents, axioms and proofs are intertwined to a point where they seem almost inseparable. Thus, I am, cautiously and slowly, led to the conclusion that there is hardly anything to improve in the natural deduction domain at the moment, without starting from scratch again (which would be an insult to the authors and your countless hours of contributing if it were to replace what is up now). Thus, it may be best to create something like a 'Natural Deduction 2', but then, it is more satisfying and useful to start with a completely different approach at once, one allowing to cover multiple systems with a simple modular approach. I'll think about it; in the mean time, I'll store my work in a safe place and revert to the old version. --Lord_Farin 11:59, 9 July 2012 (UTC)

The smeared-outness is indeed a problem, up to a point. It would be, as I suggested, perfectly appropriate to list the axioms as you envisaged them, but with the caveat that they are not truly "axiomatic", and to indicate the proof, that is the ur-axiom and the general rule of sequent introduction (?), which demonstrates their validity in the original metaschema. But as suggested, I'll leave it up to you to think your way round how you plan to present it. As for me, I will return to this area in due course, once I've rationalised my source works in Abstract Algebra (which, I admit, seems to dominate this site). --prime mover 12:53, 9 July 2012 (UTC)

I'll leave this part of the site for now, and will get cracking on Schilling again. In due time, when I locate appropriate ref's, I will start building a new approach to PropCalc, since this will allow me to implement the stuff with maximal freedom, and most easily conveys the presentation I pursue. --Lord_Farin 13:01, 9 July 2012 (UTC)