演绎推理是以前提作为结论的充分依据的推理：如果前提为真且推理有效，结论就不可能为假。它是逻辑学的核心研究对象之一；逻辑学考察使这类推理成立的关系。在通常的论证分析中，演绎论证既可能有效，也可能无效；称其为演绎论证，只是说明它声称为结论提供何种支持，并不保证这种支持确实成立。因此，演绎不同于仅使结论具有可能性的推理。(iep.utm.edu)
有效性与健全性
逻辑有效性关注的是前提与结论之间的关系，而不是前提事实上是否为真。如果不存在任何容许的解释，使一个论证的所有前提为真而结论为假，那么这个论证就是有效的。健全性则增加了一项要求：健全的论证必须有效，并且前提为真。因此，任何健全的论证都有真的结论；但有效的论证如果至少有一个前提为假，其结论仍可能为假。反过来，结论为真也不能证明得出该结论的推理是有效的。(iep.utm.edu)
例如：
- 所有哺乳动物都是动物。
- 所有鲸都是哺乳动物。
- 因此，所有鲸都是动物。
无论用哪些类别替换“哺乳动物”“动物”和“鲸”，只要它们之间的逻辑关系不变，这一推理形式就仍然有效。检验有效性的方法，是寻找前提为真而结论为假的反例，而不只是检查结论是否符合经验。人们常把演绎描述为“从一般到特殊”的推理，但这种描述并不完整：演绎可以将一般陈述、个别陈述，或两者的组合联系起来。(iep.utm.edu)
常见推理形式
在命题逻辑中，字母代表陈述，符号则表示蕴涵、否定等逻辑关系。两种标准形式是：
- **肯定前件式：**由 (P \rightarrow Q) 和 (P)，推出 (Q)。
- **否定后件式：**由 (P \rightarrow Q) 和 (\neg Q)，推出 (\neg P)。
例如，如果某设备的规格说明指出，指示灯亮起意味着电路处于工作状态，那么由指示灯亮起就可以推出电路正在工作。在这一前提下，该推理是有效的；至于这个前提是否准确描述了设备，则是另一个问题。(plato.stanford.edu)
三段论将关于类别的陈述联系起来，上述关于鲸的例子就是如此。一阶逻辑将形式分析扩展到谓词、关系以及“每个”“有些”等量词，从而能够处理那些仅用完整陈述作为单位无法充分表达其结构的演绎推理。(plato.stanford.edu)
一种重要的谬误是肯定后件：由 (P \rightarrow Q) 和 (Q)，得出 (P)。令 (P) 为假、(Q) 为真，就能证明这一形式无效：此时两个前提都为真，结论却为假。条件命题保证当前件成立时，后件也成立；它并不一定意味着该前件是后件成立的唯一途径。(iep.utm.edu)
形式后承与证明
演绎既可以通过研究解释与真值的语义学来考察，也可以通过形式推导来考察。模型论用 (\Gamma \models C) 表示后承关系：每一个满足 (\Gamma) 中各前提的模型，也都满足 (C)。证明论研究由明确规则支配的推导；(\Gamma \vdash C) 表示，在某个指定系统中，可以由这些前提证明 (C)。(plato.stanford.edu)
形式证明记录各个推理步骤，使其能够依据系统规则接受检验。健全的证明系统只能推导出语义后承；完备的系统则能够推导出其预期适用范围内的每一个语义后承。这些性质针对的是系统，而不是个别论证。自然演绎系统还允许在子证明中引入临时假设，并在确立条件命题或其他结论时解除这些假设。(logic.stanford.edu)
历史发展
在古希腊，亚里士多德在《前分析篇》中建立了系统的演绎理论，尤其是直言三段论理论。他的逻辑学著作影响了后来的希腊注释传统，以及中世纪的阿拉伯语和拉丁语学术传统。他对演绎的理解较为宽泛，不应将其完全等同于传统上称为三段论的那些范围较窄的直言推理形式。(plato.stanford.edu)
现代符号逻辑极大地丰富了用于表达演绎推理的手段。戈特洛布·弗雷格于1879年出版的《概念文字》引入了一套能够分析复杂陈述和量化的形式记法。这一发展使人们能够系统地处理许多超出传统直言三段论范围的推理。(plato.stanford.edu)
其他推理形式与应用
归纳推理所支持的结论，即使在前提为真时也仍可能为假，例如根据观察到的个案作出范围更广的概括。溯因推理为证据提出或支持某种解释，但不保证该解释为真。经典演绎后承具有单调性：增加前提不会使已有的后承关系失效。相比之下，非单调推理允许在新增信息改变结论所获支持时撤回结论。(plato.stanford.edu)
在数学中，数学证明依据定义、公理和先前已确立的结果来证明新的结果。数学归纳法虽然名称中有“归纳”，却是一种演绎证明方法：它通过基本情形和一般性的后继步骤，证明一个陈述对所有相关的自然数成立，而不是根据抽样的实例进行外推。(lean-lang.org)
在计算机科学中，形式演绎是可由机器检查的证明的基础。证明助手可以辅助构建证明，而检查内核则验证由此得到的形式推导。这种验证确立的是结论在所选形式框架内可以推出；它并不能独立证明该框架的假设准确描述了外部情境。(docs.lean-lang.org)