Disjunction introduction

A rule of inference that allows a disjunction to be derived from either of its disjuncts. From P, for example, one may infer P ∨ Q.

Natural deduction: A proof system that represents reasoning through inference rules and explicit assumptions. Disjunction introduction is one of its standard introduction rules.
Proposition: A declarative statement that can be assigned a truth value. The rule begins with a proposition and preserves its truth in a larger formula.
Relevant logic: A family of nonclassical logics requiring premises to be relevant to their conclusions. Unrestrictedly adding an unrelated disjunct conflicts with relevance constraints.
Propositional logic: A formal system for reasoning about propositions combined by logical connectives. Disjunction introduction is a basic derivation rule in propositional proofs.
Disjunction elimination: A rule that derives a conclusion by considering each case of a disjunction. Unlike introduction, it uses a disjunction as a premise rather than adding one.
Logical disjunction: A connective forming a compound proposition that is true when at least one component is true. It is the connective introduced by the rule.
Intuitionistic logic: A constructive logic in which proofs, rather than classical truth tables, ground logical assertions. It permits disjunction introduction, while interpreting disjunction through constructive proof.
Curry–Howard correspondence: A correspondence relating propositions to types and proofs to programs. Disjunction introduction corresponds to constructing a value in a sum type.
Sequent calculus: A formal proof system that derives sequents using rules for logical connectives. Its right-disjunction rules formalize the same inference in a different proof framework.
Inference rule: A formal pattern specifying which conclusions may be drawn from given premises. Disjunction introduction specifies one permitted step from premise to conclusion.

Linked from 4 pages