Appendix C Quick reference

C.1 Characteristic truth tables

𝒜 ¬𝒜
T F
F T
𝒜 𝒜 𝒜 𝒜 𝒜
T T T T T T
T F F T F F
F T F T T F
F F F F T T

C.2 Symbolization

Sentential Connectives
It is not the case that P ¬P
Either P or Q (PQ)
Neither P nor Q ¬(PQ) or  (¬P¬Q)
Both P and Q (PQ)
If P then Q (PQ)
P only if Q (PQ)
P if and only if Q (PQ)
P unless Q (¬QP) or (PQ)
Predicates
All Fs are Gs x(F(x)G(x))
Some Fs are Gs x(F(x)G(x))
Not all Fs are Gs ¬x(F(x)G(x)) or
x(F(x)¬G(x))
No Fs are Gs x(F(x)¬G(x)) or
¬x(F(x)G(x))
Only Fs are Gs x(G(x)F(x))
¬x(¬F(x)G(x))
Identity
Only c is G x(G(x)x=c)
Everything other
than c is G x(¬x=cG(x))
Everything
except c is G x(¬x=cG(x))
The F is G x(F(x)y(F(y)x=y)G(x))
It is not the case
that the F is G ¬x(F(x)y(F(y)x=y)G(x))
The F is non-G x(F(x)y(F(y)x=y)¬G(x))

C.3 Using identity to symbolize quantities

There are at least blank  Fs.

one xF(x)
two x1x2(F(x1)F(x2)¬x1=x2)
three x1x2x3(F(x1)F(x2)F(x3)¬x1=x2¬x1=x3¬x2=x3)
four x1x2x3x4(F(x1)F(x2)F(x3)F(x4)¬x1=x2¬x1=x3¬x1=x4¬x2=x3¬x2=x4¬x3=x4)
n x1xn(F(x1)F(xn)¬x1=x2¬xn1=xn)

There are at most blank  Fs.

One way to say ‘there are at most n Fs’ is to put a negation sign in front of the symbolization for ‘there are at least n+1 Fs’. Equivalently, we can offer:

one x1x2[(F(x1)F(x2))x1=x2]
two x1x2x3[(F(x1)F(x2)F(x3))(x1=x2x1=x3x2=x3)]
three x1x2x3x4[(F(x1)F(x2)F(x3)F(x4))(x1=x2x1=x3x1=x4x2=x3x2=x4x3=x4)]
n x1xn+1[(F(x1)F(xn+1))(x1=x2xn=xn+1)]

There are exactly blank  Fs.

One way to say ‘there are exactly n Fs’ is to conjoin two of the symbolizations above and say ‘there are at least n Fs and there are at most n Fs.’ The following equivalent formulas are shorter:

zero x¬F(x)
one x[F(x)y(F(y)x=y)]
two x1x2[F(x1)F(x2)¬x1=x2y(F(y)(y=x1y=x2))]
three x1x2x3[F(x1)F(x2)F(x3)¬x1=x2¬x1=x3¬x2=x3y(F(y)(y=x1y=x2y=x3))]
n x1xn[F(x1)F(xn)¬x1=x2¬xn1=xny(F(y)(y=x1y=xn))]

C.4 Basic deduction rules for TFL

Reiteration

Line number

Subproof level

Formula

Justification

m

0
𝒜

0
𝒜
R m

Conjunction

Line number

Subproof level

Formula

Justification

m

0
𝒜

n

0

0
𝒜
I m, n

Line number

Subproof level

Formula

Justification

m

0
𝒜

0
𝒜
E m

Line number

Subproof level

Formula

Justification

m

0
𝒜

0
E m

Conditional

Line number

Subproof level

Formula

Justification

m

open subproof, 1
𝒜
AS

n

1

close subproof, 0
𝒜
I mn

Line number

Subproof level

Formula

Justification

m

0
𝒜

n

0
𝒜

0
E m, n

Negation

Line number

Subproof level

Formula

Justification

m

open subproof, 1
𝒜
AS

n

1

close subproof, 0
¬𝒜
¬I mn

Line number

Subproof level

Formula

Justification

m

0
¬𝒜

n

0
𝒜

0
¬E m, n

Indirect proof

Line number

Subproof level

Formula

Justification

i

open subproof, 1
¬𝒜
AS

j

1

close subproof, 0
𝒜
IP ij

Explosion

Line number

Subproof level

Formula

Justification

m

0

0
𝒜
X m

Disjunction

Line number

Subproof level

Formula

Justification

m

0
𝒜

0
𝒜
I m

Line number

Subproof level

Formula

Justification

m

0
𝒜

0
𝒜
I m

Line number

Subproof level

Formula

Justification

m

0
𝒜

i

open subproof, 1
𝒜
AS

j

1
𝒞

k

close subproof, open subproof, 1
AS

l

1
𝒞

close subproof, 0
𝒞
E m, ij, kl

Biconditional

Line number

Subproof level

Formula

Justification

i

open subproof, 1
𝒜
AS

j

1

k

close subproof, open subproof, 1
AS

l

1
𝒜

close subproof, 0
𝒜
I ij, kl

Line number

Subproof level

Formula

Justification

m

0
𝒜

n

0
𝒜

0
E m, n

Line number

Subproof level

Formula

Justification

