deduction method: from A infer B
not a refutation method like DPLL and tableau
second point explained later
some of the rules (not all):
|
|
||||||
|
|
name of rules in parenthesis
prove that x∧y ⊧ y∧(x∨z)
method:
start with x∧y
use the rules to obtain y∧(x∨z)
start from the premise
rule used:
A∧B | (∧E1) |
A |
rule used:
A | (∨I1) |
A∨B |
rule:
A∧B | (∧E2) |
B |
rule:
A B | (∧I) |
A∧B |
proves that first formula implies last
in this case: x∧y ⊧ y∧(x∨z)
(still no assumptions: later)
formula, … , formula |
formula |
A1 | |
⋮ | |
An |
formula, … , formula |
formula |
|
|
|
|||||||||
|
|
|
|||||||||
|
|
||||||||||
|
|
|
|||||||||
|
|
||||||||||
|
|
most of them either Introduce a connective or Eliminates it
rule for entailment introduction (→I) still missing
x, ¬¬(y ∧ z) ⊧ ¬¬x ∧ z
completed proof:
x, ¬¬(y ∧ z) ⊧ ¬¬x ∧ z holds
x→(y→z), x, ¬z ⊧ ¬y
statement proved
main point of natural deduction
idea: like in human reasoning
is a way to obtain A→B
(the missing entailment-introduction rule)
entailment introduction
|
(∧I) | ||||
A→B |
meaning:
at any point, open a box with an arbitrary formula A
⋮ | |
|
use A to generate whatever formula (as usual)
⋮ | |||
|
at any point, close the box
⋮ | |||||
|
entailment first→last results
⋮ | |||||
| |||||
A→E |
continue as usual
⋮ | |||||
| |||||
A→E | |||||
⋮ |
the assumption A can be an arbitrary formula
how to choose it?
chose a formula A such that A→B could be useful
¬x→¬y ⊧ y→¬¬x
an arbitrary formula can be assumed
inference from the assumption
(in this case: introduce double negation)
inference can be done using both formulae in the box and outside it
(some caveat later)
closure of boxes can be done at any point
from box to entailment, using (→I)
claim proved: ¬x→¬y ⊧ y→¬¬x holds
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)
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
every step keeps the condition true
P1 | premises | |||||||
⋮ | ||||||||
Pn | ||||||||
⋮ | ||||||||
|
assumption |
according to the condition, E is a consequence of the premises and of the assumption:
P1∧…∧Pn∧A ⊧ E
therefore:
P1∧…∧Pn ⊧ A→E
A→E is a consequence of the premises
(can be written outside the box)
correct inference:
writing B in the box does not violate the condition
incorrect inference:
to maintain the condition:
write outside the box only formulae that are consequences only of the premises
x→y, y→z ⊧ z
clearly false
could be proved by natural deduction, if condition is violated
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
x→y, y→z ⊧ x→z
claim x→y, y→z ⊧ x→z proved
x→(y→z) ⊧ (x∧y)→z
claim proved: x→(y→z) ⊧ (x∧y)→z holds
(note: assumption x∧y chosen for a reason;
more on this later)
inference inside a box is like outside
follows the same rules
including: open a box, close a box
P1 | premises | |||||||||||
⋮ | ||||||||||||
Pn | ||||||||||||
⋮ | ||||||||||||
|
|
semantics?
⋮ | ||||||||||||
|
|
more generally: consequences of premises and all assumptions of boxes still open
the condition generalizes as:
each formula is a consequence of the premises and all assumptions of the boxes it is in
x∧y→z ⊧ x→(y→z)
claim proved: x∧y→z ⊧ x→(y→z) holds
policy?
natural deduction does not specify a policy of application of the rules
⇓
hard to automate
assumptions are arbitrary formulae
possible to keep introducing useless assumptions
(these assumptions are useless to prove (x∧¬y)→z)
different rules, same mechanism
|
|
||||||||||||||||
|
|
||||||||||||||||
uncommon | usual |