Here is a short summary on how to create an uncomputable large function using formal theories avoiding common mistakes and common failures:
- Choose a foundation \(F\) of mathematics which you use. Unless it is a well-known existing one, e.g. first order predicate logic and type theory, you need to precisely define it rather than intuitively declare it and avoid Incomplete Language of a New Foundation and Intuitive Abuse of Existing Notions. If we use first order predicate logic, we traditionally omit the declaration of the foundation. Therefore if you skip to declare the foundation, the reader will guess that it is first order predicate logic unless the context obviously clarified it.
- Choose a language \(L\) for a base theory in which you work in under \(F\). Unless it is a well-known existing one, e.g. the language of first order arithmetic and the language FOST of first order set theory, you need to precisely define it rather than intuitively declare it and avoid Lack of Language. If we use the language FOST of first order set theory, we traditionally omit the declaration of the language. Therefore if you skip to declare the language, the reader will guess that it is FOST unless the context obviously clarified it.
- Choose a base theory \(T\) in which you work in by specifying a collection of axioms given as \(L\)-formulae. Unless it is a well-known existing one, e.g. Peano arithmetic and ZFC set theory, you need to precisely define it rather than intuitively declare it and avoid Lack of Axioms. If we use \(\textrm{ZFC}\) set theory, we traditionally omit the declaration of the base theory. Therefore if you skip to declare the base theory, the reader will guess that it is \(\textrm{ZFC}\) set theory unless the context obviously clarified it.
- When \(L\) is not a usual one, then you need to avoid Intuitive Abuse of Existing Axioms even when you are trying to reformulate a well-known existing theory, e.g. Peano arithmetic and ZFC set theory, because the precise choice of the collection of axioms heavily depends on \(L\) due to the occurrence of axiom schema.
- When you try to formulate a higher order set theory, you need to precisely define axioms rather than intuitively declare something like "I use \(\omega\)-th order set theory" or "I define \(0\)-classes as sets, \(1\)-classes as classes, and so on. Higher classes satisfy ZFC set theory." in order to avoid Incomplete Higher Order Theory.
- When you try to formulate the definability by formulae in a formalised theory \(FT\), the definability itself should be defined in the base theory \(T\) in which \(FT\) is defined. Therefore you need to define not only \(FT\) but also \(T\) in order to avoid Lack of Base Theory.
- Define a large function in \(T\) by only using what have already been defined in \(T\) without using unformalised intuitive descriptions.
- When you try to use an existing notion, you need to understand its precise definition rather than its role in order to avoid Intuitive Abuse of Existing Notions again. Namely, unless you do not understand its precise definition, then you might abuse it even when it is not defined in \(T\) or is not applicable to the current situation. See also cheatings in I fully understand it although I do not know the precise definition! and I use ill-defined functions, because well-defined function are much weaker!.
- When you refer to the truth of or the definability by a formula in a theory \(FT\) formalised in \(T\), you need to precisely define it in order to avoid Intuitive Truth Predicate and Intuitive Definability.
- Skipping the actual definition solves nothing. See also cheatings in It is easy to outgrow the function!, It works in my mind!, I have already done it!.
I hope that this guideline will help you to create an attractive uncomputable function.