Describe a branching vertex by the first-order logic sentenceand the existence of a sink by . The directed path has sinks but no branching vertex; the directed cycle has neither sinks nor branching vertices; the directed arborescence has a branching vertex. Thus the following three sentences distinguish the named structures in order:Here are abbreviations for the displayed formulas; replacing them gives sentences in the single-relation first-order signature . Explicitly, says that some vertex has no successor and that no vertex has two distinct successors. The truth table across the three structures is:
| Sentence | |||
|---|---|---|---|
The conditions distinguish these three finite structures; they are not claimed to characterize all directed paths, cycles or trees among arbitrary directed graphs. Only local out-degrees and the presence of a sink are needed, without quantifying over paths of unbounded length.
The two satisfying rows with combine by eliminating , while the remaining satisfying row has . An equivalent disjunctive normal form is thereforeExpanding the logical biconditional into its two implications, and using , gives the conjunctive normal formEach form has exactly the same three satisfying assignments as the original propositional formula.
Propositional logic Created 2026-09-24 Updated 2026-11-05
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.
Propositional proof system 2026-11-05
A propositional proof system specifies efficiently checkable certificates for logical tautologies. In the functional formulation, it is a polynomial-time computable surjection from finite binary strings onto the encoded tautologies: the input is a proof and the output is the formula proved. Soundness means no false formula is output; completeness means every logical tautology has some proof.
For example, a truth table can certify by checking its two assignments. The same method for variables may require rows, so efficient verification in the proof's length does not imply short proofs in the formula's length. Proof complexity asks which formulas require long certificates in particular systems. Searching for a proof and checking a supplied proof are different computational tasks.[ref]
The Relative Efficiency of Propositional Proof Systems by Stephen Cook and Robert A. Reckhow. §1, Definition 1.3 and pp.38–39, proof-system encoding
Razborov–Rudich natural-proofs barrier Created 2026-09-28 Updated 2026-11-05
The Razborov–Rudich natural-proofs barrier connects lower bounds in circuit complexity with the security of pseudorandom function families. Suppose a property of Boolean functions is constructive, large and useful against a class containing the relevant pseudorandom function family.
Query all inputs of a candidate Boolean function, then run the property's membership test on its truth table. Constructivity makes this take time. Largeness gives acceptance probability at least for a uniformly random Boolean function. Usefulness gives rejection for all functions in the chosen small-circuit family at sufficiently large lengths. The property therefore supplies a statistical distinguisher.
A security assumption must cover that running time and distinguishing advantage, at the chosen relation between input length and key length. Security only against polynomial-time algorithms in does not cover a full truth table test. Razborov and Rudich use a stronger quantitative hardness assumption to obtain the barrier against P/poly. The conclusion restricts a form of lower-bound proof under the assumption; it does not settle whether P equals NP.[ref]
Silvio Micali 2026-11-05
Silvio Micali coauthored the construction of pseudorandom function families with Oded Goldreich and Shafi Goldwasser. Their 1986 paper extends pseudorandomness from a generated binary string to a function that can be evaluated repeatedly at chosen inputs.[ref]
How to Construct Random Functions by Oded Goldreich, Shafi Goldwasser and Silvio Micali. function-ensemble construction and security experiment
A short key specifies an efficiently evaluated function even though its full truth table can be exponentially large. The comparison experiment is a single randomly chosen function, so repeated queries must receive consistent answers. That consistency distinguishes function security from supplying fresh independent random bits on every call.
Silvio Micali, portrait published with his University of Waterloo distinguished lecture
. Steven Rudich 2026-11-05
Steven Rudich coauthored the natural proof framework with Alexander A. Razborov. Their 1997 paper identifies a barrier to a broad form of circuit lower bound argument, conditional on a sufficiently strong pseudorandom function family security assumption.[ref]
A property that is efficiently recognizable from a truth table, holds for many random Boolean functions and excludes the target small-circuit class could distinguish pseudorandom function families from random ones. The required security must cover the time spent reading the entire table, which is exponential in the function's input length. The barrier restricts these proof methods under its assumption; it does not prove that circuit lower bounds are impossible.
Truth table Created 2026-09-29 Updated 2026-10-14
A truth table lists a propositional formula's value for every Boolean valuation of its distinct primitive propositions. With primitive propositions, there are rows: each independently receives T or F. Evaluate compound columns from their subexpressions using the classical rules for logical connectives. This is exhaustive checking, so a formula true on every row is valid in classical propositional logic.
For a computed example over the natural numbers, let mean that is an even number and mean . The choices realize respectively : all four possible inputs.
The logical implication and its contrapositive agree on every row; the converse implication differs on two rows. A truth table therefore checks equivalence or supplies a counterexample. Classical truth conditions are given in forall x: Calgary, section 31.2. These two-valued truth tables do not characterize validity in Intuitionistic propositional logic.
Unsatisfiable Boolean formula 2026-10-18
An unsatisfiable Boolean formula has no satisfying assignment. Forthe Boolean valuation falsifies the first Boolean clause, and falsifies the second. Both possible truth values fail, proving
UNSAT. Each Boolean clause alone has a satisfying assignment, but their logical conjunction does not: compatibility is the central issue. By contrast, finding just one failed Boolean valuation for a general Boolean formula only rejects that candidate. Finding one successful Boolean valuation proves SAT; proving UNSAT requires excluding every candidate, possibly with a compact argument rather than a full truth table.


