Texas Puzzle

"One of Peirce's favorite examples... even if it perhaps be not perfectly politically correct: Every [Ork] kills some [Ork]; no [Ork] is killed by more than one [Ork]; therefore every [Ork] is killed by some [Ork]. The argument's conclusion follows validly only if the set of [Orks] is finite."

--"Charles Sanders Peirce," Stanford Encyclopedia of Philosophy

Here, we formalize and prove this theorem.

THEOREM

*******

ALL(t):ALL(v):[Set(t)

& ALL(a):[a e t => v(a) e t]

& ALL(a):ALL(b):[a e t & b e t => [v(a)=v(b) => a=b]]

=> [Finite(t)=> ALL(b):[b e t => EXIST(c):[c e t & v(c)=b]]]]

This formal proof was written and machine-verified using the author's DC Proof 2.0 freeware available at http://www.dcproof.com

Dan Christensen

2021-05-30

Define: Finite (from R. Dedekind)

1 ALL(a):[Set(a) => [Finite(a)

<=> ALL(f):[ALL(b):[b e a => f(b) e a]

& ALL(b):ALL(c):[b e a & c e a => [f(b)=f(c) => b=c]]

=> ALL(b):[b e a => EXIST(c):[c e a & f(c)=b]]]]]

Axiom

Let t be the set of Orks, and v be a function on t such that v(x) is the victim of x.

2 Set(t)

& ALL(a):[a e t => v(a) e t]

& ALL(a):ALL(b):[a e t & b e t => [v(a)=v(b) => a=b]]

Premise

3 Set(t)

Split, 2

"Every Ork kills some Ork."

Here, Peirce almost certainly did NOT mean "a least one Ork" but "only one," thus a functional relation.

4 ALL(a):[a e t => v(a) e t]

Split, 2

"No Ork is killed by more than one Ork."

The function v is injective.

5 ALL(a):ALL(b):[a e t & b e t => [v(a)=v(b) => a=b]]

Split, 2

Suppose there is a finite number of Orks.

6 Finite(t)

Premise

Apply the definition of Finite

7 Set(t) => [Finite(t)

<=> ALL(f):[ALL(b):[b e t => f(b) e t]