> I don't think that's a question that can be answered. Robert Munafo makes the point that if we went beyond formalism and computability theory, we'd by definition have nothing to define.
> There probably is no hard limit that we are going to bump into in googology, but ... that will still all be within a formalism that we can't escape, and that will place a certain fundamental
> limit on what kinds of finite numbers we can express. The catch is, we'll probably never be able to describe the size of that box without barry paradoxes or worse. So some finite numbers
> will probably always be inaccessible to us. We know they must exist, but that's about all we can say without being self-contradictory. If it's true that we can't escape computability theory then it proves the point I was trying to make with my site: that saying we can "continue indefinitely" is not exactly true. Not at least in the sense that there is no fundamental limit Sbiis Saibian (talk) 23:41, February 6, 2013 (UTC)
Is there is difference between being singular and first? It appears to me that there is - though both notions can be described by the figure of '1'.
Here what I mean by singular - it has no successors, nor any predecesors; to be exact - it is not a part, or a term.
But can mathematics actuall...
@DavidReed @AlessandroCodenotti: This assumption is not necessary in any reasonable foundational system, because having a proof verifier program is simply equivalent to having a recursive axiom set, for any first-order theory. Even in natural language, the definition of "recursive" is via programs.
@Secret That's false. Every finite integer is by definition computable; just output it. "Uncomputable" can only refer to functions.
@Secret Berry's 'paradox' is not a paradox at all, because if you actually attempt to make it logically precise you will find that it is impossible to get what you actually want. You should maybe point that person to the following post:
Let us be more precise about definable numbers, to avoid common pitfalls.
Suppose we have chosen our favourite foundational system $S$, which is in modern mathematics ZFC. $S$ of course can be implemented by a computer program that will given any input theorem and purported proof will output "ye...
It's sometimes good to see how it actually can be done with restrictions, rather than me just saying it's difficult to get right or get what the 'paradox' needs.
@skullpatrol Oh look Mozibur answered his own question with some nonsense. If his question was not about mathematics, that would still be acceptable.
@skullpatrol Incidentally, before coming here I just posted an answer that implicitly addresses the question of whether we can define 1 as a natural number:
I think that sentence is not 100% precise but was intended to mean:
Undecidability of a sentence over a deductive system is merely whether or not that system proves or disproves the sentence, and is a purely syntactic matter (at least if you believe in the classical properties of finite strin...
Of course, one could argue that "one" can be treated as a single concept of "uniqueness" and not as part of any structure, but it's a bit weird to still use "1" if we don't also want to relate it to "2" and other naturals.
I suppose you could say a proof verifier on a MODERN machine, but we have no way of knowing whether futuristic computers will be stronger than turing complete. Especially given all the AI advancements going on (neural network etc.).
For short values of n there unquestionable bias, like ppl always think of the ace of spades and nine of diamonds when asked to think of a card
but for long runs i surmise that it would very much be random
The other thing I can do that turing machines are infamous for not being able to do is compute things about mysefl
I also think I might have a stronger ability to engage in proof verification: Is there a program that is capable of learning the English and symbolic math language sufficiently to do proof verification with the input effectively the paragraph form of proofs. That is, proof verification in English language. I would have to think about that, would require going back into grammers :(
In intro to comp sci class it is a common open saying : "Computers are extremely dumb, they are just very fast"
How is the semantic of formula with free variables in FOL defined ?
In wikipedia it says that the formula is true iff the universal closure of the formula is true (universal closure means that we place Uni-Quant before any free variables )
Small correction, the wikipedia says the formula is satisfiable iff...., not "true"
but my professor seems to say that the formula is satisfiable iff there is an interpretation in which it is true
in other words, it just has to be true for a particular assignment of these free variables in a given structure
then it is satisfiable
so my question is, which one is correct/ more standard ?
@TungNguyen It depends on the particular system. My preferred one doesn't assign semantics to formula having free variables. Others assign it to be true if the universal closure of the formula is true
Is there is difference between being singular and first? It appears to me that there is - though both notions can be described by the figure of '1'.
Here what I mean by singular - it has no successors, nor any predecesors; to be exact - it is not a part, or a term.
But can mathematics actuall...
