natural deduction

(redirected from Deductive logic)
Also found in: Dictionary, Wikipedia.

natural deduction

A set of rules expressing how valid proofs may be constructed in predicate logic.

In the traditional notation, a horizontal line separates premises (above) from conclusions (below). Vertical ellipsis (dots) stand for a series of applications of the rules. "T" is the constant "true" and "F" is the constant "false" (sometimes written with a LaTeX \perp).

"^" is the AND (conjunction) operator, "v" is the inclusive OR (disjunction) operator and "/" is NOT (negation or complement, normally written with a LaTeX \neg).

P, Q, P1, P2, etc. stand for propositions such as "Socrates was a man". P[x] is a proposition possibly containing instances of the variable x, e.g. "x can fly".

A proof (a sequence of applications of the rules) may be enclosed in a box. A boxed proof produces conclusions that are only valid given the assumptions made inside the box, however, the proof demonstrates certain relationships which are valid outside the box. For example, the box below labelled "Implication introduction" starts by assuming P, which need not be a true proposition so long as it can be used to derive Q.

Truth introduction:

- T

(Truth is free).

Binary AND introduction:

----------- | . | . | | . | . | | Q1 | Q2 | ----------- Q1 ^ Q2

(If we can derive both Q1 and Q2 then Q1^Q2 is true).

N-ary AND introduction:

---------------- | . | .. | . | | . | .. | . | | Q1 | .. | Qn | ---------------- Q1^..^Qi^..^Qn

Other n-ary rules follow the binary versions similarly.

Quantified AND introduction:

--------- | x . | | . | | Q[x] | --------- For all x . Q[x]

(If we can prove Q for arbitrary x then Q is true for all x).

Falsity elimination:

F - Q

(Falsity opens the floodgates).

OR elimination:

P1 v P2 ----------- | P1 | P2 | | . | . | | . | . | | Q | Q | ----------- Q

(Given P1 v P2, if Q follows from both then Q is true).

Exists elimination:

Exists x . P[x] ----------- | x P[x] | | . | | . | | Q | ----------- Q

(If Q follows from P[x] for arbitrary x and such an x exists then Q is true).

OR introduction 1:

P1 ------- P1 v P2

(If P1 is true then P1 OR anything is true).

OR introduction 2:

P2 ------- P1 v P2

(If P2 is true then anything OR P2 is true). Similar symmetries apply to ^ rules.

Exists introduction:

P[a] ------------- Exists x.P[x]

(If P is true for "a" then it is true for all x).

AND elimination 1:

P1 ^ P2 ------- P1

(If P1 and P2 are true then P1 is true).

For all elimination:

For all x . P[x] ---------------- P[a]

(If P is true for all x then it is true for "a").

For all implication introduction:

----------- | x P[x] | | . | | . | | Q[x] | ----------- For all x . P[x] -> Q[x]

(If Q follows from P for arbitrary x then Q follows from P for all x).

Implication introduction:

----- | P | | . | | . | | Q | ----- P -> Q

(If Q follows from P then P implies Q).

NOT introduction:

----- | P | | . | | . | | F | ----- / P

(If falsity follows from P then P is false).


//P --- P

(If it is not the case that P is not true then P is true).

For all implies exists:

P[a] For all x . P[x] -> Q[x] ------------------------------- Q[a]

(If P is true for given "a" and P implies Q for all x then Q is true for a).

Implication elimination, modus ponens:

P P -> Q ---------- Q

(If P and P implies Q then Q).

NOT elimination, contradiction:

P /P ------ F

(If P is true and P is not true then false is true).
References in periodicals archive ?
But it is when Nashe and Pozzi first enter the home of Flower and Stone that a prior, nonsensical, expanding universe contracts to a mansion of terrifying and deductive logic.
There is nothing we can say to someone who rejects the axioms and inference rules of deductive logic without begging the question.
He observes that, although the utilization of game theory does not lend itself to easy solutions, "it provides a deductive logic for understanding the conditions that facilitate or impede negotiation" (p.
In the epistemological system of medieval philosophy, such experience can neither be found in revelation, nor in the deductive logic of Aristutelian philosophy.
A rule of thumb is neither an inductive theory that explains comprehensively, a deductive logic in individuals that determines choice robustly, nor empirical evidence of individual preferences confirmed in a market during a particular appraisal.
Sniffer MultiSegment Intelligence employs patent-pending algorithms that correlate front-end to back-end transactions, mimicking the deductive logic and thought process typically employed by senior network engineers to solve multifaceted network performance issues.
He describes how to develop a theme, including accepting the irrelevance of most library research, playing by the rules of plagiarism and notation, writing with the criteria for grading in mind, using general principles of good writing, avoiding mistakes of grammar and diction as well as stylistic "infelicities," dancing with language and logic (with a chapters on deductive logic and logic without necessity) and understanding the varieties of philosophy papers and using each variety appropriately.
The least to be inferred from this issue and Peirce's concern about "cognizing a relation" is suggested by Randall Dipert at the end of his contribution, "Peirce's deductive Logic," where he rues "perhaps our worst failing in our appraisal of Peirce's philosophy," namely, "a continuing unwillingness to take up relations not as a privileged historical or even logical subject, but as a philosophical and specifically metaphysical topic.
4 By and large, my remarks are confined to deductive logic.
Even in rare instances in which population inferences might be technically feasible, such inductive inferences are necessarily logically disconnected from the deductive logic of appraisal, unless they can be reasoned to extend from the first principles of appraisal logic.
ClearSupport combines a full text search (FTS) engine with Clarify's deductive logic reasoning system to speed the problem resolution process.
This Allard identifies as first "to defend the legitimacy and usefulness of deductive logic against Mill" and second "to determine the ontological status of the system of knowledge constructed by thought" (p.