User:Lord Farin/Archive/Natural Deduction Axioms
General note
The below page is a copy of the revision 96983 of Definition:Natural Deduction, accessible here.
Definition
Natural deduction is a proof system for propositional logic.
As such, it consists of certain axioms, which together constitute a collection of theorems.
This can be specified as follows.
Work In Progress In particular: The inevitable subpages You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by completing it. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{WIP}} from the code. |
Notation
To indicate that a collection of WFFs $P$, the pool of assumptions, entails a particular WFF $p$, the conclusion, we agree to write a sequent:
- $P \vdash p$
To make exposition more natural, we also agree to omit the brackets of explicit set definition and use commas in a suggestive way, so that:
- $p, q \vdash p \land q$
- $P, Q \vdash p \land q$
- $P, p \vdash q$
are used instead of the formally more correct:
- $\left\{{p, q}\right\} \vdash p \land q$
- $P \cup Q \vdash p \land q$
- $P \cup \left\{{p}\right\} \vdash q$
Furthermore, in the last expression it is implicitly understood that $p \notin P$.
The $\Large\leadsto$ symbol indicates that given the sequent(s) on the left-hand side, the sequent on the right-hand side may be inferred.
Axioms
Natural deduction has the following twelve axioms, explained in more detail on their own pages:
\(\text {(\mathrm{ND}:\mathrm A)}: \quad\) | \(\ds \) | \(\) | \(\ds q \vdash q\) | Rule of Assumption | ||||||||||
\(\text {(\mathrm{ND}:\lor \mathcal I_1)}: \quad\) | \(\ds P \vdash p\) | \(\, \Large\leadsto \,\) | \(\ds P \vdash p \lor q\) | Rule of Addition | ||||||||||
\(\text {(\mathrm{ND}:\lor \mathcal I_2)}: \quad\) | \(\ds P \vdash q\) | \(\, \Large\leadsto \,\) | \(\ds P \vdash p \lor q\) | Rule of Addition | ||||||||||
\(\text {(\mathrm{ND}:\lor \mathcal E)}: \quad\) | \(\ds \left.{ \begin{align} P &\vdash p \lor q \\ Q, p &\vdash r \\ R, q &\vdash r \end{align} }\right\}\) | \(\, \Large\leadsto \,\) | \(\ds P, Q, R \vdash r\) | Proof by Cases | ||||||||||
\(\text {(\mathrm{ND}:\land \mathcal I)}: \quad\) | \(\ds \left.{ \begin{align} P &\vdash p \\ Q &\vdash q \end{align} }\right\}\) | \(\, \Large\leadsto \,\) | \(\ds P, Q \vdash p \land q\) | Rule of Conjunction | ||||||||||
\(\text {(\mathrm{ND}:\land \mathcal E_1)}: \quad\) | \(\ds P \vdash p \land q\) | \(\, \Large\leadsto \,\) | \(\ds P \vdash p\) | Rule of Simplification | ||||||||||
\(\text {(\mathrm{ND}:\land \mathcal E_2)}: \quad\) | \(\ds P \vdash p \land q\) | \(\, \Large\leadsto \,\) | \(\ds P \vdash q\) | Rule of Simplification | ||||||||||
\(\text {(\mathrm{ND}:\implies \mathcal I)}: \quad\) | \(\ds P, p \vdash q\) | \(\, \Large\leadsto \,\) | \(\ds P \vdash p \implies q\) | Rule of Implication | ||||||||||
\(\text {(\mathrm{ND}:\implies \mathcal E)}: \quad\) | \(\ds \left.{ \begin{align} P &\vdash p \implies q \\ Q &\vdash p \end{align} }\right\}\) | \(\, \Large\leadsto \,\) | \(\ds P, Q \vdash q\) | Modus Ponendo Ponens | ||||||||||
\(\text {(\mathrm{ND}:\neg \mathcal I)}: \quad\) | \(\ds P, p \vdash \bot\) | \(\, \Large\leadsto \,\) | \(\ds P \vdash \neg p\) | Proof by Contradiction | ||||||||||
\(\text {(\mathrm{ND}:\neg \mathcal E)}: \quad\) | \(\ds \left.{ \begin{align} P &\vdash p \\ Q &\vdash \neg p \end{align} }\right\}\) | \(\, \Large\leadsto \,\) | \(\ds P, Q \vdash \bot\) | Principle of Non-Contradiction | ||||||||||
\(\text {(\mathrm{ND}:\bot \mathcal E)}: \quad\) | \(\ds P \vdash \bot\) | \(\, \Large\leadsto \,\) | \(\ds P \vdash p\) | Rule of Explosion |
This article is complete as far as it goes, but it could do with expansion. In particular: extend background; this page may become a disambig if many similar systems are covered later on. Transclusion would make it too long to read You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by adding this information. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{Expand}} from the code.If you would welcome a second opinion as to whether your work is correct, add a call to {{Proofread}} the page. |
Theorems
The theorems of natural deduction are those WFFs $p$ allowing a sequent $\vdash p$, i.e., that may be derived with an empty pool of assumptions.
Proofs
Although it is satisfying to find a (formal) proof of a theorem using the above rules, it is advisable to cast such a proof in a standard framework.
On ProofWiki, the framework chosen is that of a tableau proof, which most easily lends itself for a MediaWiki architecture.
However, many other notations exist and are used by various authors.
This article is complete as far as it goes, but it could do with expansion. In particular: mention boolean interpretations via soundness/completeness; this is really after the fact, though You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by adding this information. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{Expand}} from the code.If you would welcome a second opinion as to whether your work is correct, add a call to {{Proofread}} the page. |
Also see
There are many other proof systems for propositional logic, see here.
Sources
- 2000: Michael R.A. Huth and Mark D. Ryan: Logic in Computer Science: Modelling and reasoning about systems: $\S 1.2, \ \S 1.2.3$