目录
布拉格查理大学
布拉格查理大学（Univerzita Karlova v Praze；Universitas Carolina in Prague）成立于1348年，是捷克乃至中欧最古老的大學，也是捷克最大的大学。 布拉格大学是欧洲顶尖大学科英布拉集团、欧洲大学联盟以及Europaeum成员。布拉格大学在历史上诞生过很多著名学者和科学家。像第谷·布拉赫，约翰内斯·开普勒，伯纳德·博尔扎诺，恩斯特·马赫和阿尔伯特·爱因斯坦等都曾在此探索到他们的发现。布拉格大学的学生和教授在历史上诞生过四位诺贝尔奖获得者。 它已发展成了一所综合性的世界闻名的高等学府，现有五万四千名学生在此就读。 布拉格查理大学属于世界顶级大学，根据上海交通大学的世界大学学术排名，布拉格查理大学名列世界300强和欧洲100强（根据科学研究，主要是获诺贝尔奖情况）。.
切消定理
切消定理是确立相继式演算重要性的主要结果。它最初由格哈德·根岑在他的划时代论文《逻辑演绎研究》对分别形式化直觉逻辑和经典逻辑的系统LJ和LK做的证明。切削定理声称在相继式演算中，拥有利用了切规则的证明的任何判断，也拥有无切证明，就是说，不利用切规则的证明。 相继式是与多个句子有关的逻辑表达式，形式为"A, B, C, \ldots \vdash N, O, P"，它可以被读做"A, B, C, \ldots证明N, O, P"，并且（按Gentzen的注释）应当被理解为等价于真值函数"如果（A & B & C \ldots）那么（N or O or P）"。注意LHS（左手端）是合取（and）而RHS（右手端）是析取（or）。LHS可以有任意多个公式；在LHS为空的时候，RHS是重言式。在LK中，RHS也可以有任意数目的公式--如果没有，则LHS是个矛盾，而在LJ中，RHS只能没有或有一个公式：在右紧缩规则前面，允许RHS有多于一个公式，等价于容许排中律。注意，相继式演算是相当有表达力的框架，已经为直觉逻辑提议了允许RHS有多个公式的相继式演算，而来自Jean-Yves Girard的逻辑LC得到了RHS最多有一个公式的经典逻辑的更加自然的形式化；逻辑和结构规则的相互作用是它的关键。 "切"是在相继式演算的正规陈述中的一个规则，并等价于在其他证明论中的规则变体，给出 和 你可以推出 就是说，在推论关系中"切掉"公式"C"的出现。 切消定理声称（对于一个给定的系统）使用切规则的任何相继式证明也可以不使用这个规则来证明。如果我们认为(D, E, \ldots)是一个定理，则切消简单的声称用来证明这个定理的引理C可以被内嵌（inline）。在这个定理的证明提及引理C的时候，我们可以把它代换为C的证明。因此，切规则是可接纳的。 对于用相继式公式化的系统，分析性证明是不使用切规则的证明。这种证明典型的会很长，当然没有必要这么做。在散文《不要消除切呀!》中，George Boolos展示了可以使用切在一页中完成的推导，而它的分析性证明要耗尽宇宙的寿命来完成。 这个定理有很多丰富的推论。一旦一个系统被证明有切消定理，这个系统通常立即就是一致的。这个系统通常也有子公式性质，这是达成证明论语义的重要性质。切削是证明插值定理的最强力工具。基于归结原理的完成证明查找的可能性，导致Prolog编程语言的本质洞察，依赖于在适当的系统中接纳切规则。.
查看 格哈德·根岑和切消定理
直觉主义逻辑
觉主义逻辑或构造性逻辑是最初由阿蘭德·海廷开发的为鲁伊兹·布劳威尔的数学直觉主义计划提供形式基础的符号逻辑。这个系统保持跨越生成导出命题的变换的证实性而不是真理性。从实用的观点，也有使用直觉逻辑的强烈动机，因为它有存在性质，这使它还适合其他形式的数学构造主义。.
相干逻辑
干逻辑，也叫做相关逻辑，是一类非经典亚结构逻辑，它在蕴涵上施加了特定限制。（一般但不完全的，澳大利亚逻辑学家称之为relevant logic，其他说英语的逻辑学家称之为relevance logic）。 相干逻辑致力于捕获蕴含在经典真值泛函逻辑中被“实质蕴涵”算子所忽略的那些方面。这个想法不是新的：它导致C.
查看 格哈德·根岑和相干逻辑
相继式
在证明论中，相继式是对在规定演绎的演算的时候经常用到的可证明性的形式陈述。.
查看 格哈德·根岑和相继式
相继式演算
在证明论和数理逻辑中，相继式演算（又译矢列演算、矢列式演算）是众所周知的一阶逻辑（和作为它的特殊情况的命题逻辑）的演绎系统。这个系统也叫做LK系统，用以区别于后来建立的有时也叫做相继式演算的类似风格的各种其他系统。另一个给这种系统的术语是Gentzen系统。 相继式演算LK由Gerhard Gentzen介入为研究自然演绎的工具。它已经变成构造逻辑推导的非常有用的演算。它的名字得来自德语的Logischer Kalkül，意思是"逻辑演算"。相继式演算是关于这个主题的很多研究所选择的方法。.
查看 格哈德·根岑和相继式演算
邏輯語義學
我们在论证中可能遇到的各种句子/判决的有效性条件依赖于它们的意义，所以负责任的逻辑学家不能完全避免提供某种处理这些句子的意义的需求。逻辑的语义指称逻辑学家已经介入来理解和确定他们感兴趣的意义部分的方式；逻辑学家在传统上只对是命题的句子感兴趣，它是适合逻辑操纵的理想的句子。 直到现代逻辑出现之前，亚里士多德的工具论特别是解释篇，提供了理解逻辑意义的基础。量化的介入需要解决多重普遍性问题，表现出了亚里士多德的逻辑所支配的主词-谓词分析不能处理的那些种类，尽管对词项逻辑的兴趣正在复兴，尝试找到符合亚里士多德三段论精神并且使用基于量词的现代逻辑一般性的演算。.
查看 格哈德·根岑和邏輯語義學
重复独立发现发明列表
历史学及社会学上对于科学界「重复独立发现发明」的现象各有评论。罗伯特·金·莫顿将「重复发现」定义为各自独立开展研究的科学家得出相似的发现的情况。「有些发现是同时的，或者几乎同时的；而有些科学家得出的新发现早在几年前就有人在他不知情的情况下捷足先登。」 重复独立发现发明最常见的例子是微积分、氧气和进化论的发现及发明。微积分于17世纪由牛顿、莱布尼茨等人各自独立发明；氧气于18世纪由舍勒、普里斯特里、拉瓦锡各自独立发现；进化论则是于19世纪，由达尔文和华莱士分别独立提出。 然而，重复独立发现发明并非只限于科学研究的巨头之间。莫顿认为科学发现的常态应该是由多人独立发现，而不是由一个个人或团体独一无二地发现。 莫顿还对比了「重复发现」与「独特发现」，「独特发现」是指单一的一位科学家或一组合作的科学家得出的发现。.
量化 (数理逻辑)
在语言和逻辑中，量化是指定一个谓词的有效性的广度的构造，就是说指定谓词在一定范围的事物上成立的程度。产生量化的语言元素叫做量词。结果的句子是量化的句子，我们称我们已经量化了这个谓词。量化在自然语言和形式语言中都使用。在自然语言中，量词的例子有“所有”、“某些”；“很多”、“少量”、“大量”也是量词。在形式语言中，量化是从旧公式产生新公式的公式构造子（constructor）。语言的语义指定了如何把这个构造子解释为一个有效性的广度。量化是变量约束操作的实例。 在谓词逻辑的两类基本量化是全称量化和存在量化。这些概念被更详细的叙述于在单独文章中；下面我们讨论适用于二者的特征。其他种类的量化包括唯一量化。.
自然演绎
在数理逻辑中，自然演绎是证明论中尝试提供象“自然”发生一样的逻辑推理形式模型的一种方式。這種方式對比於使用公理的公理系統。.
查看 格哈德·根岑和自然演绎
逻辑学家
逻辑学家是学术研究主题为逻辑学的哲学家，数学家或其他人。下面按姓氏的英语的字母顺序列出著名的逻辑学家。.
查看 格哈德·根岑和逻辑学家
逻辑和谐
逻辑和谐，由 Michael Dummett 命名，是对可以用于给定的逻辑系统的推理规则的假定约束。 逻辑学家格哈德·根岑提议了逻辑连结词的意义可以用把它们介入到论述中的规则给出。例如，如果你相信“天是蓝的”并且还相信“草是绿的”，则你可以如下这样介入逻辑连接词“与”: “天是蓝的 AND 草是绿的”。Gentzen 的想法是拥有这样的规则就是对你的词语，至少对特定词语的给出意义的东西。这个想法也关联于维特根斯坦的格言，在很多情况下我们可以说意义是使用。多数当代逻辑学家偏好认为介入规则和除去规则对于表达是同等重要的。在这种情况下，“与”被如下规则所特征化: |- ! 介入: !! colspan.
查看 格哈德·根岑和逻辑和谐
柯里-霍华德同构
柯里-霍華德对应是在计算机程序和数学证明之间的紧密联系；这种对应也叫做柯里-霍華德同构、公式为类型对应或命题为类型对应。这是对形式逻辑系统和公式计算（computational calculus）之间符号的相似性的推广。它被认为是由美国数学家哈斯凯尔·加里和逻辑学家William Alvin Howard独立发现的。.
亦称为 Gentzen，Gerhard Gentzen，根岑。