Is an algorithm for a proof required to halt?

[CGandC]

I know that when giving an algorithm to prove something we need to prove two things about the algorithm ( there’s another option which is to show time-complexity but that’s optional since it’s irrelevant to the proof):
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?

 

[fresh_42]

There is a fundamental difference between a proof and an algorithm. An algorithm has to halt, since otherwise, it is useless and makes no difference to not having an algorithm at all.

Our standard logical system in mathematics (there are others for which the following is not true) includes three ways to obtain a conclusion that cannot be constructed per algorithm (at least I currently can't remember more than these three):

a) indirect proof (pretend otherwise)
b) induction (pretend we go on forever)
c) axiom of choice (pretend we can choose)

They all pretend something, i.e. include an additional truth that hasn't been proven. We accept (within this standard first order predicate logic) that FALSE cannot follow from TRUE, that AND SO ON is a valid argument since we could theoretically do exactly this, and finally and most disputed argument, that A COLLECTIO OF NON-EMPTY BASKETS IS NON-EMPTY.

The principles b) and c) do not really belong to the logical system we use. b) is basically the Peano axiom, and c) is a convenience. We cannot really pick an irrational number between two given rational numbers. We just assume that non-empty times non-empty no matter how often cannot be empty.

If you really want to doubt some of these three principles, I suggest reading about constructivism in mathematics and other logical systems.

 

[CGandC]

There is a fundamental difference between a proof and an algorithm. An algorithm has to halt, since otherwise, it is useless and makes no difference to not having an algorithm at all.

Our standard logical system in mathematics (there are others for which the following is not true) includes three ways to obtain a conclusion that cannot be constructed per algorithm (at least I currently can't remember more than these three):

a) indirect proof (pretend otherwise)
b) induction (pretend we go on forever)
c) axiom of choice (pretend we can choose)

They all pretend something, i.e. include an additional truth that hasn't been proven. We accept (within this standard first order predicate logic) that FALSE cannot follow from TRUE, that AND SO ON is a valid argument since we could theoretically do exactly this, and finally and most disputed argument, that A COLLECTIO OF NON-EMPTY BASKETS IS NON-EMPTY.

The principles b) and c) do not really belong to the logical system we use. b) is basically the Peano axiom, and c) is a convenience. We cannot really pick an irrational number between two given rational numbers. We just assume that non-empty times non-empty no matter how often cannot be empty.

If you really want to doubt some of these three principles, I suggest reading about constructivism in mathematics and other logical systems.

Thanks a lot!
So the procedure I gave is not an algorithm ( since it does not halt ) but part of a permissible proof within standard first order predicate logic because we can obtain conclusion TRUE follows TRUE, for example, by induction, which is not constructible by an algorithm? ( regardless of whether it halts or not, in this case it doesn't )

 

[fresh_42]

Thanks a lot!
So the procedure I gave is not an algorithm ( since it does not halt ) but part of a permissible proof within standard first order predicate logic because we can obtain conclusion TRUE follows TRUE, for example, by induction, which is not constructible by an algorithm? ( regardless of whether it halts or not, in this case it doesn't )

It is part of the mathematical rules we gave us. The axiom of choice is not part of the logical system but part of standard mathematics. However, there is a considerable number of mathematicians who do not accept it. Constructivism indeed requires algorithms that come to a halt in order to prove existence.

But I am no expert in constructivism, so I don't know whether it allows induction. However, induction is the formalism of and so on, and proofs by induction can at least be implemented as an algorithm. Therefore we have a reduction to an indirect proof:

Give me a counterexample and I can show you that it is none by performing the induction step long enough. Thus there won't be any counterexample at all. It is true because you won't ever find an example where it is not true. And I can prove that.

The axiom of choice is different. There is not even an algorithm in most cases (halting or not).

Seems, that constructivism doesn't even allow indirect proofs:
https://en.wikipedia.org/wiki/Constructivism_(philosophy_of_mathematics)