Is continuum hypothesis decidable in second-order ZFC? From this question I've found that some logicians claimed that the CH is decided in the second-order ZFC, namely $(ZFC_2\vdash CH)\vee (ZFC_2\vdash\neg CH)$. G. Kreisel's "Informal rigour and completeness proofs" of 1967 contains the result regarding Zermelo's set theory, though I've not dived into details and could misunderstand smth. Also T.S. Weston stated the opposite in his work of 1977.
Is it widely known result? Is it considered correct by logicians? Or they accept Weston's arguments? I've failed to find any modern discussion of it, though it looks interesting as it provides a natural way to define the truth value of CH and in fact re-open the problem of CH.
 A: There are several problems with this:
First of all, second-order logic is not complete. This means that even if $\varphi$ is true in all the models of $T$, it does not mean that $T$ proves $\varphi$. 
Secondly, second-order logic requires some sort of set theoretic meta-theory, since it allows second-order quantification, the notion of a set needs to be pre-existing.
If $\sf ZFC_2$ has a model then it is necessarily isomorphic to $V_\kappa$ for a strongly inaccessible cardinals $\kappa$. In particular, such model contains all the reals, all the sets of reals, and so on. So $\sf CH$ is either true in all the models of $\sf ZFC_2$, or it is false in all of them. In that sense, yes, second-order $\sf ZFC$ does "decide" the continuum hypothesis. But it is not the second-order theory that decides the value, as much as it inherits it from the meta-theory.
 
One of the good things about first-order logic is that to a large extent it is agnostic to its meta-theory. You can formalize it in $\sf ZFC$ or in $\sf PA$ or $\sf PRA$ or any system which provides sufficient induction. With second-order logic, you must inherit some of the properties of the meta-theory. So different people, working in different meta-theories, might disagree on what are "sets" to begin with. And so, if I work in a meta-theory where $\sf CH$ is true, the results would be different than someone working in a meta-theory where $\sf CH$ is false.
A: Short version: there's no contradiction, Weston and Kreisel et al mean different things when they say "second-order," and (in my opinion) Weston's paper is misleading on this point; and second-order logic is absolutely useless for attacking CH.

Weston's paper, in my opinion, is quite misleading: what he calls "second-order ZF" is really a first-order theory resembling second-order ZF. Yes, this is a different thing than ZF itself - and the crux of the matter, if you haven't seen it before, is the distinction between standard semantics and Henkin semantics. 
That Weston is referring to the Henkin, rather than standard, semantics for second-order logic is hinted at when he writes

This note presents a proof that in the usual (proof-theoretic) sense of
  "decided", second-order Zermelo-Frankel set theory (ZF$^2$) does not decide
  CH. $\quad$ (Emphasis mine)

