It's clear that you can fix some particular set notation that can enable you to perform those three operations computably, as well as determine if some set is a member of another, because every set has finitely many members and you can test equality between sets by checking that every member of one is a member of the other. The recursion terminates because the depth of nesting is finite.

@Raute: Hello! Any inquiry/discussion on (mathematical) logic is welcome here.

@user21820: Hey there! I was just stopping by to copy your text on tomorrow's discussion. I'm a rookie but I'd like to follow along. May I, even if I can't contribute anything meaningful?

@Raute Sure why not? There is no obligation to 'actively' participate. You can just follow the discussion and ask to clarify anything that is unclear to you.

Yay! Thanks. :-)

In fact, that is the main purpose of my discussion session, to give as simple proofs as possible of the incompleteness theorems, and try to ensure that everyone understands them. The side-remarks are indeed at a higher level but that's more for interested people to explore in greater depth if they wish.

The main problem I see is that there is hardly any simple yet rigorous proofs of the incompleteness theorems anywhere, even on the internet. This leads to people having to rely on pop-science articles most of which are wrong, or having to wade through a hundred pages of a proper logic textbook just to get to the desired goals.

In contrast, my write-up only relies on basic understanding of programming, and is just a few pages. One reason is that I think few people are aware of this type of proof. Everyone hears of the "This statement is unprovable." kind, which is actually a significantly harder route. I myself did not know of the proof I presented until I read a blog post by someone who isn't even a professional logician...

@Raute: So yeap I'm glad you would like to join. =)

The more people get to learn about it, the better!

@user21820 what's the difference between ⟹ and →?

@LeakyNun I use both interchangeably, but some authors use "⇒" for the notion of "logically implies" in the meta-logic.

I simply use brackets and precedence rules to make things clear.

For example, if S |− P ⇒ Q (where |− has lower precedence) then ( S |− P ) ⇒ ( S |− Q ).

But the converse may not hold for arbitrary P,Q, if you recall a recent conversation.

Those authors that use "⇒" for "logically implies" would write instead:

> if S |− P → Q then P ⇒ Q over S.

or something like that.

I don't because it's usually unclear.

wat

@LeakyNun wat what?

I don't understand

Which line?

every

@LeakyNun Ok I assume you know what "|−" means?

sure

Given any first-order system S and sentences P,Q over S, if S |− P⇒Q then ( S |− P ) ⇒ ( S |− Q ).

It's easy to prove this. Just notice that you can combine proofs of P and of P⇒Q to get a proof of Q over S.

what does "logically implies" mean?

and what is material condition?

Never mind any of that. We just look at the mathematics. Do you get what I just said?

sure

but that doesn't answer my question

Now some authors presumably don't like writing so much and so they do not use "⇒" for the first-order implication symbol. Instead they define that P⇒Q over S iff ( ( S |− P ) ⇒ ( S |− Q ) ).

Under this definition P⇒Q over S does not always imply that S |− P→Q, as we recently discussed with Mathmore.

Some other authors define P⇒Q semantically (for first-order S), namely that it is true iff every model of S that satisfies P also satisfies Q. Under this definition P⇒Q over S if and only if S |− P→Q.

Anyway I guess most authors use the term "logically implies" for the semantic definition above, so you can ignore what I said earlier.

hmm

Makes sense now? It's not really important; just know the precise definitions that the author is using.

The equivalence of the semantic truth of "⇒" and syntactic provability of "→" can be proven via the semantic-completeness theorem for first-order logic.

I'm just confused why "logically" means semantically not syntactically

@LeakyNun This is a social/historical phenomenon.

In other words, people use words the way they want to, and if sufficiently many do it in one way, then it becomes a norm.

Excited for tomorrows discussion! :D