Definition talk:Natural Deduction

From ProofWiki
Jump to navigation Jump to search

I am looking for ways to rewrite this page in a more rigorous, yet as structured way. Am I correct in putting that the natural deduction system relies on the concept of WFFs with pooled assumptions, using only as an axiom the rule of assumption (in the form (coming down to) $p \vdash p$), treating the rest as rules of inference? That would allow me to present the stuff in a more uniform way while practically not altering the content. You have to agree that $p, (p \vdash q) \vdash q$ is hardly to be called an axiom, at best it is an impredicative (i.e., self-relying, circular) schema. --Lord_Farin 22:20, 27 June 2012 (UTC)

The rules of natural deduction as they stand were presented in the work I got them from as a set of axioms. Now I know there are other systems which use considerably less axioms than those, and there *is* a one-axiom system, but it's far more complicated an axiom than that one. Suspect we may need to do a similar job to Natural Numbers and set up a series of axiom systems: the existing 10-ish axioms; the 3 axioms as presented by Hamilton (which I think originates with Meredith), and perhaps go back through the history to Russell and whoever. --prime mover 10:26, 28 June 2012 (UTC)
Generally the other systems you talk about (I've dealt with them in a course on proof theory) use the amount of axioms you mention, ánd the "Rule of Detachment", Modus Ponendo Ponens. It is generally vital, in order to be able to derive simpler statements from more complicated ones.
I just wrote down what I think is the rigorous version of natural deduction as currently presented. It consists of 1 axiom and 12 rules of inference (note that IPC follows if the last axiom, Double Negation Elimination, is dropped). Besides covering the different systems, we ought to specify the various ways to denote them; I imagine there's months of work here, but we can take a break when all the stuff currently up is covered.
Concerning the source, I have a digital copy so I can verify that my new presentation respects it as far as it can. I feel obliged to stress that both 'axioms' and 'rules of inference' in the formal system are in fact (what we generally consider to be) axioms if we take a position outside the system itself. The only difference between them is that an 'axiom' is expressible in the formal language, while a 'rule of inference' needs a metalanguage. That is, an 'axiom' generally consists of symbols, and a 'rule of inference' generally needs words (or a symbol like $\leadsto$, which happens to have a nice name but apparently doesn't render as it does on my compiler). --Lord_Farin 10:54, 28 June 2012 (UTC)
It is noteworthy that the twelve rules of inference I wrote down correspond exactly to the 'basic rules of natural deduction' of Huth, but I managed to find a way to present them in a more vertically compressed manner. An example: $\lor I_1: P \vdash p \leadsto P \vdash p \lor q$ where $P$ is a pool of assumptions, $p$ and $q$ are WFFs. Of course, I will use appropriate wording to explain this string of symbols. But first, lunch. --Lord_Farin 10:59, 28 June 2012 (UTC)
We still want to keep the notation as used by Huth in addition to the compressed version you came up with, of course.
At this level of analysis I can't see the difference between an "axiom" and a "rule of inference". In this context they are both "statements which can not be derived from other statements in this system". So whether (for example) the "Rule of Conjuction" (or "law" I misremember) is called a rule or an axiom matters not. The fact is, it stands alone outside the system and arises from "natural intuition" and, unless some work is done to explain what the difference is between an axiom and such a rule (I can't tell) I recommend we merge the distinctions. --prime mover 11:31, 28 June 2012 (UTC)
I must agree that there is hardly any distinction. Maybe I formulated it wrong, and should $p \implies p$ be the genuine axiom (in the sense that it is a WFF accepted to be true) and $p \vdash p$ be simply another rule of inference. But the distinction isn't very valuable in any case, so we'd better drop it indeed.
The two-dimensional presentation Huth gives (before reverting to the more writer-friendly tableau notation) is of considerable importance and should be preserved. I was hoping to replace things like $p, (p \vdash q) \vdash q$ with my new schematics, but you may postpone your verdict until I am finished here. I am just getting ready for a nice application of the eqn template again. --Lord_Farin 11:40, 28 June 2012 (UTC)
Just to muddy the waters: $p \vdash p$ and $p \implies p$ are not axiomatic in the Huth system - they are derived. From what I understand. --prime mover 11:56, 28 June 2012 (UTC)

They are derived, from some loosely formulated thing coming down to 'you may write down a premise and call it a tableau proof' principle which is captured precisely by $p \vdash p$. I consider it a syntactical detail.

Just to give you a taste of what I'm brewing on:

\(\text {(\mathrm{ND}:\land \mathcal I)}: \quad\) \(\ds \begin{align} P &\vdash p \\ Q &\vdash q \end{align}\) \(\, \Large\leadsto \,\) \(\ds P, Q \vdash p \land q\) Rule of Conjunction

I hope you like it; don't worry, there is a section 'Notation' in which I explain everything. This will (I think) just be a summary for the main page, something like what is up now being put on the 'Axioms' subpage. --Lord_Farin 12:04, 28 June 2012 (UTC)

So, what do you think of the result (note the curly braces I added for optimal readability)? --Lord_Farin 12:33, 28 June 2012 (UTC)

On a side note, what do you think of this:
$p \mathop \Longrightarrow q$
$p \mathop{\, \Longrightarrow \,} q$
$p \implies q$
The contrast is rather huge, I'd almost consider to overrule the definition of '\implies' in our MathJax config to save space. --Lord_Farin 12:40, 28 June 2012 (UTC)
\implies every time, and that gap is supposed to be there from what I understand from the designers of LaTeX etc. because you *want* a nice big gap in this context. Besides, I refuse to countenance changing a sweet simple "\implies to an filthily unwieldy "\mathop(\, \Longrightarrow \,}" on the grounds that the latter has so much wrong we would have to invent a whole new definition for the category of "incorrect". --prime mover 16:33, 28 June 2012 (UTC)
You have a point there, please note the 'almost' in my sentence. But in fact the MathJax configuration file could have a line like:
\renewcommand{\implies}{\mathop{\, \Longrightarrow \,}}
which allows to reap the benefits of both forms. --Lord_Farin 16:57, 28 June 2012 (UTC)
By the way, I take it that you not reverting all my edits on Natural Deduction means you approve of the new form? --Lord_Farin 17:00, 28 June 2012 (UTC)
Give me a chance, some of us have a day job, you know.
... it's all right I suppose, I expect I'll get used to it. --prime mover 18:30, 28 June 2012 (UTC)
I don't see "\mathop{\, \Longrightarrow \,}" as worth a damn. "\implies" as it stands, with a good big gap either side is fine. We do not need to redefine it. --prime mover 18:27, 28 June 2012 (UTC)

Apologies if I pressed on too much; the holiday mood struck, I suppose. Oh, and let's bury those suggestions about $\implies$. --Lord_Farin 21:11, 28 June 2012 (UTC)


I discovered after a lot of trial and error that I will need to rewrite the axiom pages and Definition:Proof Rule, as well as Definition:Tableau Proof (Natural Deduction) (the latter to a lesser extent, probably only adding stuff) to accommodate for the desired rigour and to allow for describing other methods of notation (eg. 'marked proof trees') in a more structural way. Hopefully, this will not offend you; I'm quite sure (as I will ensure that the tableau proof currently up remain correct) that this will not damage the references' validity. If it does offend (however unlikely) please tell me in advance. A tasting is at Rule of Assumption which needed some adaptation. --Lord_Farin 14:34, 29 June 2012 (UTC)

Set notation

There's some vague wordage about the use or non-use of set notation. When I originally contrived the structure of this site, I was conscious of the fact that the Zermelo-Fraenkel axioms include as part of their definition the concept of a "propositional function". The latter can be defined in terms of symbolic logic, but the latter needs to be defined at the most basic level possible, explicitly without using the language of set theory. This partly explains the non-mathematical and to an extent clumsy language in which this whole field was originally defined. Once we have established the basics of propositional logic (not PropCalc, that is) to a sufficient extent (which incidentally requires that "propositional function" itself is defined without recourse to a set-theoretical definition. Hope this makes sense and doesn't cause too much of a headache. --prime mover 12:58, 4 July 2012 (UTC)

There is no problem here; the set notation occurs in sequents, which are not part of propositional logic or PropCalc. They are mere phrasings of allowed cq. valid deductions in Natural Deduction. This does not in any way (in principle at least) interfere with the introduction of propositional, relation and/or function symbols. Simply put, a sequent is not a set, nor does it contain one; it's a notation. If such matters concern you, I think we have no choice but to pass to sequent calculus (see WP) which defines a much more unwieldy notation, which allows to more easily circumvent such possible circularity concerns... --Lord_Farin 13:40, 4 July 2012 (UTC)