Transcript Formal Proofs and Quantifiers

Language, Proof and
Logic
Formal Proofs and Quantifiers
Chapter 13
13.1
 Elim:
Universal quantifier rules
x
t
c
--- variable
--- constant term (variable-free term)
--- constant which does not occur outside
the subproof where it is introduced
P(x), Q(x) --- any wffs only containing x free
P(c), Q(c) --- the results of replacing in
P(x), Q(x) all free occurrences
of x by c
P(t) --- the results of replacing in P(x) all
free occurrences of x by t
xP(x)
…
P(t)
 Intro (General Cond. Proof):
c P(c)
…
Q(c)
x[P(x)Q(x)]
 Intro (Universal introduct.):
c
…
Q(c)
xQ(x)
You try it, pp. 353, 354 [Universal 1-2]
13.2
Existential quantifier rules
 Intro:
 Elim:
P(t)
…
xP(x)
…
c P(c)
…
Q
Q
xP(x)
x --- variable
t --- constant term (variable-free term)
c --- constant which does not occur outside the subproof where it is introduced
P(x) --- any wff only containing x free
P(c) --- the results of replacing in P(x) all free occurrences of x by c
P(t) --- the results of replacing in P(x) all free occurrences of x by t
You try it, pp. 358 [Existential 1]
13.3.a
Strategy and tactics
General tips:
1. Always be clear about the meaning of the sentences you are using.
Practically zero chance to succeed without that!
2. A good strategy is to find an informal proof and then try to formalize
it.
3. Working backwards can be very useful in proving universal claims.
You typically use  Intro in these cases.
4. Working backwards ( Intro) is not useful in proving an existential
claim xS(x) unless you can think of a particular instance S(c) of the
claim that follows from the premises.
5. If you get stuck, consider using proof by contradiction.
13.3.b
Strategy and tactics
x[Tet(x)Small(x)]
x[Small(x)LeftOf(x,b)]
xLeftOf(x,b)
Informal proof:
Look, Bozo, we are told that
there is a small tetrahedron.
So we know that it is small,
right? But we’re also told that
anything that’s small is left of
b. So if it’s small, it’s got to
be left of b, too. So, something
is left of b, namely, the small
tetrahedron.
You try it, p.366 [Quantifier Strategy 1]
Formal proof:
1. x[Tet(x)  Small(x)]
2. x[Small(x)  LeftOf(x,b)]
3.
c Tet(c)  Small(c)
4.
5.
6.
7.
Small(c)
Small(c)  LeftOf(c,b)]
LeftOf(c,b)
xLeftOf(x,b)
8. xLeftOf(x,b)
 Elim: 3
 Elim: 2
 Elim: 4,5
 Inro: 6
 Elim: 1, 3-7
13.4
Soundness and completeness
As in the propositional case, we have:
Q is provable in Fitch from premises P1,…, Pn
if (completeness) and only if (soundness)
Q is a FO consequence of P1,…, Pn