Propositional logic Created 2026-09-24 Updated 2026-10-14
Propositional logic studies reasoning with whole propositions represented by letters such as and , and propositional formulas built from them using logical connectives. The classical two-valued, truth-functional presentation below assigns each primitive proposition either true or false: each compound value depends only on its component values. This is classical propositional logic; other systems, including Intuitionistic propositional logic, have different semantics and rules.
Starting with and , one can build by logical negation, by logical conjunction, by logical disjunction, and by logical implication, then combine these into larger propositional formulas. Parentheses specify the construction: has logical conjunction as its outermost logical connective. Primitive propositions have no internal structure in this language; a first-order formula can additionally describe objects and quantify over them. The formation rules are given in forall x: Calgary, chapter 6.
The following truth table shows the four basic logical connectives. Logical disjunction is inclusive: is true when either or both inputs are true. Classical logical implication has exactly the same values as ; its only false row has true and false. These truth conditions are specified in forall x: Calgary, chapter 9.
Evaluate from the inside out: first the logical implication, then the outer logical conjunction. The final column also tests the logical implication expressing the modus ponens rule:At , the logical implication is false, so the logical conjunction is false. The abstract syntax tree below separates the construction of the propositional formula from the values propagated through it. Both occurrences of receive the same value from the Boolean valuation. With the opposite assignment , the logical implication is true but the logical conjunction is still false because its second input is false. Recursive evaluation and exhaustive truth tables are explained in forall x: Calgary, chapter 11.
The last column is always true: is a tautology. This expresses the logical validity of the modus ponens rule: whenever both premises and are true, is true. It does not say the premises are true under every Boolean valuation; their logical conjunction is true only on the first row. For a short natural deduction proof outline, assume , extract both conjuncts, apply the implication elimination rule to obtain , then discharge the assumption by the implication introduction rule. See forall x: Calgary, sections 17.3–17.5.
Three tests answer different questions: Boolean satisfiability requires at least one true row, a tautology requires every row true, and a contradiction has every row false. Thus is a tautology, is a contradiction, and is satisfiable but not a tautology: it is true only at . See forall x: Calgary, sections 12.1–12.4.
Propositional logic is useful because an inference pattern can be checked once and reused for many choices of propositions. Its beauty is that a finite truth table completely settles classical truth-functional questions about a fixed propositional formula. But logical validity does not verify real atomic claims. If means “the switch is closed” and means “the lamp is lit”, a valid use of the modus ponens rule still requires establishing its premises about the apparatus; the truth table supplies neither an observation nor a causal explanation. See forall x: Calgary, chapter 2 and chapter 10.
Set difference Created 2026-10-05 Updated 2026-10-14
The set difference keeps the set elements of that do not belong to :Thus set difference combines logical conjunction (AND) with logical negation (NOT): pass the first condition and fail the second. The definition applies to any two sets; need not be a subset of .
For and , the two orders give different answers:The common member is removed in both directions. A database filter illustrates the usefulness: if is the set of records matching the first condition and the set matching the second, selects records matching the first but not the second. The Venn diagram in set union shades both directions separately.
The name relative complement emphasizes that the ambient set is : is the complement of within . If a larger universal set contains and , then . Changing that larger universal set does not change the set difference, because membership still requires belonging to . In ZF the set difference exists by the axiom schema of separation. It also gives relative complements within a fixed tuple domain in finite relation closure for set-theoretic coding.
Set intersection Created 2026-09-24 Updated 2026-10-14
The intersection keeps exactly the set elements common to both sets:Membership in an intersection therefore uses logical conjunction (AND). For and , the only shared member is , so . The Venn diagram in set union shades only the overlap for this operation.
An intersection is useful when every requirement must hold. If and are the sets of database records passing two separate conditions, their intersection gives the records passing both. Similarly, satisfying two equations requires belonging to the intersection of their solution sets. The same membership rule applies even when the objects have entirely different meanings.
For a family of sets, the intersection contains exactly the set elements belonging to every set :Here universal quantification expresses “every”. If all the sets lie within a fixed universal set , the intersection over no indexing members is defined to be : there are no requirements to fail. This convention depends on specifying . By contrast, intersecting with the empty set always gives .
Stability of a formula under double negation 2026-10-05
A first-order formula is stable when intuitionistic first-order logic proves . Double negations and logical falsity are stable. Logical conjunction of stable first-order formulas is stable; a logical implication is stable when its consequent is stable; and universal quantification preserves stability. For logical implication, from and , assuming contradicts the first hypothesis, giving and then . For universality, obtain from for arbitrary , then use stability and generalize.

