Propositional logic examines statements that are either true or false, focusing on how these are combined using operators. It forms a foundational sub-field of mathematical logic alongside first-order logic, higher-order logic, and others. This formal system represents and analyzes statements with definite truth values. Syntax defines the formal structure with propositions and logical connectives. Semantics determines truth values using truth tables, identifying tautologies and contradictions. Equivalences include laws like De Morgan's and distributive laws for simplification. Inference Rules such as modus ponens enable step-by-step proofs. Normal Forms provide standard representation methods like CNF and DNF. Proof Techniques include contradiction and direct proof methods to validate arguments. This logical system finds applications across mathematics, computer science (circuit design, program verification), artificial intelligence (knowledge representation), philosophy, and many other fields.
Basic laws of Propositional Logic
Understanding Propositional Logic Laws
Propositional logic provides a powerful framework for formal reasoning, and at its core are several fundamental laws that help us manipulate logical expressions. On this page we aggregated a summary of these laws and rules. They may be grouped into families based on their logical functions: Basic Operators: Identity, Domination, and Idempotent laws establish how basic operations behave with constants and themselves Structural Laws: Commutative, Associative, and Distributive laws govern how expressions can be rearranged Transformation Rules: Double Negation, De Morgan's Laws, and Absorption laws help convert between different logical forms Semantic Principles: Negation laws represent fundamental truths about contradictions and the law of excluded middle Implications: Contrapositive and Conditional laws help reason through logical implications Special Operators: Exclusive OR laws define the behavior of XOR operations Advanced Principles: Resolution, Monotonicity, and Peirce's Law provide powerful tools for formal proofs Each law is presented with its formal notation, a plain-language explanation, and its relevant topic area (such as Equivalences, Semantics, Normal Forms, or Proof Techniques). This organization makes it easier to find specific laws when constructing proofs or simplifying expressions. Whether you're working on simplifying complex logical statements, converting expressions to normal forms, or building formal proofs, these laws provide the essential toolkit for manipulating propositional logic expressions with confidence and precision.
The syntax of propositional logic establishes the formal rules for constructing well-formed formulas—similar to how grammar determines what constitutes a valid sentence in natural language. Unlike semantics, which concerns itself with truth and meaning, syntax focuses purely on form and structure. It defines the alphabet of symbols, the valid combinations of these symbols, and the rules for building increasingly complex expressions, all without reference to what these expressions might represent in the real world. Syntax answers the fundamental question: "Is this a properly formed logical statement?" regardless of whether that statement is true, false, or meaningful.
Propositional logic syntax is built from atomic propositions (e.g., 'P', 'Q', 'R') — the indivisible units of meaning. These are combined using logical connectives such as '¬', '∧', '∨', '→', and '↔', which form more complex expressions. A well-formed formula (WFF) is any expression built according to the formation rules, which define how formulas can be recursively constructed from simpler components. Parentheses are essential for maintaining clarity, especially when multiple connectives are involved, ensuring expressions are structurally unambiguous.
In addition to these core concepts, syntax trees are used to visually represent the hierarchical structure of formulas, and structural induction is a key proof method for demonstrating properties of formulas (e.g., that all formulas have finite depth). These tools help validate and analyze the form of logical statements without reference to their truth value — staying fully within the domain of syntax.
In propositional logic, semantics refers to the study of the meaning of logical formulas. While syntax concerns itself with the formal structure and the rules for constructing well-formed formulas (WFFs), semantics addresses how these formulas are interpreted and how their truth-values are determined within a given model. The semantic analysis of logic allows us to rigorously define concepts such as truth, satisfiability, validity, and logical equivalence, which are central to formal reasoning.
Truth values: T (true), F (false) Interpretations / Models: Assignments of truth values to variables Truth tables: Show truth values under all possible interpretations Semantic equivalence: e.g., P → Q ≡ ¬P ∨ Q Tautology / Contradiction / Contingency Model: An interpretation where a formula is true Satisfiability: Whether a formula is true in some interpretation
Propositions in classical logic have several important properties. Here are a few key ones:
1.Logical Equivalence:
Two propositions P and Q are logically equivalent (denoted P≡Q) if they have the same truth value in every possible interpretation. Example: P∨Q≡Q∨P (Commutativity of disjunction) Read more about equivalence.
2.Consistency & Inconsistency:
A set of propositions is consistent if it is possible for all of them to be true at the same time. A set of propositions is inconsistent if they cannot all be true simultaneously (i.e., they lead to a contradiction). Example: The set {"It is raining", "It is not raining"} is inconsistent. The set {"It is raining", "The ground is wet"} is consistent.
3.Implication (Entailment / Logical Consequence):
A proposition Q is a logical consequence of P (denoted P⊨Q) if whenever P is true, Q must also be true. Example: P= "It is raining." Q= "The ground is wet." If P is true, then Q logically follows (assuming no weird circumstances). Read more about logical implications.
4. Independence:
A proposition is independent of another if neither one logically determines the truth value of the other. Example: "It is raining" and "The stock market is up" are independent because knowing one does not tell us anything about the other.
5.Validity & Invalidity:
A proposition is valid if it is true in all possible interpretations (i.e., a tautology). A proposition is invalid if it is not true in all interpretations (i.e., it is either a contingency or a contradiction).
Validity is an important concept in logic because valid statements are universally true, meaning they hold regardless of the truth values of their components.
6.Satisfiability & Unsatisfiability:
A proposition is satisfiable if there is at least one interpretation where it is true (i.e., a tautology or a contingency). A proposition is unsatisfiable if it is false in all possible interpretations (i.e., a contradiction).
Proof System
Hilbert Proof System in Propositional Logic
A. Axioms (3 Schemas)
A1: A → (B → A)
Self-evidence axiom: Any proposition implies that any other proposition implies the first one. This captures the idea that if something is true, it remains true regardless of what other assumptions you make.
A2: (A → (B → C)) → ((A → B) → (A → C))
Distribution axiom: If A implies that B implies C, and A also implies B, then A must imply C directly. This enables chain reasoning and logical distribution.
A3: (¬B → ¬A) → (A → B)
Contrapositive axiom: If the negation of B implies the negation of A, then A implies B. This establishes the logical equivalence between a statement and its contrapositive.
B. Premises
Definition
Premises are the starting assumptions in a proof. They serve as the foundation from which conclusions are derived.
Types:
1. Logical premises: The axiom schemas above, universally valid 2. Domain premises: Specific assumptions given for a particular proof 3. Temporary premises: Assumptions made for conditional or indirect proofs
Role in proofs:
Premises establish the initial truth conditions. All subsequent steps must follow logically from these starting points using valid inference rules.
C. Inference Rules
Modus Ponens (MP)
Rule: From A and A → B, derive B Purpose: The only inference rule needed in pure Hilbert systems. It allows you to detach the consequent of an implication when you have both the implication and its antecedent.
Substitution (Implicit)
Rule: Replace variables in axiom schemas with any well-formed formulas Purpose: Generates specific instances of the general axiom patterns for use in particular proofs.
Proof Construction
A proof is a finite sequence of formulas where each formula is either:
The system is complete (proves all tautologies) and sound (proves only tautologies).