Kutta
1516
252
Kutta has not written any posts yet.
Kutta has not written any posts yet.
It is important to distinguish the "complete" which is in Gödel's completeness theorem and the "complete"-s in the incompleteness theorems, because these are not the same.
The first one presupposes two things, a) a syntax for a logical language, also containing a syntax for proofs b) a notion of model. Then, a combination of a) and b) is complete if every sentence which holds in all models is also syntactically provable.
The second one for our purpose can be summarized as follows: a syntax for a logical language is complete if for every sentence , either or its negation is provable. This sense of completeness does not mention models or semantics!
The main point... (read more)
I'd like to ask a not-too-closely related question, if you don't mind.
A Curry-Howard analogue of Gödel's Second Incompleteness Theorem is the statement "no total language can embed its own interpreter"; see the classic post by Conor McBride. But Conor also says (and it's quite obviously true), that total languages can still embed their coinductive interpreters, for example one that returns in the partiality monad.
So, my question is: what is the logical interpretation of a coinductive self-interpreter? I feel I'm not well-versed enough in mathematical logic for this. I imagine it would have a type like "forall (A : 'Type) -> 'Term A -> Partiality (Interp A)", where 'Type and 'Term denote types and terms in the object language and "Interp" returns a type in the meta-language. But what does "Partiality" mean logically, and is it anyhow related to the Löbstacle?
You're right, I mixed it up. Edited the comment.
Suppose "mathemathics would never prove a contradiction". We can write it out as ¬Provable(⊥). This is logically equivalent to Provable(⊥) → ⊥, and it also implies Provable(Provable(⊥) → ⊥) by the rules of provability. But Löb's theorem expresses ∀ A (Provable(Provable(A) → A) → Provable(A)), which we can instantiate to Provable(Provable(⊥) → ⊥)→ Provable(⊥), and now we can apply modus ponens and our assumption to get a Provable(⊥).
To clarify my point, I meant that Solomonoff induction can justify caring less about some agents (and I'm largely aware of the scheme you described), but simultaneously rejecting Solomonoff and caring less about agents running on more complex physics is not justified.
The unsimulated life is not worth living.
-- Socrates.
You conflate two very different things here, as I see.
First, there are the preferences for simpler physical laws or simpler mathematical constructions. I don't doubt that they are real amongst humans; after all, there is an evolutionary advantage to using simpler models ceteris paribus since they are easier to memorize and easier to reason about. Such evolved preferences probably contribute to a matemathician's sense of elegance.
Second, there are preferences about the concrete evolutionarily relevant environment and the relevant agents in it. Naturally, this includes our fellow humans. Note here that we might also care about animals, uploads, AIs or aliens because of our evolved preferences and intuitions regarding humans. Of course,... (read more)
Donated $500.
Survey taken.
Yes. To expand a bit, in fact the straightforward way to show that second-order arithmetic isn't complete in the first sense is by using the Gödel sentence G.
G says via an encoding that G is not provable in second-order arithmetic. Since the only model (up to isomorphism) is the model with the standard natural numbers, an internal statement which talks about encoded proofs is interpreted in the semantics as a statement which talks about actual proof objects of second-order arithmetic. This is in contrast to first-order arithmetic where we can interpret an internal statement about encoded proofs as ranging over nonstandard numbers as well, and such numbers do not encode actual proof objects.
Therefore, when we interpret second-order G, we always get the semantic statement "G is not provable in second-order arithmetic". From this and the soundness of the proof system, it follows that G is not provable. Hence, G holds in all models (recall that there is just one model up to isomorphism), but is not provable.