principles are the same:
checking entailment A ⊧ B
same as validity of A → B
F valid if true in all models and interpretations
interpretation = evaluation of the variables
therefore:
free variables are as if they were universally quantified
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)
∀x A | (∀E) | where t is a term | |
A[t/x] |
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?
for simplicity, assume x=y
violating the rule: more on this later
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
A[t/x] | (∃I) | ||
∃x A |
obvious: if A is true for some terms t, there exists a value making it true
|
(∃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
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
∀x(P(x)→Q(x))∧P(c) ⊧ Q(c)
take first of a conjunction
take second of conjunction
from universal to a specific term
modus ponens
claim proved:
∀x(P(x)→Q(x))∧P(c) ⊧ Q(c)
violating the rule for (∀I):
∃xP(x) | ||||||
|
|
|||||
∀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
prove inconsistency of:
{ ∃x P(x)∧Q(x), ∀x ¬P(x) }
claim proved: inconsistency of
{
∃x P(x)∧Q(x),
∀x ¬P(x)
}
prove the following entailment:
{ ∀x∀y P(x,y), ∃x P(x,x)→Q(x,x) } ⊧ ∃x Q(x,x)
claim proved:
{
∀x∀y P(x,y),
∃x P(x,x)→Q(x,x)
} ⊧
∃x Q(x,x)
{ P(a,a), ∀x∀y(P(x,x)→Q(y,x)), ∃y ¬Q(y,y) } ⊧ ∃y Q(y,y)
{ ∀(P(x,a)→P(a,x)), P(b,a), } ⊧ ∃x P(a,x)