First-order natural deduction

principles are the same:


Natural deduction: validity

checking entailment A ⊧ B

same as validity of A → B


Validity in first-order logic

F valid if true in all models and interpretations

interpretation = evaluation of the variables

therefore:

free variables are as if they were universally quantified

Semantics

rules for introducing and eliminating quantifiers

follows from the semantics of natural deduction:

P1∧…∧Pn A1∧…∧Am F
premises active
assumpt.

(a formula in a proof is a consequence of the premises and of the assumptions of the boxes the formula is in)


Rules


Eliminating universal quantifiers

∀x A (∀E) where t is a term
A[t/x]

Introducing universal quantifiers

A[y/x] (∀I) where y is a variable not occurring free in the premises and in the active assumptions
∀x A

why the condition on y?


Condition on y: why?

for simplicity, assume x=y

violating the rule: more on this later


Why y/x?

y could also occur quantified in A

A[y/x] means: precondition is A where x is replaced by y

conclusion ∀x A is on x


Introducing existential quantifiers

A[t/x] (∃I)
∃x A

obvious: if A is true for some terms t, there exists a value making it true


Eliminating existential quantifiers

∃x A
A[y/x]
C
(∃E) where y does not occur free in C, in the premises and in the active assumptions
C

if A is true for some value,
and for an arbitrary value A entails C,
then C holds


Why the rule on y?

before: ∀y ( P1∧…∧Am → ∃xA ∧ (A[y/x]→C) )

if y satisfies the condition then
P1∧…∧Am → ∃xA ∧ ∀ y (A[y/x]→C) )

now ∃xA ∧ ∀ y (A[y/x]→C) entails C


Example

∀x(P(x)→Q(x))∧P(c) ⊧ Q(c)


Example (1)


Example (2)

take first of a conjunction


Example (3)

take second of conjunction


Example (4)

from universal to a specific term


Example (5)

modus ponens

claim proved:
∀x(P(x)→Q(x))∧P(c) ⊧ Q(c)


Counterexample

violating the rule for (∀I):

∃xP(x)
P(x)
∀xP(x)
assumption
(∀I)
∀xP(x) (∃E)

but ∃ does not imply ∀
(∃x P(x) does not entail ∀x P(x))

mistake was: we assumed P(x) true, that is, P true for x

never assumed that P was always true


First example

prove inconsistency of:

{ ∃x P(x)∧Q(x), ∀x ¬P(x) }


First example (1)


First example (2)


First example (3)


First example (4)


First example (5)


First example (6)


First example (7)

claim proved: inconsistency of
{ ∃x P(x)∧Q(x), ∀x ¬P(x) }


Second example

prove the following entailment:

{ ∀x∀y P(x,y), ∃x P(x,x)→Q(x,x) } ⊧ ∃x Q(x,x)


Second example (1)


Second example (2)


Second example (3)


Second example (4)


Second example (5)


Second example (6)


Second example (7)

claim proved:
{ ∀x∀y P(x,y), ∃x P(x,x)→Q(x,x) } ⊧ ∃x Q(x,x)


Third example

{ P(a,a), ∀x∀y(P(x,x)→Q(y,x)), ∃y ¬Q(y,y) } ⊧ ∃y Q(y,y)


Third example: solution


Fourth example

{ ∀(P(x,a)→P(a,x)), P(b,a), } ⊧ ∃x P(a,x)


Fourth example: solution