The existing answers fail to capture the important criterion that the formal system in question can carry out arithmetical reasoning. If you look carefully, the most precious ingredient of all in Godel's contribution was the β-function, so I feel that it should be adequately represented.
Also, n...
@Wildcard There is something slightly wrong with that. The definition of the island implies that N can only say true or false sentences, and so N cannot say something that cannot be guaranteed to be boolean. In particular, N cannot say "You will never believe that I am a knight." to L unless somehow N can foresee the future of L. The argument then rests on the existence of such an N (and L). In provability logic existence of L is soundness and existence of N is the modal fixed point lemma.
Alright I came to the later part that says pretty much the same thing, namely that L should doubt that N is a native of the knight-knave island...
Haha okay I shall read it to the finish before commenting more. =)
The part about self-fulfilling beliefs again comes down to the existence of modal fixed points, this time in N saying "If you ever believe I'm a knight, then the cure will work." which is instantiating a sentence K such that K⇔(⬜K⇒C). The paper calls reasoners who can do so "reflexive" for some opaque reason. And it seems to me that whoever believes the doctor's claim can be called "wishful". And Lob's theorem can be thought of as a resolution of Curry's paradox.
By the way, if we do have modal fixed points, then although "⬜P⇒P" is in general not deducible, it is still possible to allow deducing "P" from "⬜P". In English, it is wishful to think that in any scenario everything I believe is true (how about the scenario where I believe nonsense?), but it is acceptable to think that anything that I believe absolutely (in all scenarios) then it is true. This is a sound rule if the original system is sound (or just Σ1-sound if ⬜ = Provable).
@user21820 this is why I personally don't believe that every statement must be either true or false. Believing this fact itself can lead to logical contradictions. :)
In other words, I don't accept the Law of the Excluded Middle—but I'm usually amenable to accepting specific instances of it on a case-by-case basis. (Outrageous, right?)
By L doubting it just means that L neither believes nor disbelieves that N is a native of the KK island.
It does not disallow L from believing LEM for "N is a native of the KK island.".
In particular, it is okay for any logician to believe LEM for every statement about reality. I expand on this idea in a few of my posts (see my profile: "Building Blocks" and "Paradoxes resolved" under "Foundations").
In particular, in that second post I justify LEM for statements about reality as well as show that we cannot have LEM in general if we want to be able to express certain reasonable notions.
You're welcome! The whole incompleteness business is quite fascinating to me.
user131753
I forgot to tell you that recently I have made two posts regarding the difference of an axiom scheme and an axiom of which we discussed earlier. The links of the posts are:
The basic question which motivated me to write this post is the following,
What is(are) the difference(s) between an axiom scheme and an axiom?
In Margaris's book First Order Mathematical Logic we have the following,
However, the difference between an axiom and an axiom scheme is not clea...
The basic question which motivated me to write this post is the following,
What is(are) the difference(s) between an axiom scheme and an axiom?
In Margaris's book First Order Mathematical Logic we have the following,
However, the difference between an axiom and an axiom scheme is not clea...
@user21820 yeah, I guess they did. Too bad. Now our example of peacefully (and friendlily) resolving what started as a fight on the internet shall not be preserved for posterity. :)
Oh well. I guess I'll have to start and then resolve another fight now, so I can prove it's possible. :D
@user170039 I see you've received two answers that are basically covered by what I've told you over here. =)
Indeed the term itself "schema" is used because it's not just an arbitrary axiom set but a specific template-based set. It's not exactly precise, so some people might not consider arbitrary recursive sets to be schemas, but perhaps just primitive recursive.
@user170039: There are rather complicated schemas. For example, see this thread where they are referring to a "reflection schema for PA", which is basically the collection of all sentences of the form "( PA proves P ) implies P". Now it may seem that it is just a sentential template, but not if you want this schema to be over the language of arithmetic, since we need to encode "PA proves P" as an arithmetical sentence!
The basic question which motivated me to write this post is the following,
What is(are) the difference(s) between an axiom scheme and an axiom?
In Margaris's book First Order Mathematical Logic we have the following,
However, the difference between an axiom and an axiom scheme is not clea...
