Truth Semantics

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:

1. Caring only for the semantics up to provability
2. Using Tarskian semantics, an older term used by Jean-Yves Girard.^[3]
3. Operating at layer -1, a newer term due to Jean-Yves Girard.^[4]

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\frac{1}{2}: not quite up to mere provability, but not going as far down as the semantics of proofs (layer -2).