数理逻辑/形式与符号
形式
从众多具体现象中抽象出的具有某种同样性质的模式，称为形式。比如老鼠会打洞可以模板化为老鼠 会 打洞，同时将具体对象和谓词抽象化，形式化为 ， 是一个动物， 为一个动作， 为一个谓词。当然也可以进一步形式化为 （ 是不同的名词， 是一个动词 ）乃至进一步为 （ 各为一个不同的词）。
老鼠会打洞（实例）→老鼠 会 打洞（模板）→动物名词 谓词 行为名字（形式）→名词 谓词 名词（形式）→词 词 词（形式）
从左往右，距离实例越来越远。直观的来看，越右的形式能创建的实例越多。
从形式反过来到实例的过程则称为实例化，显然，“动物名词 谓词 行为名字”形式除了可实例化老鼠会打洞。也可实例化为猫会吃老鼠或老鼠会吃猫。这是形式化的一个主要用处，假如一个形式可以反映一个对象的某些特性，则只要定义或推演这个形式的特性或属性，就等同于定义或推演了这个形式下所有可能实例的属性。这样，我们可以定义一套形式化程度恰到好处的公理或规则，然后将现实世界的某些事物或现象“挂靠”或称形式化到形式上，这样就获得形式的正确性。
过程：
提前定义形式1→形式1具有性质1→发现实例1→发现实例1可以形式化为形式1→实例1具有性质1
变量
一个对象是。。。随便什么东西，只要是思想可以生成的，比如“可恶的老鼠”或“爬过一条下水道”。对象一般受到一组定义的规则限制，从而缩减了其范围。比如规则“禁止前两个字是“可恶的””就使这个对象排除了“可恶的老鼠”这一可能的选择。
一个变量包含一个对象和对这个对象的限制规则，一般用英文小写字母表示。形如： （ 是一个自然数）.显然，这个变量可以包含1，2,3,4,5….以内所有的数字。将一个变量实例化的过程称为赋值。如 .代表之后 表示数字1。而一个 的赋值将导致逻辑错误。因为规则是先于赋值定义的。
命题变量是一个变量与并且这个变量只能是命题（规则）。
命题变量里的命题限制是比较松散的，可以允许 是 一类的形式。其中 和 都是可以增加任意多形容词（乃至定语从句，只要是形容词性的部分）的名词。如小灰狗 是 小的灰色的长有牙齿的犬科动物，这种动物是人类的朋友。又比如，自然数的基数小于实数。
命题变量有一个真值，换句话说，命题变量有一个属性，那个属性可以是“真”或“假”，也可以是“未定义”。这个属性是命题逻辑赋予变量的（即变量本身没有这个性质，只是在命题逻辑系统中被附加了这个性质），这类变量在更高级的一阶逻辑有类似但不相同的使用方式。
有时我们需要表示两个命题实际上是一个命题，或两个变量应是一个变量。这可以有很多表示方法，比如a,b (a=b)或像命题逻辑做得那样。应是同一个变量的位置使用同一个字母表示，相应的，不同变量之间严禁使用同样的字母表示。
虽然并不明显，但我们自然语言中的大多数部分都可以用 是 句型表示，也就是说，大多数自然语言中出现的命题都可以以命题逻辑方式形式化。比如扶老太太过马路是好的可形式化为a，金胖子是会被撑死的人形式化为a，飞机是飞机形式化为 。当然，它们只能在不同的论证中被形式化为同一个符号。但在特别指定一个实例前， 可以实例化为其中任意一个命题。
这看起来很无聊，因为符号 并没有任何性质，可以让我们将实例“挂靠”到（形式化为） 上后推出任何关于 的“新”信息（严格的说，演绎推理不会产生任何新信息，因为信息在指定公理和实例后就应该“自动得到”了。但这一点并不明显，比如你并不能总那么容易的做出几何证明题，虽然那些题在无限穷举下总是可以被做出的）。
推理
现在我们来考虑命题之间的交互。假设有这么一个问题“我是男人或是女人 我不是女人 是否可以推出我是男人”？
答案是“可以推出”，这样一类陈述称为复合命题。至于它怎么形式化来获得对“可以推出”这一答案的正确性的证明，马上就可以见到。现在先以一般的方式推理这个问题，假如你觉得这个问题太简单，明显了。那么令人高兴的，命题逻辑就是建立在这些显而易见正确的思维之上，在此之外，命题逻辑排除了一些人类思维中含糊的地方，并使大规模的推理（以以上语句组成，但长度翻一百倍的陈述。人类通常能直达问题命门的感觉性的思维毫无用途，只能依赖命题逻辑的一种机械计算。）
根据自然语言的定义，“我是男人或是女人”可以转化为“我是男人或我是女人”，“我不是女人”可以转化为“我是女人，这一命题为假”。现在开始形式化，显然以上语句都可以形式化为 是 形式，令 为命题“我是男人”，令d为命题“我是女人”。
现在有两个命题 和 分别代表不同的意思。我们得有一种方式表示“我是男人或我是女人”，我们使用符号 ，转为“ ”。 “ ”也可表示为另一个命题 ，对于这一点，只需构建“变量命题 是“我是男人或是女人”这一命题（定语从句）”即可。不过直观的来看，这么做除了减少了信息毫无意义，不过注意到这一点有助于加深对复合命题的理解，这种方法在推理算法中也有应用。由于可以表示为另一个命题，所以“ ”也有一个真值（这一过程可以复习形式化的用途，我们将“ ”形式化为命题，然后根据命题逻辑对命题的定义，“ ”这一命题的实例有一个真值。）。更一般化的，所有经“ ”之类的符号计算的复合命题都可以视为另一命题并拥有真值。而“ ”之类的符号就是将参数（如符号左右两边的命题）的真值经过计算后得到一个新命题的新真值，并通过一系列这样的复合表示一整个陈述。
对于任何类似“我是男人或女人”，“我是女人，这一命题为假”的语言，我们称为为条件，所有条件都是真的。这就是说“ ”的真值为真。可像“我是女人，这一命题为假”这种语句中就表示这一命题为假的语句应该怎么表示呢？只要令“命题为假”这一断言为真即可。换句话说，假设a表示命题“我是人”，而且这是一个条件。则 的真值为真。而“我不是人”=“我是人，这一命题为假”这一命题可以先用某种符号将其表示为“ 命题为假”，那自然“ 命题为假”为真就代表 命题本身为假了。使命题从直接的含义转为对直接的含义的否定的符号是 ，如 表示“我是人”，则 表示“我是人，这一命题为假”即“我不是人”。注意“这一命题为假”这种用法并不一定必然可以转化为“我不是人”这种“自然的”表述。可以是““我不是人，这一命题为假”这一命题为假”之类的句子。其中根据日常语法的定义，这种双重否定句将导致肯定，逻辑中有一条类似的规则 ，这里暂不详述。
现在，我们有两个断言， 与 。我们想知道它是不是能推出命题 （这种符号单独出现时代表这一命题为真，在这里代表“我是男人”或称“我是男人，这一命题为真”）。为此，我们形式化的定义 和 的意思，以符合我们推理的直觉。前面已经提到过， 是让一个命题附加一个“该命题为假”陈述的方式。更一般化的， 也可使一个为假的命题变为真，用之前提到过的双重否定规则。所以可以这么说， 符号使一个真命题变为假命题，使一个假命题（根据定义，符号单独出现时不可能，但当做复合命题时可能）变为真命题。我们使用所谓的真值表表示：
真值表是复合命题的新命题的新真值的一种表现方式，它遍历所有可能的参数赋值并标出对应情况的新命题的新真值。 表示true，即 当时的真值为true时， 表示false，即 当时的真值为假。易见这确实覆盖了所有的情况。
F
逻辑方程
为了加深理解，我们可以将“ ”，“ ”之类的符号称为逻辑运算符，他们本身可以视为一个函数。如 ， 。事实上在一些编程语言里就是这样做的， 原形 只是一种“语法便利”，是等价的。之后我们会更有意义的使用运算符是一种函数的这种概念。
现在我们提前涉及一下“逻辑方程”这种概念，正式定义中并不存在这个概念，不过我觉得这使逻辑推理的某些部分变得容易理解。然而比较糟的是，“方程”自己的含义却有些含糊，我们可以把它当做日常的方程来考虑。即给出几个条件去限制另一个条件，会产生一个或几个令“等式”成立的“解”。这里我们看看 是否是原陈述的一个解。
在此之前，再加入一个运算符 符号表示and，并，而且之类的意思。真值表为
F
可以自己测试一下，会发现正像自然语言的里的意思。
列出形式：
查询真值表，发现 仅当 和 都为真时才会出现。所以这里 都为真，这就反映了条件的性质（都为真）。
然后，由 为真得到 为假，然后将这个 的真值代入到 的 中，又由 真值表中当其为真且其中一项为假，则另一项为真的“性质”（可以看得出来的）。得到 为 ，从而，我们证明了 。