文字 (数理逻辑)

在数理逻辑中，文字(literal)是一个原子公式(atom)或它的否定。文字可以分为两种类型:

  • 肯定文字就是一个原子。
  • 否定文字是一个原子的否定。

纯文字是其变量(在某个公式内)的所有出现都有相同符号的文字。

解释

文字来源于拉丁文的 litera 就是字母的意思。

在编程语言中，文字表示的字符串的意思，这个些字符串被允许或者用来定义基本类型的（Basistypen）（比如说，整数，浮点数，字符串等等）。它们没有被标记，但是却在某些情况下被植入编程源中。文字只能在右边的表达法（比如说在一个指示性运算符或者函数论证的右边）中出现。绝大多数情况下，文字被归入常量或者指称为文字常量，因为两者相对于变量和运行时间来讲是相对不变的。常量在严格的意义上来讲就是其赋值不变的表达因子，也就是说，指称在源代码中可以经常应用的唯一的对象，而不是将相同的文字重复给出。

例子：

逻辑值： 真，假 （在许多语言中都是被保留的单字或词） 整数：1200，＋1200，－12 （只有数字和＋， －号） 浮点数：12.34, －12e34, 12.e-34 (数字，前缀，点，e) 单一的字符： 'a' （在标点间的任意单个字符） 字符串：“这是一个字符串”（在双引号之间的任意个字符）

在逻辑当中人们称一个定理为文字，如果它既非真（w,wahr,true)，又非假(f,falsch,false)。这既包括单一的语句，也包括相互连结的语句。在二值的逻辑中没有“半真”的情况。这个定理可以来自于日常的用语，也可以来自数学用语。

引用

  • Buss, Samuel. An introduction to proof theory. Handbook of proof theory. Elsevier: 1–78. 1998. ISBN 0-444-89840-9.