and is made clear in his arguments. By contrast, Kreisel et al refer to the genuinely second-order theory (and see part 2 of this answer for an explanation of what they're talking about). 
This distinction is huge! Full second-order logic has no complete proof system (and this is why Weston's remark makes it clear that he's treating a first-order version of second-order ZF; also, this means that it's misleading to use "$\vdash$" instead of "$\models$" when talking about full second-order logic). The natural "first-orderization" of second-order ZF, where we include predicate variables but despite appearances work with Henkin (so, first-order in disguise) semantics, is subject to all the usual restrictions of first-order logic. 
By contrast, true second-order logic (that is, second-order logic with the "standard semantics") is intimately bound up with set theory: to tell whether a structure satisfies a given second-order sentence, we need to look at the full powerset of that structure, and of course the properties of the full powerset can depend heavily on the ambient set theory (and this has led to quite reasonable criticism of second-order logic, e.g. Quine's famous comment that it is "set theory in sheep's clothing," although others such as Boolos disagree - see e.g. this paper for some discussion of the topic).
Weston is clearly critical of full second-order logic (EDIT: this may be a flawed interpretation, see Carl's comment below). This is quite reasonable, and indeed from a proof-theoretic perspective it's hard to see how one couldn't object to full second-order logic, given that it has no complete proof system. However, I find it quite inexcusable that at no point does he explicitly state that he is working in the Henkin semantics, and instead leaves that up to the reader to discover (leading to quite reasonable potential confusions).

So how does "true" second-order ZF decide the continuum hypothesis? Well, we argue as follows.


*

*First, note that there is a second-order sentence $\varphi_\mathbb{N}$ which characterizes the structure $(\mathbb{N}; <)$ up to isomorphism (this is because "has no infinite descending sequence" is expressible in second-order logic, if we use the standard semantics).

*Now consider the language $\Sigma=\{U, V, <, E,\prec\}$ where


*

*$U, V$ are unary predicate symbols (which we think of as sorts), and

*$<$, $\prec$, and $E$ are binary relations.


*We'll build a particular $\Sigma$-sentence $\tau$, consisting of the conjunction of the following sentences:


*

*$U$ and $V$ partition the domain.

*$\varphi_\mathbb{N}$ holds relativized to $U$ (so the reduct to $\{<\}$ of the $U$-part of a model of $\tau$ is a copy of $(\mathbb{N}; <)$). This is one of the three truly first-order conjuncts in $\tau$.

*$E\subseteq U\times V$ (thought of as "$x\in y$"), $<\subseteq U^2$ (thought of as, well, "$<$"), and $\prec\subseteq V^2$ (thought of as giving an ordering of the elements of the $V$-part).

*Every subset of the $U$-part is represented by an element of the $V$-part: $\forall A\exists b(b\in V\wedge\forall x\in U(x\in A\iff xEb))$. (Of course "$b\in V$" and "$x\in U$" are abbreviations.) This is truly-second-order conjunct number two.

*Finally, that for each $v\in V$ there is an injection from $\{w\in V: w\prec v\}$ to $\mathbb{N}$. This is the third truly-second-order conjunct.
It's easy to check that $\tau$ has a model if and only if the continuum hypothesis holds. So, if you know which second-order sentences are satisfiable, then you can figure out whether CH is true; it is in this sense that second-order logic (we don't even need second-order ZF!) "decides" CH.
We can do worse: we can cook up a second-order sentence $\psi$ which is true (in the standard semantics) in every structure (= is valid for full second-order logic) iff the generalized continuum hypothesis holds; or if there is no measurable cardinal; or etc.

OK, let me wrap up with one last point. You write 

it looks interesting as it provides a natural way to define the truth value of CH and in fact re-open the problem of CH.

Unfortunately, this is not the case. First of all, the claim "second-order logic decides CH" requires us to already believe that the full powerset of an arbitrary structure exists; this level of set-theoretic realism already commits us to the claim that the continuum hypothesis has a definite truth value. So this observation doesn't get us any closer to answering the question of whether CH has a definite truth value, because it implicitly already assumes that.
Second of all, there's the fact that second-order logic has no good proof system: there is in general no way to figure out that a given second-order sentence is satisfiable without already knowing facts about the set-theoretic universe. So to tell whether CH is a validity in full second-order logic, we would need to know whether CH is true.$^1$
(For a further example of how second-order logic depends on set theory, see e.g. this mathoverflow question.)
So second-order logic, while enticing at first, is ultimately not a useful tool. Instead, it's better to think of it as an interesting object of study. 
$^1$OK, fine, there's ways around this. For instance, a set-theoretic-multiversist would argue that each universe's version of full second-order logic decides CH in that model. But this doesn't really help, because then second-order logic can decide CH in different ways in different universes, and does require us to commit to CH having a definite truth value in each universe (which the multiverse view does anyways). So I'd argue that this doesn't really avoid my point above.
A: the points raised about about my paper were discussed, 'way back in the day, in another article: Journal of Philosophical Logic, May 1976, Volume 5, Issue 2, pp 281–298,Kreisel, the continuum hypothesis and second order set theory. In particular, semantic and syntactic results are distinguished, and a semantic "proof" that the CH is decided in 2nd order ZF is included there and also, I think, debunked. Tom Weston
