Propositional formula
A propositional formula is a formal expression in propositional logic, constructed recursively from propositional variables (such as p, q, or r) and logical connectives, including negation (\neg), conjunction (\wedge), disjunction (\vee), implication (\rightarrow), and biconditional (\leftrightarrow).[1] These formulas represent declarative statements that can be evaluated as true or false under a given truth assignment to the variables, forming the syntactic backbone of propositional logic.[2] The syntax ensures well-formedness through rules: atomic propositions are formulas; if A is a formula, then \neg A is a formula; and if A and B are formulas, then (A \wedge B), (A \vee B), (A \rightarrow B), and (A \leftrightarrow B) are formulas.[3] Propositional formulas enable the systematic analysis of logical inference, where their truth values are determined semantically via truth tables that exhaustively list all possible assignments of truth values (true or false) to the variables.[2] For instance, the formula \neg p \vee q is true unless p is true and q is false, illustrating how connectives define truth-functional relationships.[3] A formula is deemed valid (a tautology) if it evaluates to true under every possible assignment, such as (p \vee q) \leftrightarrow (q \vee p), which captures the commutativity of disjunction.[3] Historically, propositional formulas emerged in the late 19th century as part of the development of modern logic, with key contributions from Gottlob Frege, who formalized connectives and their inferential roles, building on earlier Aristotelian ideas about syllogisms but abstracting away from content to focus on form.[2] This abstraction distinguishes propositional logic from predicate logic, limiting analysis to whole propositions without internal structure.[2] In contemporary applications, propositional formulas underpin automated reasoning in computer science, including satisfiability solving (SAT) for optimization problems and verification in software and hardware design, due to their decidability via exhaustive enumeration.[2] Their simplicity yet expressiveness make them essential for modeling binary decisions in fields like artificial intelligence and philosophy.[2]Fundamentals of Propositions
Definition and Basic Concepts
In logic, a proposition is defined as a declarative statement that expresses a complete thought and possesses a definite truth value, being either true or false but not both.[2] For instance, the sentence "It is raining" qualifies as a proposition because it can be verified as true or false depending on the current weather conditions, while "2 + 2 = 4" is always true as a mathematical fact.[4] Propositions form the foundational units in propositional logic, distinguishing them from questions, commands, or exclamations that lack such binary truth values.[5] A propositional formula, also referred to as a propositional expression, is a finite syntactic expression constructed by combining atomic propositions using logical connectives, without the inclusion of quantifiers or variables that vary over domains.[2] These formulas represent structured logical assertions that can be analyzed for their overall truth conditions based on the truth values of their components.[6] Atomic propositions serve as the simplest building blocks of these formulas, while compound formulas arise from applying connectives to one or more atomic or other compound propositions, enabling the expression of more complex relationships.[5] In formal notation, atomic propositions are typically represented by uppercase letters such as P, Q, or R, allowing for abstract representation of any declarative statement with a truth value.[7] This symbolic approach facilitates rigorous analysis without tying formulas to specific natural language sentences.[8] Propositional formulas are essential for modeling binary decision-making and truth-functional structures across disciplines, including computer science for designing digital circuits and verifying program correctness, philosophy for evaluating deductive arguments, and mathematics for constructing proofs in discrete structures.[9][2] Their simplicity in handling only truth values makes them a cornerstone for understanding more advanced logical systems.[10]Relation to Predicate Logic
Predicate logic, also known as first-order logic, extends propositional logic by incorporating predicates, variables, and quantifiers such as ∀ (universal quantification) and ∃ (existential quantification). In this framework, predicate formulas build upon propositional structures but allow for the expression of relations between objects and properties within a domain, enabling more complex statements about generality and specificity.[11] Propositional formulas represent a special case within predicate logic, where atomic propositions—such as P or Q—are treated as indivisible units without internal structure, relying solely on connectives like conjunction (∧) or negation (¬) to form compound statements. For instance, a propositional formula like [P](/page/P′′) \land [Q](/page/Q) captures the truth-functional combination of two atomic propositions but cannot specify the objects or relations they involve. In contrast, predicate logic treats such atoms as predicate applications, such as Man(x) for "x is a man," allowing formulas like \forall x (Man(x) \to Mortal(x)), which asserts "all men are mortal" by quantifying over a domain of individuals.[2][11] This extension highlights key limitations of propositional logic: it lacks the expressive power to handle quantifications or relations, making it unable to formalize statements involving variables or universal claims, such as "there exists a mortal man" (\exists x (Man(x) \land [Mortal](/page/Mortal)(x))). Propositional logic thus serves as a foundational but restricted subset, suitable for analyzing sentence-level inferences without delving into sub-sentential components.[2] Historically, propositional logic's development in the 19th century, building on earlier Aristotelian syllogistics, provided a simplified lens for studying logical connectives, paving the way for Gottlob Frege's 1879 introduction of predicate logic in Begriffsschrift, which integrated quantification to address these expressive gaps. This simplification allowed early logicians to isolate truth-functional aspects before tackling the fuller machinery of predicate logic, as formalized in Kurt Gödel's 1930 completeness theorem for first-order systems.[12][11]Components of Formulas
Propositional Variables
Propositional variables, also known as atomic propositions or sentence letters, are fundamental symbols in propositional logic that serve as placeholders for simple declarative statements capable of being true or false. These variables represent unspecified propositions without specifying their content, allowing the focus to remain on the structure of logical expressions rather than particular facts about the world. By convention, propositional variables are typically denoted using lowercase letters such as p, q, r or uppercase letters with numerical subscripts like P_1, P_2, \dots, drawn from a countable infinite set to ensure an ample supply for any formula construction. This notation facilitates clear distinction among variables, where each distinct symbol is treated as representing a potentially unique proposition. The primary role of propositional variables is to formalize logical arguments by abstracting away from concrete propositions, enabling generalization and analysis of inference patterns across diverse contexts. For example, one might substitute p with the proposition "Snow is white" and q with "Grass is green" to instantiate a general schema, thereby testing the logical validity of relationships without reliance on the actual truth of those specific statements. This abstraction underscores how distinct variables maintain independence, as they can be assigned differing truth values in any given interpretation.Logical Connectives
Logical connectives, also known as propositional connectives, are operators that combine propositional variables to form compound propositions in propositional logic.[13] These connectives allow the construction of complex statements from simpler ones, serving as the building blocks for expressing relationships between propositions.[14] The standard unary connective is negation, denoted by ¬ or ~, which reverses the truth value of its operand: ¬P is true if and only if P is false.[14] The common binary connectives include conjunction (∧ or AND), disjunction (∨ or OR), implication (→ or ⇒), and biconditional (↔ or ⇔). Their intuitive meanings are as follows:| Connective | Symbol(s) | Intuitive Meaning |
|---|---|---|
| Conjunction | ∧ | True only if both operands are true (e.g., P ∧ Q holds when P and Q both occur).[14] |
| Disjunction | ∨ | True if at least one operand is true (inclusive OR, e.g., P ∨ Q holds if either or both occur).[14] |
| Implication | →, ⇒ | True unless the first operand is true and the second is false (e.g., P → Q means if P then Q).[14] |
| Biconditional | ↔, ⇔ | True if both operands have the same truth value (e.g., P ↔ Q means P if and only if Q).[14] |
Syntax and Construction
Inductive Definition
A propositional formula is defined inductively as the smallest set of expressions closed under a base case and specific formation rules using logical connectives.[19] In the base case, the atomic formulas consist of propositional variables, such as p, q, r, and the truth constants [\top](/page/top) (true) and \bot (false).[19] For the inductive step, given any formulas \phi and \psi, the following compound expressions are also formulas: the negation \neg \phi; the conjunction (\phi \wedge \psi); the disjunction (\phi \vee \psi); the implication (\phi \to \psi); and the biconditional (\phi \leftrightarrow \psi).[19][20] Parentheses are required around compound expressions to ensure structural clarity and unambiguous nesting, though the outermost pair may sometimes be omitted in informal notation.[19][20] The set of all propositional formulas is thus the closure under these rules, meaning it includes exactly those expressions generated by starting from atomic formulas and repeatedly applying the inductive steps.[19] To illustrate, consider constructing the formula (([p](/page/P′′) \wedge [q](/page/Q)) \to [r](/page/R)):- Base: [p](/page/P′′), [q](/page/Q), and [r](/page/R) are atomic formulas.
- Inductive: ([p](/page/P′′) \wedge [q](/page/Q)) is a formula, as it applies conjunction to [p](/page/P′′) and [q](/page/Q).
- Inductive: (([p](/page/P′′) \wedge [q](/page/Q)) \to [r](/page/R)) is a formula, as it applies implication to ([p](/page/P′′) \wedge [q](/page/Q)) and [r](/page/R).[19]
Well-Formed Formulas
In propositional logic, a well-formed formula (WFF), also known as a well-formed expression, is a finite string over a specified alphabet that adheres strictly to the syntactic rules of the language, ensuring it can be unambiguously interpreted as a logical expression.[21] These rules are derived from the inductive definition of formulas, which builds expressions recursively from basic components.[22] Unlike semantically valid formulas, which are true under all interpretations, WFFs concern only syntactic correctness and do not imply truth or falsity.[23] The alphabet for propositional formulas consists of propositional variables (typically denoted by uppercase letters such as P, Q, or lowercase p, q), logical connectives (including negation \neg or \sim, conjunction \land, disjunction \lor, implication \to or \Rightarrow, and equivalence \leftrightarrow or \Leftrightarrow), and parentheses ( and ) to enforce grouping.[21][22] A string qualifies as a WFF through a recursive verification process: atomic formulas, such as single propositional variables (e.g., P), are WFFs by base case; a negated formula \neg \phi is a WFF if \phi is a WFF; and a compound formula (\phi \circ \psi) is a WFF if \phi and \psi are WFFs and \circ is a binary connective, with parentheses ensuring balanced nesting.[23] This recursion guarantees that every subexpression is itself a WFF, preventing malformed structures. For instance, the expression ((P \to Q) \land R) is a WFF, as it is built by first recognizing [P](/page/P′′) and [Q](/page/Q) as atomic WFFs, forming (P \to Q), then combining it with [R](/page/R) using \land under outer parentheses.[21] In contrast, P \land Q \to R is not a WFF due to missing parentheses, which would render the structure ambiguous and fail the recursive balance check.[22] Another valid example is \neg \neg ([P](/page/P′′) \to [Q](/page/Q)), formed by successive negations of the WFF ([P](/page/P′′) \to [Q](/page/Q)).[23] Well-formedness is preserved under substitution: replacing any propositional variable in a WFF with another WFF (fully parenthesized if compound) yields a new WFF, maintaining syntactic integrity without altering the recursive structure.[22] This property allows for the construction of complex expressions while ensuring all remain syntactically valid.Parsing and Precedence
Parsing propositional formulas requires unambiguous rules to interpret linear strings of symbols, as well-formed formulas may lack sufficient parentheses to dictate grouping.[24] These rules, known as precedence and associativity conventions, establish a standard hierarchy and grouping for logical connectives, allowing consistent evaluation without full parenthesization. The standard precedence order assigns the highest priority to negation (¬), followed by conjunction (∧), then disjunction (∨), and finally implication (→) and equivalence (↔) at the lowest level.[24] For instance, the formula ¬p ∧ q is parsed as (¬p) ∧ q, where negation binds more tightly to p than conjunction does. Similarly, ∧ and ∨ take precedence over →, so p → q ∧ r is interpreted as p → (q ∧ r). Associativity determines grouping when multiple connectives of the same precedence appear consecutively. Conjunction and disjunction are left-associative, meaning p ∧ q ∧ r parses as (p ∧ q) ∧ r, and likewise for ∨.[24] In contrast, implication and equivalence are right-associative, so p → q → r is parsed as p → (q → r).[25] These conventions apply only to syntactic parsing and do not alter the semantic commutativity of ∧ and ∨, where p ∧ q is equivalent to q ∧ p despite the fixed left-to-right grouping. While precedence and associativity reduce the need for parentheses in many cases, fully parenthesized formulas eliminate all ambiguity and are required for non-standard interpretations. For example, the ambiguous string p ∧ q → r could be intended as (p ∧ q) → r or p ∧ (q → r), necessitating explicit parentheses to specify the grouping.[24] Adhering to these conventions ensures that well-formed formulas are parsed consistently across logical systems.Semantics and Evaluation
Truth Values and Assignments
In propositional logic, the semantics are bivalent, meaning every atomic proposition assumes exactly one of two truth values: true (often denoted as 1, T, or \top) or false (denoted as 0, F, or \bot).[26] These truth values form the foundational building blocks for evaluating the truth of more complex formulas.[2] A truth assignment, or valuation, is a function v that assigns to each propositional variable one of these two truth values, thereby specifying a complete interpretation for the variables in a given language.[2] For instance, in a language with variables p and q, one possible assignment might be v(p) = \top and v(q) = \bot.[27] Given n distinct propositional variables, the total number of possible truth assignments is $2^n, as each variable can independently take one of two values.[28] Propositional constants include \top, which evaluates to true under every truth assignment, and \bot, which evaluates to false under every truth assignment.[26] To illustrate, consider the two propositional variables p and q; the four possible truth assignments are enumerated in the following table:| p | q |
|---|---|
| \top | \top |
| \top | \bot |
| \bot | \top |
| \bot | \bot |
Formula Evaluation
The evaluation of a propositional formula under a given truth assignment proceeds recursively, starting from the atomic propositions and building up to compound subformulas using the semantics of the logical connectives.[2] A truth assignment, or valuation, assigns a truth value (true, denoted T, or false, denoted F) to each propositional variable, and this extends inductively to all formulas. For an atomic formula p, the value v(p) is simply the assigned truth value of p. For negation, v(\neg \phi) is T if v(\phi) is F, and F otherwise. For conjunction, v(\phi \wedge \psi) is T if and only if both v(\phi) is T and v(\psi) is T; otherwise, it is F. For disjunction, v(\phi \vee \psi) is T if at least one of v(\phi) or v(\psi) is T; otherwise, it is F. For implication, v(\phi \to \psi) is F only if v(\phi) is T and v(\psi) is F; in all other cases, it is T. For biconditional, v(\phi \leftrightarrow \psi) is T if v(\phi) and v(\psi) have the same truth value, and F otherwise.[29] These semantics for the connectives are often presented via truth tables, which exhaustively list the output truth values for all possible input combinations from the operands. The following table shows the truth tables for the binary connectives, assuming standard truth values T and F:| \phi | \psi | \phi \wedge \psi | \phi \vee \psi | \phi \to \psi | \phi \leftrightarrow \psi |
|---|---|---|---|---|---|
| T | T | T | T | T | T |
| T | F | F | T | F | F |
| F | T | F | T | T | F |
| F | F | F | F | T | T |
Tautologies and Validity
In propositional logic, a tautology is a formula that evaluates to true under every possible truth assignment to its propositional variables. For instance, the formula p \lor \neg p (the law of excluded middle) is a tautology because it holds regardless of whether p is true or false.[2] A valid formula is synonymous with a tautology, particularly in contexts involving logical inference, where it denotes a statement that cannot be false.[2] In contrast, a contradiction is a formula that evaluates to false under every truth assignment, such as p \land \neg p, which is impossible for any value of p.[30] A formula is satisfiable if there exists at least one truth assignment under which it evaluates to true; otherwise, it is unsatisfiable, which is equivalent to being a contradiction.[2] To detect whether a formula is a tautology, contradiction, or satisfiable, one can construct an exhaustive truth table that enumerates all possible assignments for its variables and evaluates the formula in each case. For a formula with n variables, the table has $2^n rows. Consider the formula (p \to q) \lor (q \to p), where \to denotes implication (equivalent to \neg p \lor q). The truth table below demonstrates that it is a tautology, as it yields true in every row:| p | q | p \to q | q \to p | (p \to q) \lor (q \to p) |
|---|---|---|---|---|
| T | T | T | T | T |
| T | F | F | T | T |
| F | T | T | F | T |
| F | F | T | T | T |
Algebraic Structure
Propositional logic possesses a rich algebraic structure, specifically that of a Boolean algebra. The carrier set consists of equivalence classes of propositional formulas under logical equivalence, where two formulas are equivalent if they have the same truth value in every interpretation. The Boolean operations are defined by the logical connectives: conjunction \wedge as meet, disjunction \vee as join, negation \neg as complement, with constant formulas \top (tautology) as the top element and \bot (contradiction) as the bottom element. This structure captures the semantic relationships among formulas algebraically.[32]Propositional Calculus
The propositional calculus provides a formal deductive framework for reasoning about propositional formulas, where theorems are derived from a set of axioms using specified inference rules.[33] This system ensures that valid inferences in propositional logic can be mechanically justified through syntactic manipulation alone.[34] In this calculus, propositions are treated algebraically, with logical connectives functioning as operations that combine atomic propositions or compound formulas to yield new formulas.[33] The connectives, such as implication (→), negation (¬), conjunction (∧), and disjunction (∨), form the basis for constructing the algebra, allowing the expression of complex relationships among truth-bearing statements.[34] A prominent formulation is the Hilbert-style system, which relies on a finite set of axiom schemas for the implicational and negation fragments of propositional logic.[33] The core axiom schemas include:- p \to (q \to p)
- (p \to (q \to r)) \to ((p \to q) \to (p \to r))
- (\neg p \to \neg q) \to (q \to p)
- p \to ((p \to p) \to p) (axiom 1, substituting q with p \to p)
- (p \to ((p \to p) \to p)) \to ((p \to (p \to p)) \to (p \to p)) (axiom 2, substituting appropriately)
- p \to (p \to p) (modus ponens from 1 and 2)
- (p \to p) \to (p \to (p \to p)) \to (p \to p) (axiom 1, substituting q with p \to p)
- p \to (p \to p) \to (p \to p) (modus ponens from 3 and 4)
- p \to p (modus ponens from 3 and 5)