17:29
@ParamanandSingh Chat again soon! Sorry I was away for a bit just now.
@ParamanandSingh The example that always comes to my mind is the compactness theorem for FOL, which is not only non-constructive but necessarily so. Two interesting facts that show this are:
(1) Compactness trivially yields a non-standard model of PA, but there is no computable non-standard model of PA, so the compactness argument cannot have a computable witness!
(2) There is a computable infinite binary tree (i.e. a computable set S of finite binary strings closed under prefixes) with no computable infinite path (i.e. binary string whose finite prefixes are all in S), despite the fact that the same argument to prove compactness for countable FOL theories also proves that there is in fact an infinite path.
So in some sense compactness for even countable FOL theories is truly non-constructive.
Worse is when it is applied to uncountable theories, which I cannot get my mind around. I can mentally grasp countable iterations, but I cannot grasp uncountably long iterations...