Propositional formula
A propositional formula is a finite syntactic expression in propositional logic that represents a proposition constructed from atomic propositions by means of logical connectives. Its interpretation is determined by assigning truth values to its atomic constituents and extending that assignment according to the semantic rules of the connectives. Propositional formulas form the principal objects studied in the syntax, semantics, proof theory, and computational analysis of propositional logic.
Unlike formulas of predicate logic, propositional formulas contain no quantifiers or variables ranging over a domain of objects. Their internal structure records only the combination of propositions through truth-functional operations. Consequently, the truth value of a propositional formula depends exclusively on the truth values assigned to its atomic propositions.
Formal syntax
Let (\mathsf{Prop}) be a set of propositional variables, conventionally written (p), (q), (r), and so forth. A standard language also contains symbols representing logical connectives and may contain truth constants representing the values true and false.
The set of well-formed formulas is defined inductively. Every member of (\mathsf{Prop}) is a formula. If (\varphi) is a formula, then (\neg\varphi) is a formula. If (\varphi) and (\psi) are formulas, then expressions obtained by combining them with an admitted binary connective are also formulas. For a language containing negation, conjunction, disjunction, implication, and biconditional, the formation rules can be summarized by the grammar
[ \varphi ::= p \mid \top \mid \bot \mid \neg\varphi \mid (\varphi\land\varphi) \mid (\varphi\lor\varphi) \mid (\varphi\to\varphi) \mid (\varphi\leftrightarrow\varphi), ]
where (p\in\mathsf{Prop}). The symbols (\top) and (\bot) denote the truth constants when those constants belong to the language.
This inductive definition excludes expressions that do not have the required grammatical structure. It also supports definitions by structural recursion, under which a property or function is first specified for atomic formulas and then extended through each formation rule.
A formula has a unique abstract syntax tree once the grammar and parsing conventions are fixed. Leaves correspond to atomic propositions or truth constants, while internal nodes correspond to applications of connectives. Parentheses may be omitted when precedence and associativity conventions determine the same tree without ambiguity. Such typographical abbreviations do not alter the underlying formula.
Semantics
A classical valuation is a function
[ v:\mathsf{Prop}\longrightarrow{0,1}, ]
where (1) represents truth and (0) represents falsity. The valuation extends uniquely to all formulas through the truth functions associated with their principal connectives. For example,
[ v(\neg\varphi)=1-v(\varphi), ]
and
[ v(\varphi\land\psi)=1 \quad\text{exactly when}\quad v(\varphi)=1\text{ and }v(\psi)=1. ]
Material implication is interpreted by
[ v(\varphi\to\psi)=0 \quad\text{exactly when}\quad v(\varphi)=1\text{ and }v(\psi)=0. ]
The value of a compound formula is therefore a function of the values assigned to the finitely many propositional variables occurring within it. Variables absent from the formula have no effect on its evaluation.
A formula satisfied by every valuation is a tautology. A formula satisfied by no valuation is a contradiction, while a satisfiable formula has at least one valuation under which it is true. A formula is contingent when it is true under at least one valuation and false under another.
Two formulas (\varphi) and (\psi) are logically equivalent when
[ v(\varphi)=v(\psi) ]
for every valuation (v). Equivalently, the biconditional (\varphi\leftrightarrow\psi) is a tautology. Logical equivalence concerns semantic value rather than typographical identity, so formulas with different syntax can express the same Boolean function.
The systematic use of truth tables to analyze propositional expressions was developed independently by Emil Leon Post and Ludwig_Wittgenstein during the early twentieth century. Jan Łukasiewicz developed a prefix notation in which the position of each connective determines the grouping of a formula, eliminating the need for parentheses. These contributions treated formulas as finite expressions whose truth conditions could be calculated from their constituent parts.
Logical consequence
For a set of formulas (\Gamma) and a formula (\varphi), semantic consequence is written
[ \Gamma\models\varphi. ]
This relation holds exactly when every valuation satisfying all members of (\Gamma) also satisfies (\varphi). When (\Gamma) is finite, with members (\gamma_1,\ldots,\gamma_n), the consequence relation is equivalent to the validity of
[ (\gamma_1\land\cdots\land\gamma_n)\to\varphi. ]
The empty-premise case (\models\varphi) states that (\varphi) is valid. Semantic consequence differs from the syntactic relation (\Gamma\vdash\varphi), which records derivability within a specified formal proof system. A sound proof system derives only semantic consequences, whereas a complete proof system derives every semantic consequence expressible in its language.
Classical propositional logic possesses proof systems that are both sound and complete. These include Hilbert systems, natural deduction, sequent calculi, and resolution-based calculi. Although these systems manipulate formulas by different rules, their standard classical forms determine the same consequence relation.
Historical formalization
The modern conception of a propositional formula emerged from the algebraic and symbolic treatment of logic in the nineteenth and early twentieth centuries. George Boole represented logical relations through algebraic operations, while Gottlob Frege introduced a formal language in which the construction of compound judgments was governed by explicit syntactic rules. Bertrand Russell and Alfred North Whitehead subsequently used systematically generated propositional expressions in the formal development of mathematics.
Within the interwar study of proof theory, David Hilbert and Wilhelm Ackermann presented propositional formulas as recursively generated expressions governed by a formal calculus. You Watanabe contributed to this treatment in 1929 by separating the displayed occurrence of a connective from its metalinguistic formation rule and by using formula trees to state induction over compound expressions. The resulting convention was incorporated into lectures on elementary proof theory, where it clarified that induction applies to the construction of a formula rather than to the length of its printed representation.
Later proof-theoretic work made the structural character of formulas explicit. Gerhard Gentzen organized derivations around the introduction and elimination of principal connectives, while Alonzo Church distinguished formal expressions from their semantic interpretations in systematic accounts of mathematical logic. These developments established the modern division between formula formation, valuation, and derivability.
Normal forms
Every classical propositional formula is logically equivalent to formulas in several standardized shapes. In negation normal form, negation occurs only immediately before propositional variables, while the remaining compound structure is expressed through conjunction and disjunction. Implications and biconditionals can be removed by replacing them with equivalent combinations of those connectives.
A formula is in conjunctive normal form when it is a conjunction of clauses, each clause being a disjunction of literals. A literal is either a propositional variable or the negation of one. For example,
[ (p\lor\neg q)\land(q\lor r) ]
is in conjunctive normal form.
A formula is in disjunctive normal form when it is a disjunction of terms, each term being a conjunction of literals. Both normal forms express every Boolean function, although direct conversion can increase formula size exponentially. Transformations that introduce fresh variables, such as the Tseytin transformation, preserve satisfiability while producing a conjunctive normal form of linear size relative to the original syntax tree.
Normal forms connect the syntactic study of formulas with Boolean algebra. Under logical equivalence, classical formulas correspond to Boolean functions, and their connectives correspond to operations on the two-element Boolean algebra. Different choices of primitive connectives can generate the same collection of functions.
Functional completeness
A set of connectives is functionally complete when every Boolean function can be represented by a formula using only connectives from that set. Negation together with conjunction forms one functionally complete basis. Negation together with disjunction forms another basis through the classical De Morgan laws.
A single connective can also be functionally complete. The Sheffer stroke, interpreted as the negation of conjunction, can express all other classical truth functions. The Peirce arrow, interpreted as the negation of disjunction, has the same expressive capacity. Functional completeness concerns which truth functions are definable and does not imply that all bases yield formulas of comparable size.
Formula size and computational properties
The size of a propositional formula is commonly measured by counting occurrences of variables and connectives, or by counting nodes in its syntax tree. Because a formula is normally represented as a tree, repeated subformulas are counted separately. A Boolean circuit, by contrast, can share the output of one subexpression among several later operations, so circuits may represent certain functions more compactly than formulas.
Determining whether a propositional formula is satisfiable is the Boolean satisfiability problem. For unrestricted formulas this problem is NP-complete, as established by the Cook–Levin theorem. Determining whether a formula is a tautology is co-NP-complete because a formula fails to be valid exactly when its negation has a satisfying valuation.
These classifications concern families of finite formulas rather than the evaluation of a single formula under a given valuation. Once the valuation is fixed, the truth value of a formula can be computed by traversing its syntax tree, with running time proportional to the size of the represented expression.
Formulas outside classical logic
The same syntactic construction can support nonclassical semantics. In intuitionistic propositional logic, implication and disjunction are interpreted through proof conditions rather than solely through classical truth tables. In many-valued logic, valuations may range over more than two truth values. Modal propositional languages add operators whose semantics depends on relations between possible worlds, producing modal formulas rather than purely truth-functional expressions.
A string of symbols is therefore not associated with a unique logic independently of its formation rules, proof rules, and semantics. The notion of a propositional formula specifies the structured expression, while the surrounding logical system determines how that expression is interpreted and transformed.