This talk investigates logical connections between is and ought in a purely proof-theoretic way in contrast to model-theoretic investigations. It is established as a new insight that the Is-Ought-thesis (in a special form) is deeply related to the cut elimination theorem. The setting is Gentzen sequents. The key result, i.e. that the formal system in question does not allow for Is-Ought-Inferences, is established in a syntactic way.