« first day (1291 days earlier)      last day (1190 days later) » 

12:25
@user21820 I voted. I am quite surprised that they give an entire silver badge for giving just one vote.
@user21820 Does you system allow a deduction like this?
If ∃x ∈ S (P(x))
    Let c ∈ S such that P(c)
    P(c)
∃x ∈ S (P(x)) ⇒ P(c)
@Prithubiswas No, because "P(c)" is not a boolean statement in the outer context, which is where you must apply the ⇒intro rule.
@user21820 Oh . So thats where the fault was...
@Prithubiswas Yes, similarly if you introduce new variables inside a ∀subcontext, you can't use them when you apply ∀intro.
12:49
@user21820 Is P(c) a boolean statement in the "inner" context?
@Prithubiswas Yes it is.
Remember the syntax rules? "A" is a boolean statement iff you can deduce "A : bool".
Yes I do remember the syntax rules. I have it opened up from my bookmark. Although I am not not sure precisely which rule is responsible for
P(c) : bool in the inner context.
> [v is a used variable] ⊢ v : term
After the "Let c ..." line "c" is now a used variable.
So after that:
t[1],...,t[k] : term ; [Q is a k-input predicate-symbol] ⊢ Q(t[1],...,t[k]) : bool
right?
Right.
12:58
Thanks. That resolves the confusion for me. I think I should make a notepad with all my understanding about the system in it to recall them later. Is that a good idea?
Might be useful for experimentation.
@Prithubiswas Of course you should take your own notes for your own reference. I did that when I was an undergraduate, for all the courses that I couldn't completely understand immediately.
And yes it's a good idea to experiment as much as you can. Trying to break a system is a good way to understand how it works if you fail to break it. =)
@user21820 Since you mentioned the election , do you ever find it odd that they offer an entire silver badge for just giving one vote?
@Prithubiswas Lol many of the badges are so disgusting that even that badge is better.
@user21820 Huh?
There are horrible badges? That is something I don't know about.
For example, the fanatic badge, archaelogist badge, tumbleweed badge. Bad behaviour is encouraged by such badges.
Not many users actually engage in objectionable behaviour due to the badges, but it does happen occasionally with some regularity.
Not to say that the gamification aspect of the whole SE system is distasteful. At least the voting badge only encourages voting and nothing else, which can be said to be a good thing.
13:14
Fanatic badge: If you miss a day , game over.
Archaelogist badge: Edit old posts for no reason.
Tumbleweed badge: Why ? just ... why?
@Prithubiswas Exactly.

« first day (1291 days earlier)      last day (1190 days later) »