解释是一种将形式语言中的符号赋予意义的行为。许多使用于数学、逻辑及理论计算机科学的形式语言都会以纯语法的方式定义，且直到给予某些解释之前，不含有任何意义。一般研究形式语言的解释的学科称为形式语义学。
最常研究的形式逻辑为命题逻辑、谓词逻辑及其衍生的逻辑，且此类的逻辑都已经有标准的方式来给出解释。在这些情况下，解释是一个可以提供目标语言的符号及符号字串外延的函数。例如，一个解释函数可作用在谓词（表示“高”）上，并赋予其一个外延{}（表示“小明”）。须注意的是，上述解释只是将外延{}赋予在非逻辑常数 之上，但没有宣称是否表示“高”， 是否表示“小明”。同样地，逻辑解释也没有对“和”、“或”及“否定”之类的逻辑联结词作宣称。虽然人们习惯上可能会把这些符号拿来代表特定的事物或概念，但这不是由解释函数来决定的。
解释通常（但不总是）会提供一个方法来决定语言中句子的真值。若一给定解释赋予一个句子或理论的真值为真，则这个解释即称为此一句子或理论的模型。
形式语言是由一组固定句子（依上下文不同，也称为词或公式）所组成的，这些句子则是由一套固定的字母或符号所组成。用来定义语言的字母清单称之为字母表。形式语言的重要特性之一在于，其语法不需要指涉解释即可定义。例如，( 或) 是一个合式公式，即使不知道真值是真是假。
为了区分形式语言中的符号字串和随意符号字串之间的不同，前者有时被称为合式公式。
定义一个形式语言: (Φ 中的一部分Φ 在此解释下为真，所以 为真。现在，只存在另外一种可能的解释，即令Φ 为假，则¬Φ 因否定联结词而为真。结果， 还是为真，因为 中的一部分~Φ 在此解释下为真。既然这两种对 的解释是唯一可能存在的逻辑解释， 在每个解释下皆为真，因此称之为逻辑有效的，或重言式。
理论的解释是指一个理论与某个论题之间的关系，是一个在理论中的某些基本叙述与和论题相关的某个叙述之间的多对一对应关系。若每个理论中的基本叙述都找得到一个对应，则称之为完全解释；若其中有些无法找到对应，则称之为部分解释。
命题逻辑的形式语言是由以命题符号（亦称为句子符号、句子变数及命题变数）和逻辑联结词建构成的公式所组成的。在此形式语言中，唯一的非逻辑符号只有通常会标记为大写字母的命题符号。为了要使这个形式语言够精确，一些特定的命题符号必须要先确定。
此类形式语言中的标准解释为一个将每一命题符号映射至真值的真或假之中其中一个的函数。此函数称为真值赋值函数。在许多的表述中，这个函数就于字面上的意思会赋予一个真值，但在部分的表述中，这个函数赋予的是另一种真值载体的概念。
对有着 个不同的命题变数的语言，存在2 个不同的可能解释。举任意一个变数 为例，存在21=2 个可能解释：1) 赋值为“真”，或2) 赋值为“假”。对一对、 来说，存在22=4 个可能解释：1) 两者皆赋值为“真”，2) 两者皆赋值为“假”，3) 赋值为“真”且 赋值为“假”，或4) 赋值为“假”且 赋值为“真”。
给定一组命题符号的真值赋值，对所有由这些变数建构成的公式，即只存在唯一一个解释的扩展。这个扩展解释可以利用上面讨论过的逻辑联结词的真值表，来递归地定义。
不像命题逻辑，每个语言除了选定的命题变数不同之外，其他都一样，一阶逻辑则存在着许多不同的一阶语言。每个一阶语言都可以由标识来定义。标识是由一组非逻辑符号所组成的，且将每个符号识别为常数符号、函数符号或谓词符号。在函数符号及谓词符号里，也会被指派给一个自然数元数。这类形式语言的字母表即是由逻辑常数、等式关系符号 = 、所有在标识中的符号，以及额外一组无限多的符号（称为变数）所组成的。
例如，在环的语言里，有常数符号0 和1、两个二元函数符号+ 和·，且没有二元关系符号。（此处，等式关系被视成是一个逻辑常数。）
给定一标识σ，其对应的形式语言即为由σ-公式组成的集合。每个σ-公式都是由原子公式以逻辑联结词的方式建构而成的；原子公式则是由使用了谓词符号的项建构而成的。σ-公式的集合的形式定义以另一种方向得出：首先，由常数和函数符号，以及变数集结为项。然后，项可以使用标识中的谓词符号（关系符号）或表示等式的特殊谓词符号“=”来结合成原子公式。最后，此语言的公式即可由使用逻辑联结词和量化的原子公式集结而成。
为了将意义赋于一阶语言的所有句子之中，下列的资讯是必需的。
带有这些资讯的物件即称为结构，或“模型”。
解释中指定的资讯可提供足够的讯息，在每个自由变数都替代为论域中的元素后，以决定任意一个原子公式的真值。然后，任意句子的真值即可使用T-模式递归地定义。T-模式使用真值表如上所述来解释逻辑联结词。因此，举例来说，φ & ψ会被满足，当且仅当φ 和ψ 都会被满足。
接下来剩下要如何解释∀ φ() and ∃ φ() 之类形式的公式。论域会形成这些量化的值域, 其概念如下：句子∀ φ() 在一解释下为真，只在每个φ() 中的 被某个论域中的元素取代而成的置换实例都能被满足。公式∃ φ() 能被满足，若至少有一个在论域中的元素 ，能使得φ() 被满足。
严格来说，上面所叙之公式的置换实例φ() 并不是φ 原本所在这个形式语言中的公式，因为 是论域中的元素。这个技术上的问题有两种处理的方法。第一种是扩展至较大的语言，将论域中的每个元素都命名为一个常数符号。第二种是将赋予每个变数到一个论域中的元素的函数加入解释之中。然后，T-模式即可在和原解释相比，变数赋值函数有些不同的修订解释之上量化，以取代在置换实例上的量化。
一些作者会允许一阶逻辑中出现命题变数，因此也必须被解释。命题变数可以视自身为一原子公式。一个命题变数的解释即是真值的“真”或“假”的其中之一。
因为这里叙述的一阶解释是定义在集合论里的，这些解释并没有将每个谓词符号与性质（或关系）相关连，而是将其与性质（或关系）的外延相关连。换句话说，这些一阶解释是外延的，而非内涵的。
一阶逻辑的解释可举例叙述如下：
在此解释下：
如上所述，一阶逻辑通常需要指定一个非空集合做为其论域，原因在于下面的双条件句需要是逻辑有效的。
其中， 不是φ 的自由变数。这个等价在每个具有非空论域的解释下皆是成立的，但若允许空论域的话就不一定了。例如，双条件句
在任一具有空论域的结构中都无法是逻辑有效的。因此，若允许空结构的存在，一阶逻辑的证明论会变得较复杂。而且因为人们研究的理论的预期及有兴趣的解释都有非空论域，允许空论域所能获得的几乎可以忽略。
等式关系在一阶逻辑和其他谓词逻辑中通常会被特别地对待，主要有两种方法。
第一种方法是将等式视同其他的二元关系。如此，若等式符号包含在标识之中，则通常需要增加几个有关等式的公理至公理系统之中（例如，替换公理叙述，若 = 且() 成立，则() 也会成立）。这个方法通常用在研究那些不包括等式关系的标识时最为有效，如集合论和二阶算术的标识，在二阶算术中只存在数字的等式关系，但没有数字集合间的等式关系。
第二种方法是将等式视为一个逻辑常数，必须在所有解释下解释为实在的等式关系。如此解释等式的解释称之为正规模型，所以第二种方法和只研究为正规模型的解释是同样的意思。此一方法的优势在于，和等式有关的公理会自动满足于每一个正规模型，且因此不需要明确述明包含于一阶理论之中。第二种方法有时称为“具等式的一阶逻辑”，但有许多作者会不另叙明即直接采用此一方法。
将研究一阶逻辑限缩至正规模型中还有一些其他的理由。首先可以知道的是，每个等式可以解释为一个等价关系，且满足替换公理的一阶解释，都可缩减至在原论域的子集之上的一个基本等价解释。因此，研究非正规模型，只需要对正规模型做一点额外的广义化即可。第二，若考虑非正规模型，则每个相容理论都会有个无限模型；这会影响如勒文海姆–斯科伦定理之类结论的叙述，此类结论通常是在假定只考虑正规模型之下叙述的。
对一阶逻辑广义化的方法之一为考虑具一个以上类型之变数的语言。其想法为，不同类型的变数可用来表示不同类型的物件。每个类型的变数都能被量化；因此多类语言的解释会对每种变数都会有不同范围（每个类型都会有无限多个变数）、相分别的论域。函数和关系符号，除了有元数外，它们的每个参数也都会指明需哪个类型。
多类逻辑的一个例子为平面欧氏几何：具有两个类型（点和线），有对点的等式关系符号、对线的等式关系符号，及一个以一个点变数与一个线变数为参数的二元重合关系。这个语言的预期解释有其范围为欧氏平面上所有点的点变数、范围为平面上所有线的线变数，及重合关系(,) 会成立，当且仅当点 在线 上。
高阶谓词逻辑的形式语言看起来很像一阶逻辑的形式语言。不同之处在于，高阶谓词逻辑有许多不同类型的变数。一些变数相对至论域的元素，如一阶逻辑一般。其他的变数对应至较高的类型：论域的子集、论域的函数、取论域的子集为参数，传回从论域映射至论域子集之函数的函数、…等。所有此类类型的变数都可被量化。
一般常见用于高阶逻辑的有两种解释。完全语义学需要一旦论域被满足，高阶变数即涵盖所有可能的正确类型（所有论域的子集、所有从论域映射至自身的函数、…等）的元素。因此，指定一个完全解释，和指定一个一阶解释的方法相同。亨金语义学在实质上为一个多类一阶语义学，需要解释将每个类型的高阶变数指定一个分别的论域。因此，亨金语义学的解释包括一个论域、一堆 的子集、一堆从 映射至 的函数、…等。上述两个语义学的关系在高阶逻辑中是很重要的课题。
上面所述的命题逻辑和谓词逻辑的解释并非唯一可能的解释。尤其是，还存在其他类型的解释，使用在非传统逻辑（如直觉主义逻辑）和模态逻辑的研究上。
使用在非传统逻辑研究上的解释包括拓扑模型、布林值模型和关系语义。模态逻辑也使用关系语义。
形式语言通常会有预期的特定解释，这亦是当初研究该形式语言的动机。例如，集合论的一阶标识包括一个二元关系∈，预期用来表示集合的元素关系；自然数的一阶理论中的论域预期为一自然数的集合。不过，也总是存在其他“非预期解释”，其论域或非逻辑符号不是由其预期意义所给定。
在皮亚诺算术之中，其预期解释称为算术的标准模型，由自然数及其一般四则运算所组成。所有同构于上述模型的模型都称为是标准的；这些模型也都满足皮亚诺公理。当然，也存在皮亚诺公理的非标准模型，其中包含与自然数不相关连的元素。
除了将形式语言赋予上意义外，“解释”还有其他不同的意思。
在模型论中，称结构 解释结构，若存在一个 的可定义子集，和 上的可定义关系与函数，使得 同构于具论域 及之上函数与关系的结构。若需要更多的说明，请见解释 (模型论)。
称理论 解释理论，若存在一个 的有限定义扩展′，使得 包含于′ 。
& ∨ ¬ ~ → ⊃ ≡ | ∀ ∃ ⊤ ⊥ ⊢ ⊨ ∴ ∵
