Truth semantics refers to the approach of giving the semantics of a formal language L by interpreting it in a model that is assumed well-enough understood (a form of denotational semantics), with the understanding that a different ambient language supplies the necessary notion of truth and enables us to reason about truth in the model.
Tarski published a result on the undefinability of truth [1], which uses diagonalization to show that in a formal system that is appearing strong enough to reason about its own semantics, one cannot properly define a notion of truth. Reasoning about truth semantically - without reference to the formal system - then became the point of departure for Tarski's semantic theory of truth [2] and the standard approach taken in model theory.
Formulating a semantics of truth amounts to assigning meaning only to the formulas of a logical system (not the proofs). Soundness - that a proof in L is a statement that is actually (semantically) true - amounts to showing that from a proof in L one can obtain a proof in the ambient language used when reasoning about truth in the model.
There are many synonyms of this practice:
Some would say that this is the same as working in a proof-irrelevant manner. This is not entirely clear: in algebraic presentations of logic there are 'degrees' of truth, which are modelled by the different elements of a Heyting or Boolean algebra. Arguably, this is what proof-irrelevance corresponds to. In Girardian terms, it corresponds to a new layer -1: not quite up to mere provability, but not going as far down as the semantics of proofs (layer -2).
Used in the classic book Proofs and Types. ↩︎
Used in the more recent book The Blind Spot. ↩︎