Equivalence of sequences and subsets of natural numbers

Question

For me, facts like the independence of the continuum hypotheses from ZFC cast a doubt on the "law of the excluded middle". (In this context, the doubt is that there might be no "final set theory" such that every proposition about sets is either true or false.) Now I'm looking for simpler (mathematical) examples that are easier to understand, but still cast a similar doubt on the "law of the excluded middle" (or on another law of the three classical laws of thought). Right now, I think that recursion theory (also known as computability theory) might teach me the sort of examples I'm looking for (at least I can appreciate the difference between primitive recursive functions and $\mu$-recursive functions).

Here is an example closely related to "computability theory" that I "nearly" understand:

For a sequence $(a_n)_{n\in \mathbb N}$ of natural numbers, the set of all natural numbers occurring in the sequence $U_a:=\cup_{n\in \mathbb N}\{a_n\}$ is a subset of the natural numbers. Each subset $U$ of the natural numbers gives rise to a unique sequence $(a_n^U)_{n\in \mathbb N}$ with $a_n^U < a_{n+1}^U$ and $U=\cup_{n\in \mathbb N}\{a_n^U\}$. Two subsets $U$ and $V$ of the natural numbers are identical if and only if the sequences $(a_n^U)_{n\in \mathbb N}$ and $(a_n^V)_{n\in \mathbb N}$ are identical. Comparing two sequences for equality is easy, at least when the sequences are given explicitly in a computable form. However, it may happen that a computable sequence $(a_n)_{n\in \mathbb N}$ gives rise to a set $U_a$ for which the sequence $(a_n^{U_a})_{n\in \mathbb N}$ is not computable. Even worse, there are computable sequences $(a_n)_{n\in \mathbb N}$ and $(b_n)_{n\in \mathbb N}$ for which there exists no computable way to determine whether $U_a$ and $U_b$ are identical.

It seems to me that all references to "computable" in this example can be made exact by interpreting them as "computable by a $\mu$-recursive function", except the statement "there exists no computable way".

• Is there a way to also give the statement "there exists no computable way" a well defined meaning in the context of recursion theory?
• Can the example be further simplified? Is the statement "there exists no computable way" necessary at all for understanding the "undecidability properties" that allow the "law of the excluded middle" to not apply (in certain mathematical contexts)?
• Are there simpler examples using less infinite objects and assumptions, for examples just working with sequences of 0 and 1 without making the rest of the construction significantly more complicated?
• Are there any questionable assumptions or axioms used by the example above, except the assumption that the union $\cup_{n\in \mathbb N}\{a_n\}$ always exists?

Edit The comments below show that it is quite difficult (for me) to explain what I actually would like to know. Especially, there was the suggestion to change the title of the question. The problem is that the title is actually quite appropriate for my question, but that mentioning of the "laws of thought" seems to divert the attention of the readers completely from what I actually want to know. There is also a limit to how much I want to change an existing question by editing. Trying to clarify the question is fine, but if it should be necessary to turn it into a completely different question I prefer to ask another question instead.

Answer 1

Here's a doubt we can have about the LEM: First you'll need to have proven Goedel's incompleteness theorem: for Peano Arithmetic, $PA$, there is an arithmetical sentence $S$ such that $PA$ does not prove $S$ and $PA$ does not prove $\lnot S$. Since $PA$ is a first-order theory of classical logic, for any sentence $X$, $PA$ proves $X \lor \lnot X$. In particular then, $PA$ proves $S \lor \lnot S$. Yet $PA$ proves neither disjunct. So the meaning of $\lor$ in classical logic seems to be just wrong in some cases: we have proven a disjunction yet we can prove neither disjunct. Then first-order theories lack the so-called disjunction property.

In contrast, if we take the same axioms as $PA$ yet use intuitionistic first-order logic, where we take classical FOL and discard (one of the axioms equivalent to) LEM, then we do have the disjunction property: Anytime this system $HA$ proves $A \lor B$, then either $HA$ proves $A$ or $HA$ proves $B$. So there's a dilemma we face: either have classical logic and have $\lor$ behave deviantly, or use a non-classical logic, like intuitionism, have the disjunction property, at the cost of (among other things) a more complicated semantics for the logic. Granted this is also an example also using an independent statement, but I would submit this is less "advanced" than CH, and maybe it's a helpful way to rephrase what your worry was about LEM.