In this thesis, we introduce a proof-theoretic approach for verifying hyperproperties expressed in Hyper²LTL, an extension of HyperLTL that adds second-order quantification over sets of traces. Current methods for verifying such hyperproperties rely on model checking, which becomes infeasible for complex properties or large systems. To mitigate this problem, we develop two inductive proof rules for a universal and an existential fragment of Hyper²LTL, enabling formal verification of second-order hyperproperties over transition systems. Both fragments are restricted to second-order quantification over subsets of system traces that define a unique fixed-point. The universal rule allows reasoning about properties that must hold for all traces in such a fixed-point-defined subset, while the existential rule establishes that some property holds for at least one trace in that subset. Both rules are shown to be sound and complete (relatively in the case of the universal rule), and enable us to reason about a wide range of non-trivial hyperproperties, such as stutter equivalence and common knowledge in multi-agent systems. Our rules avoid the explicit fixed-point computation by internalizing it into the rule structure, allowing properties to be proven inductively. We investigate the completeness of the universal rule under different logical frameworks and establish the ultimately periodic nature of the witness in the existential rule. We also demonstrate the applicability of our method through various examples, showcasing its contribution to a principled approach for verifying rich hyperproperties beyond the expressive power of standard first-order or propositional temporal logics.