Definition
Propositional logic is the part of Logic in which formulas are built from propositional variables using logical connectives, without quantification over individuals. It studies how compound propositions are formed and how they may be proved or evaluated.
This note records the propositional rules themselves. For the general proof-theoretic perspective on introduction and elimination rules, assumption discharge, normalization, and related metatheory, see Natural deduction.
Syntax
Starting from propositional variables , formulas are generated by connectives such as
and often also negation , either as a primitive connective or as an abbreviation for .
Judgments have the form
where is a context of assumptions.
Deductive system
Propositional logic can be presented by different proof systems, including Natural deduction and sequent calculi.
Structural rules
In natural deduction, one works implicitly with structural rules on contexts. For example, thinning may be written as
and similarly one usually allows exchange and contraction on assumptions.
Intuitionistic fragment
Intuitionistic propositional logic uses the same basic propositional connectives, but its proof theory omits specifically classical principles.
In natural deduction, the characteristic intuitionistic rules include (for arbitrary propositions and contexts ):
\qquad \dfrac{\Gamma \vdash A \land B}{\Gamma \vdash A} \qquad \dfrac{\Gamma \vdash A \land B}{\Gamma \vdash B}$$ $$\dfrac{\Gamma \vdash A}{\Gamma \vdash A \lor B} \qquad \dfrac{\Gamma \vdash B}{\Gamma \vdash A \lor B} \qquad \dfrac{\Gamma \vdash A \lor B \qquad \Delta, A \vdash C \qquad \Theta, B \vdash C}{\Gamma, \Delta, \Theta \vdash C}$$ $$\dfrac{\Gamma, A \vdash B}{\Gamma \vdash A \to B} \qquad \dfrac{\Gamma \vdash A \qquad \Delta \vdash A \to B}{\Gamma, \Delta \vdash B}$$ $$\dfrac{\Gamma \vdash \bot}{\Gamma \vdash A}$$ These are the core propositional rules on the deductive side. They form the intuitionistic fragment. ## Classical extension Adding [[Law of Excluded Middle|LEM]] turns this into a classical system: $$\dfrac{}{\Gamma \vdash A \lor \neg A}$$ Other classically valid principles include double negation elimination and Peirce's law. ## Semantics In the classical setting, a valuation assigns each propositional variable a truth value. The truth value of a compound formula is then determined by the usual truth tables for the connectives. This yields the usual semantic notions of satisfiability, contradiction, tautology, and logical consequence. For intuitionistic propositional logic, one instead uses semantics such as [[Kripke Semantics]]. ## Relation to type theory Under the [[Curry-Howard Correspondence]], intuitionistic propositional logic corresponds to typed functional calculi. In particular, the implicational fragment corresponds to the [[Simply-Typed Lambda Calculus]]. ## Related Concepts - [[Logic]] - [[Natural deduction]] - [[Method of Enumeration]] - [[Curry-Howard Correspondence]] - [[Simply-Typed Lambda Calculus]]