 The consequence relation of a logic system can be given in several ways, some using proof-theoretic tools, others semantic means. A substitution-invariant consequence relation can be defined using a proof system like a Hilbert-style axiom system, a Gentzen-style sequent calculus or a natural deduction style calculus, etc. One can also define a substitution-invariant consequence relation semantically using a class of mathematical objects (algebras, Kripke models, topological models, etc.) and a satisfaction relation.