- #1

CGandC

- 326

- 34

1. Correctness

2. That it halts

But there are also algorithms/procedures that never halt and are indeed counted as proofs ,for example:

**Theorem:**For every infinite set there exists a countable subset.

**Proof:**

Assume the axiom of choice and let ## A## be an arbitrary infinite set. Perform the following procedure to find a countable subset:

1. Pick an arbitrary element from ## A## , denote it ## a_ 0 ##.

2. Pick an arbitrary element from ## A\setminus \{a_0\}## , denote it ## a_ 1 ##.

3. Pick an arbitrary element from ## A\setminus \{a_0,a_1\}## , denote it ## a_ 2 ##.

4. Continue like-so.

The procedure constructs a set ## \{ a_0 , a_1 , a_2 , \ldots \} = \{ a_i \}_{i\in \mathbb{N} } ## which is a countable subset of ## A ##. Q.E.D.

**Questions :**

1. The algorithm in the proof of the theorem above is correct ( under axiom of choice ) but never halts; if so, can it still be counted as a proof for the theorem? ( because from my knowledge an algorithm must also terminate )

2. When proving something how to know if it’s permissible to give a correct algorithm that never halts?