A,
导出矛盾，从而A得证，这是人工的，不自然的。除非我们验证了一切可能的情形，发现A都不成立，才说A得证。反过来，即使我们验证了所有的可能情况，A都不成立，此时也只能得到A。在自然主义逻辑系统中，A与A是不等价的。在经典的一阶形式推理系统中，矛盾律表达为
若Σ,
A│-B同时Σ,A│-B,
则Σ│-A。
（1*）而在自然主义推理系统中，此推理规则被减弱为两部分：
若Σ, A│-B, 同时Σ，A│-
B，则Σ│-
A。
（2*）若Σ,│-B，同时Σ，│-
B,
则Σ可推出任一A。
（3*）（1*）与（2*）+（3*）的区别从语法上很难理解。建议读者首先尝试证明（1*）成立则（2*）+（3*）成立；然后参阅关于Kripke模型的文献，使用 Kripke 赋值，很容易构造一个 Kripke 模型，其中（2*）+（3*）是有效的，但（1）却不成立。Kripke 模型的构造的主要思想是K 是一个集合，R 是 K 上的一个偏序，K 的每一个元素 v 代表 对部分正原子命题的真值指派。但不立即指派真值给原子公式的否定，对一个原子命题δ，v指派真值给
δ，仅当对所有的u≥v，u对d都没有指派真值。这正是哲学思想的数学实现。从这个赋值定义，读者也能多少理解为什么（2）+（3）不能推出（1）。规则（2）在
Kripke 赋值中的有效性可解释为如果对所有的模型，给Σ中的每一公式指派的都是真，同时给
A 指派的也是真，则 B
及
B 都取真，这是不可能的。所以，对每一个模型，如果对Σ指派的都是真，
A 都不取真，那么我们可以断言，当Σ都取真的时候，按
A 的 Kripke 赋值的定义，
A 一定取真。如上所述，要从语法上理解不同的逻辑系统（尽管在语义上,哲学解释上的巨大差异是很明显的）不是一件很容易的事。Gentzen 的串形演算的优点之一就是要在其逻辑框架下描述直觉主义的逻辑系统就十分简明、清楚。
直觉主义的串形演算系统中，接受同样的恒等式 C│- C , C是任一公式。任一 8.3.2 中1的规则，必须加上一个限制：任一规则，它的前提含一个或者两个串形， 而串形的右边只允许含最多一个公式 。读者可以尝试按这个规定逐个将规则改写成直觉主义的逻辑推理规则。注意，有些规则是不可能改写的，此时只能废除该规则。例如结构规则中的 RX 、RC 就必须废除。另外，逻辑规则中的 L∨应写成
（结论中只含一个 B, 而不是两个 B ）。
这里我们对直觉主义逻辑做一个直观的介绍。直觉主义逻辑又称为构造型逻辑，它是在构造性推理中所使用的逻辑。所谓的构造性推理是指：在进行证明时必须是构造性证明。这点可通过对存在性命题的证明清楚地看出，例如，要证明命题：
"存在一个奇素数"。
在古典的推理中，只要证明奇素数的存在性即可证明这个命题；而在构造性证明中，必须找出（构造出）一个既是奇数又是素数，这样才能证明这个命题成立。例如，若证明了"3是一个奇素数"，则证明了"存在一个奇素数"。下面的证明不是构造性证明，只是一个一般性证明：
证明若不存在奇素数，则所有的素数皆是偶数。又因为每>1的素数都可分解为素数的乘积，从而每个>1的自然数都是偶数，矛盾。
在这个证明中，没有构造出一个奇素数，而只是证明了"
（存在奇素数）"不成立，所以直觉主义逻辑认为由"α不真"不能推出"α真"，即α∨α不一定必真，不接受排中律是直觉主义逻辑的一个基本立场。再考察关于自然数n的如下命题：
。在古典逻辑中此命题容易由归纳法证明。但直觉主义逻辑不承认无限归纳法证明，认为无限归纳法永远是在构造中，而没有构造结束的时候。所以，直觉主义逻辑的又一基本立场是不承认无穷集合的存在性。如下的证明是上面命题的一个构造性证明：
对任意的自然数n。
（1） 当n是偶数时，设n = 2m，则
1 + 2 +…+ n
= (1 + n) + (2 + (n - 1)) + … + (m + (m + 1))
= (n + 1) + (n + 1) + … + (2m + 1)
= (n + 1) + (n + 1) + … + (n + 1)
= m(n + 1) =
（2） 当n是奇数时，设n = 2m + 1，则
1 + 2+…+ n
= (1 + n) + (2 + (n - 1)) +…+((m - 1) + (m + 2)) + (m + 1)
= m(n + 1) + (m + 1) = mn + 2m + 1
= mn + n = (m + 1)n =
构造性证明对计算机科学很有用，因为计算机所做的工作都是构造性的，因而有人认为直觉主义逻辑比古典逻辑、古典数学更适合于作为计算机科学的框架。