Natural deduction

deduction method: from A infer B

not a refutation method like DPLL and tableau

Components

• inference rules
• assumptions

second point explained later

Some inference rules

some of the rules (not all):

name of rules in parenthesis

An example (without assumptions)

prove that x∧y ⊧ y∧(x∨z)

method:

start with x∧y

use the rules to obtain y∧(x∨z)

Example (1)

start from the premise

Example (2)

rule used:

Example (3)

rule used:

Example (4)

rule:

Example (5)

rule:

Example: completed proof

proves that first formula implies last

in this case: x∧y ⊧ y∧(x∨z)

Note on the example

• proof is always a line, not a tree
• some rules break formulae (like in the tableau method) but
  some others build formulae from subformulae

Natural deduction

(still no assumptions: later)

rules

all in the form:

formula, … , formula

formula

inference

to prove A₁, … , A_n ⊧ B

• place preconditions in a line:

  	A1
  	⋮
  	An

• if there is a rule like

  formula, … , formula

  formula

  and formula, … , formula are all in the line
  add formula at the bottom
• if B is obtained, proof is successful

Rules (most of them)

Rules: comments

most of them either Introduce a connective or Eliminates it

rule for entailment introduction (→I) still missing

Example

x, ¬¬(y ∧ z) ⊧ ¬¬x ∧ z

Example (1)

Example (2)

Example (3)

Example (4)

Example (5)

Example (6)

completed proof:

x, ¬¬(y ∧ z) ⊧ ¬¬x ∧ z holds

Example: comments

• start with premises
• add formulae according to rules
  rules are valid: only consequences are generated
• works by generating consequences

Example

x→(y→z), x, ¬z ⊧ ¬y

Example (1)

Example (2)

Example (3)

statement proved

Assumptions

main point of natural deduction

idea: like in human reasoning

• assume that some formulae are true
• infer other formulae from assumptions
• these are consequences of assumptions

Assumptions, formally

• assume that some arbitrary formula A is true
• obtain whatever formula B using the rules
• this proves A→B

is a way to obtain A→B
(the missing entailment-introduction rule)

Assumption rule

entailment introduction

meaning:

• assume A
• if B follows…
• … A→B holds

Use of assumptions (1)

at any point, open a box with an arbitrary formula A

Use of assumptions (2)

use A to generate whatever formula (as usual)

Use of assumptions (3)

at any point, close the box

Use of assumptions (4)

entailment first→last results

Use of assumptions (5)

continue as usual

Assumption: which formula?

the assumption A can be an arbitrary formula

how to choose it?

chose a formula A such that A→B could be useful

Example (with assumptions)

¬x→¬y ⊧ y→¬¬x

Example (1)

Example (2)

an arbitrary formula can be assumed

Example (3)

inference from the assumption
(in this case: introduce double negation)

Example (4)

inference can be done using both formulae in the box and outside it
(some caveat later)

Example (5)

closure of boxes can be done at any point

Example (6)

from box to entailment, using (→I)

Example (7)

claim proved: ¬x→¬y ⊧ y→¬¬x holds

Assumption: semantics

formulae outside the box are consequences of the premise (¬x→¬y)

formulae in the box are consequences of both the premise (¬x→¬y) and the assumption (y)

Semantics of formulae in a proof

each formula is a consequence of the premises and, if it is in a box, of the assumption of the box

natural deduction works by keeping this condition true

Condition: consequences

every step keeps the condition true

premises

they are consequences of them, so they can be written in the proof

inferred formulae

they are consequences of the premises or of other consequences of the premises

assumption

according to the rule, has to be a consequence of the premises and the assumption
the latter is itself

formulae in the box

obtained by inference from the premises and the assumption

closing the box

formula A→B is a consequence of the premise and not of A
(more on next slide)

Closing a box

according to the condition, E is a consequence of the premises and of the assumption:

P₁∧…∧P_n∧A ⊧ E

therefore:

P₁∧…∧P_n ⊧ A→E

A→E is a consequence of the premises
(can be written outside the box)

Valid and invalid steps (1)

correct inference:

• B→C consequence of the premises
• B is a consequence of the premise and the assumption A
• therefore, C is a consequence of the premises and the assumption A

writing B in the box does not violate the condition

Valid and invalid steps (2)

incorrect inference:

• B∧C consequence of the premises and the assumption
• C is a consequence of B∧C
• therefore, C is a consequence of the premises and the assumption
• cannot be written outside the box

to maintain the condition:

write outside the box only formulae that are consequences only of the premises

Violation of condition: example

x→y, y→z ⊧ z

clearly false

could be proved by natural deduction, if condition is violated

Violation of condition: wrong inference

all correct up to this point

use formula in the box to generate formula outside

allows incorrectly infer z from x→y and y→z

A correct example (1)

x→y, y→z ⊧ x→z

A correct example (2)

A correct example (3)

A correct example (4)

A correct example (5)

A correct example (6)

A correct example (7)

claim x→y, y→z ⊧ x→z proved

Another example (1)

x→(y→z) ⊧ (x∧y)→z

Another example (2)

Another example (3)

Another example (4)

Another example (5)

Another example (6)

Another example (7)

Another example (8)

Another example (9)

claim proved: x→(y→z) ⊧ (x∧y)→z holds

(note: assumption x∧y chosen for a reason;
more on this later)

Nested boxes

inference inside a box is like outside
follows the same rules

including: open a box, close a box

semantics?

Semantics of nested boxes

• A and B are consequences of premises and A
• C, D and E are consequences of premises, A and C

more generally: consequences of premises and all assumptions of boxes still open

Condition on formulae

the condition generalizes as:

each formula is a consequence of the premises and all assumptions of the boxes it is in

Effects of condition

• a formula in a box cannot be used to generate a formula outside that box
• it can be used to generate a formula in the same box, or in a box within
• formulae of closed boxes cannot be used any longer
• once a box is closed, it can only be used as a whole with (→I)
  (rule (→I) is: from box infer A→B)

Nested boxes: example (1)

x∧y→z ⊧ x→(y→z)

Nested boxes: example (2)

Nested boxes: example (3)

Nested boxes: example (4)

Nested boxes: example (5)

Nested boxes: example (6)

Nested boxes: example (7)

Nested boxes: example (8)

Nested boxes: example (9)

claim proved: x∧y→z ⊧ x→(y→z) holds

How to proceed

• to obtain a formula, introduce its connectives
• use (∨I), (∧I), (¬I), (→I) to do so
• (→I) requires a box:
  use the precondition of the formula to obtain as the assumption
• use (∨E), (∧E), (¬E), (→E) only to get formulae that are needed for the previous points

policy?

Method

natural deduction does not specify a policy of application of the rules

⇓

hard to automate

Assumptions

assumptions are arbitrary formulae

possible to keep introducing useless assumptions

(these assumptions are useless to prove (x∧¬y)→z)

Natural deductions: variants

different rules, same mechanism

Natural deduction, in general

• proof=sequence of formulae
• rules for obtaining new formulae from existing ones
• assumptions can be made
• what is obtained using an assumption is consequence of that assumption
• some rules allow inferring something when an assumption is retracted