m

0
𝒜

n

0

0
𝒜
E m, n

C.5 Derived rules for TFL

Disjunctive syllogism

Line number

Subproof level

Formula

Justification

m

0
𝒜

n

0
¬𝒜

0
DS m, n

Line number

Subproof level

Formula

Justification

m

0
𝒜

n

0
¬

0
𝒜
DS m, n

Modus Tollens

Line number

Subproof level

Formula

Justification

m

0
𝒜

n

0
¬

0
¬𝒜
MT m, n

Double-negation elimination

Line number

Subproof level

Formula

Justification

m

0
¬¬𝒜

0
𝒜
DNE m

Excluded middle

Line number

Subproof level

Formula

Justification

i

open subproof, 1
𝒜
AS

j

1

k

close subproof, open subproof, 1
¬𝒜
AS

l

1

close subproof, 0
LEM ij, kl

De Morgan Rules

Line number

Subproof level

Formula

Justification

m

0
¬(𝒜)

0
¬𝒜¬
DeM m

Line number

Subproof level

Formula

Justification

m

0
¬𝒜¬

0
¬(𝒜)
DeM m

Line number

Subproof level

Formula

Justification

m

0
¬(𝒜)

0
¬𝒜¬
DeM m

Line number

Subproof level

Formula

Justification

m

0
¬𝒜¬

0
¬(𝒜)
DeM m

C.6 Basic deduction rules for FOL

Universal elimination

Line number

Subproof level

Formula

Justification

m

0
𝓍𝒜(𝓍𝓍)

0
𝒜(𝒸𝒸)
E m

Universal introduction

Line number

Subproof level

Formula

Justification

m

0
𝒜(𝒸𝒸)

0
𝓍𝒜(𝓍𝓍)
I m

𝒸 must not occur in any undischarged assumption

Existential introduction

Line number

Subproof level

Formula

Justification

m

0
𝒜(𝒸𝒸)

0
𝓍𝒜(𝓍𝒸)
I m

Existential elimination

Line number

Subproof level

Formula

Justification

m

0
𝓍𝒜(𝓍𝓍)

i

open subproof, 1
𝒜(𝒸𝒸)
AS

j

1

close subproof, 0
E m, ij

𝒸 must not occur in any undischarged assumption, in 𝓍𝒜(𝓍𝓍), or in

Identity introduction

Line number

Subproof level

Formula

Justification

0
𝒸=𝒸
=I

Identity elimination

Line number

Subproof level

Formula

Justification

m

0
𝒶=𝒷

n

0
𝒜(𝒶𝒶)

0
𝒜(𝒷𝒶)
=E m, n

Line number

Subproof level

Formula

Justification

m

0
𝒶=𝒷

n

0
𝒜(𝒷𝒷)

0
𝒜(𝒶𝒷)
=E m, n

C.7 Derived rules for FOL

Line number

Subproof level

Formula

Justification

m

0
𝓍¬𝒜

0
¬𝓍𝒜
CQ m

Line number

Subproof level

Formula

Justification

m

0
¬𝓍𝒜

0
𝓍¬𝒜
CQ m

Line number

Subproof level

Formula

Justification

m

0
𝓍¬𝒜

0
¬𝓍𝒜
CQ m

Line number

Subproof level

Formula

Justification

m

0
¬𝓍𝒜

0
𝓍¬𝒜
CQ m

C.8 Rules for the use of subproofs and citations

To cite an individual line when applying a rule:

  1. 1.

    the line must come before the line where the rule is applied, but

  2. 2.

    not occur within a subproof that has been closed before the line where the rule is applied.

To cite a subproof when applying a rule:

  1. 1.

    the cited subproof must come entirely before the application of the rule where it is cited,

  2. 2.

    the cited subproof must not lie within some other closed subproof which is closed at the line it is cited, and

  3. 3.

    the last line of the cited subproof must not occur inside a nested subproof.

C.9 Rules for chains of equivalences

¬¬𝒫 𝒫 (DN)
(𝒫𝒬) (¬𝒫𝒬) (Cond)
¬(𝒫𝒬) (𝒫¬𝒬)
(𝒫𝒬) ((𝒫𝒬)(𝒬𝒫)) (Bicond)
¬(𝒫𝒬) (¬𝒫¬𝒬) (DeM)
¬(𝒫𝒬) (¬𝒫¬𝒬)
(𝒫𝒬) (𝒬𝒫) (Comm)
(𝒫𝒬) (𝒬𝒫)
(𝒫(𝒬)) ((𝒫𝒬)(𝒫)) (Dist)
(𝒫(𝒬)) ((𝒫𝒬)(𝒫))
(𝒫(𝒬)) ((𝒫𝒬)) (Assoc)
(𝒫(𝒬)) ((𝒫𝒬))
(𝒫𝒫) 𝒫 (Id)
(𝒫𝒫) 𝒫
(𝒫(𝒫𝒬)) 𝒫 (Abs)
(𝒫(𝒫𝒬)) 𝒫
(𝒫(𝒬¬𝒬)) 𝒫 (Simp)
(𝒫(𝒬¬𝒬)) 𝒫
(𝒫(𝒬¬𝒬)) (𝒬¬𝒬)
(𝒫(𝒬¬𝒬)) (𝒬¬𝒬)