@LeakyNun The issue you're facing is because you haven't precisely enough specified what you mean by "computably decide".

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?

@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