Recent from talks
Nothing was collected or created yet.
Logical equality
View on Wikipedia| EQ, XNOR | |
|---|---|
| Definition | |
| Truth table | |
| Logic gate | |
| Normal forms | |
| Disjunctive | |
| Conjunctive | |
| Zhegalkin polynomial | |
| Post's lattices | |
| 0-preserving | no |
| 1-preserving | yes |
| Monotone | no |
| Affine | yes |
| Self-dual | no |
Logical equality is a logical operator that compares two truth values, or more generally, two formulas, such that it gives the value True if both arguments have the same truth value, and False if they are different. In the case where formulas have free variables, we say two formulas are equal when their truth values are equal for all possible resolutions of free variables. It corresponds to equality in Boolean algebra and to the logical biconditional in propositional calculus.
It is customary practice in various applications, if not always technically precise, to indicate the operation of logical equality on the logical operands x and y by any of the following forms:
Some logicians, however, draw a firm distinction between a functional form, like those in the left column, which they interpret as an application of a function to a pair of arguments — and thus a mere indication that the value of the compound expression depends on the values of the component expressions — and an equational form, like those in the right column, which they interpret as an assertion that the arguments have equal values, in other words, that the functional value of the compound expression is true.[citation needed]
Definition
[edit]Logical equality is an operation on two logical values, typically the values of two propositions, that produces a value of true if and only if both operands are false or both operands are true.
The truth table of p EQ q (also written as p = q, p ↔ q, Epq, p ≡ q, or p == q) is as follows:

Logical equality p q p = q 0 0 1 0 1 0 1 0 0 1 1 1
Alternative descriptions
[edit]The form (x = y) is equivalent to the form (x ∧ y) ∨ (¬x ∧ ¬y).
For the operands x and y, the truth table of the logical equality operator is as follows:
y T F x T T F F F T
Inequality
[edit]In mathematics, the plus sign "+" almost invariably indicates an operation that satisfies the axioms assigned to addition in the type of algebraic structure that is known as a field. For Boolean algebra, this means that the logical operation signified by "+" is not the same as the inclusive disjunction signified by "∨" but is actually equivalent to the logical inequality operator signified by "≠", or what amounts to the same thing, the exclusive disjunction signified by "XOR" or "⊕". Naturally, these variations in usage have caused some failures to communicate between mathematicians and switching engineers over the years. At any rate, one has the following array of corresponding forms for the symbols associated with logical inequality:
This explains why "EQ" is often called "XNOR" in the combinational logic of circuit engineers, since it is the negation of the XOR operation; "NXOR" is a less commonly used alternative.[1] Another rationalization of the admittedly circuitous name "XNOR" is that one begins with the "both false" operator NOR and then adds the eXception "or both true".
See also
[edit]References
[edit]- ^ Keeton, Brian; Cavaness, Chuck; Friesen, Geoff (2001), Using Java 2, Que Publishing, p. 112, ISBN 9780789724687.
External links
[edit]
Media related to Logical equality at Wikimedia Commons- Mathworld, XNOR
Logical equality
View on GrokipediaFundamentals
Definition
In propositional logic, a proposition is a declarative statement that expresses a complete thought and possesses one of two possible truth values: true or false.[5] These truth values, often denoted as T for true and F for false, determine the logical status of the proposition under any given interpretation. Logical equality, also referred to as logical equivalence, is the binary relation between two propositions and such that and share identical truth values under every possible interpretation of the propositional variables involved.[4] This means is true if and only if is true across all possible assignments of truth values to the atomic propositions.[6] In other words, the propositions are indistinguishable in terms of their logical consequences and truth conditions, regardless of the specific circumstances.[7] As a binary relation in logic, logical equality connects pairs of propositions and is distinct from other forms of equality in mathematics, such as numerical equality (where two numbers have the same magnitude) or set equality (where two sets contain precisely the same elements); instead, it focuses exclusively on the alignment of truth values for logical statements. This relation ensures that logically equal propositions can be substituted for one another in any logical argument without altering the overall truth value.[8]Notation and Symbols
In propositional logic, logical equality, which indicates that two propositions have the same truth value in all possible cases, is commonly denoted using specific symbols. The primary symbols are the triple bar , representing material equivalence or logical equivalence, and the double arrow , representing the biconditional or "if and only if" relation.[9] The symbol is widely used in mathematical logic texts to express that two formulas are logically equivalent, emphasizing their identical semantic behavior across interpretations. In contrast, appears frequently in philosophical writings on logic, where it underscores the mutual implication between propositions in arguments about necessity and sufficiency.[10] In constructing logical formulas, operator precedence conventions treat equivalence as having the lowest priority among common connectives, below implication (), disjunction (), conjunction (), and negation (). For example, the expression is parsed as without parentheses, requiring explicit grouping to alter this order and avoid ambiguity.[11]Properties and Relations
Equivalence Relations
Logical equality, also known as logical equivalence, constitutes an equivalence relation on the set of propositions within propositional logic. This means it satisfies three fundamental properties: reflexivity, symmetry, and transitivity.[12] Reflexivity holds because for any proposition , . To see this, consider that under any truth assignment (interpretation), receives the same truth value as itself, ensuring identical truth tables for both sides.[12] Symmetry follows from the definition: if , then and have the same truth value in every interpretation, so . For transitivity, suppose and ; then and match in all interpretations, and and match, implying and match everywhere, so . These properties partition the set of propositions into equivalence classes, where each class contains formulas indistinguishable semantically.[13] Logical equivalence relates closely to material implication. Specifically, if and only if . This biconditional captures mutual entailment: implies and vice versa under all interpretations. Expanding the biconditional fully using the definition of implication () yields: This form highlights the truth-functional symmetry, as the conjunction ensures both directions hold tautologically.[12] In logical systems, equivalence relations like logical equality differ from partial orders. While both are reflexive and transitive, partial orders require antisymmetry (if and , then ) instead of symmetry, enabling hierarchical structures such as logical entailment (), where does not imply unless equivalence holds. Logical equality's symmetry thus supports grouping rather than strict ordering.[14]Logical Inequality
Logical inequality in propositional logic refers to the relation between two propositions and where holds if there exists at least one interpretation in which one proposition is true and the other is false.[15] This contrasts with logical equality, where propositions share the same truth value across all interpretations.[15] The relation of logical inequality exhibits irreflexivity, as no proposition can differ from itself ( is always false, since is a tautology). It is symmetric—if then —but lacks transitivity, distinguishing it from logical equality's reflexivity, symmetry, and transitivity. Logical inequality corresponds to the cases detected by the exclusive disjunction operator , also known as XOR, which produces a true value precisely when the operands differ in truth value under an interpretation.[16] This operator is defined by the equivalence , or alternatively .[17] A representative example is the pair and , where because under any interpretation assigning true to , is false, and vice versa.[18] Thus, is a tautology, always true.[17]Representations
Truth Tables
Truth tables provide a systematic method to evaluate the truth values of compound propositions involving logical equality and inequality, by enumerating all possible combinations of truth values for the atomic propositions. For two propositions and , the truth table for logical equality (also denoted as the biconditional ) consists of four rows, corresponding to the possible assignments of truth values to and . The operation yields true precisely when and share the same truth value—both true or both false—and false otherwise.[19] The following table illustrates this:| T | T | T |
| T | F | F |
| F | T | F |
| F | F | T |
| T | T | F |
| T | F | T |
| F | T | T |
| F | F | F |
Alternative Descriptions
Logical equality, or logical equivalence, can be described semantically as the relation between two propositions that are true under exactly the same interpretations or models. In propositional logic, two formulas φ and ψ are semantically equivalent if every model satisfying φ also satisfies ψ, and vice versa, meaning they share the identical set of models where they hold true.[22] This perspective emphasizes the meaning of propositions in terms of their truth conditions across all possible assignments of truth values to atomic propositions. From a syntactic viewpoint, logical equality is characterized by mutual derivability within a formal proof system. Specifically, two formulas φ and ψ are syntactically equivalent if each can be derived from the other using the axioms and rules of inference of the system, or equivalently, if the biconditional φ ↔ ψ is a theorem of the system.[22] By the soundness and completeness theorems for classical propositional logic, this syntactic notion aligns precisely with the semantic one, ensuring that provable equivalences correspond to identical truth behaviors.[22] In a set-theoretic framework, particularly within possible worlds semantics, propositions are represented as subsets of the set of all possible worlds, where a proposition corresponds to the collection of worlds in which it is true. Logical equality then holds when two propositions denote identical subsets, as they are satisfied in precisely the same possible worlds. This description underscores the extensional nature of logical equivalence, treating it as set identity rather than mere similarity. Logical equality is closely related to the concept of entailment, where two propositions φ and ψ are equivalent if each semantically entails the other without one strictly implying the former in a non-biconditional sense. That is, φ entails ψ (every model of φ is a model of ψ) and ψ entails φ, but neither reduces to a one-way implication like material implication.[23] This mutual entailment captures the bidirectional necessity inherent in logical equality, distinguishing it from weaker relations such as one-sided implication.Historical Context
Origins in Classical Logic
The roots of logical equality trace back to Aristotle's syllogistic logic in the 4th century BCE, where the notion is implicit rather than explicitly formalized, manifesting in the recognition that certain syllogistic forms are intertransformable via rules such as conversion (interchanging subject and predicate in particular negative or universal negative propositions) and obversion (replacing a proposition with one having the same truth conditions but altered quality and predicate), thereby preserving validity and yielding identical conclusions. For instance, the first-figure syllogism Barbara (universal affirmative premises yielding universal affirmative conclusion) is equivalent to the second-figure Baroco (universal affirmative major and particular negative minor yielding particular negative conclusion) through indirect reduction, a process that negates and interchanges premises to demonstrate their inferential parity. This equivalence underscores how structurally related forms ensure consistent deductive outcomes, as analyzed in modern reconstructions of Aristotelian validity.[24] These ideas were elaborated in the medieval period through interpretations of Aristotelian logic, beginning with Boethius (c. 480–524 CE), whose commentaries on the Organon distinguished equivalent inferences by introducing principles of co-removal (if one entity is removed, another necessarily is) and co-introduction (if one is introduced, the other must be), treating them as interchangeable in part-whole and genus-species relations to capture logical dependencies.[25] Boethius applied this to mereological inferences, such as the rule that the existence of a whole entails the existence of its parts (si totum est, pars est), with its contrapositive establishing equivalence in destructive reasoning (si pars non est, totum non est), influencing early medieval essentialism about wholes and parts.[25] Peter Abelard (1079–1142 CE) advanced these distinctions in his Dialectica by differentiating "perfect" from "imperfect" entailments: perfect ones, like syllogistic inferences, hold equivalently regardless of term substitutions due to their formal structure alone, independent of external relations among things.[26] A pivotal transition to propositional approaches occurred in Stoic logic during the 3rd century BCE, where equivalence emerged through connectives like the conditional (if p, then q), defined via incompatibility between the antecedent and the negation of the consequent, allowing the biconditional (p if and only if q) to arise as the paired use of a conditional and its converse to express mutual implication.[27] This propositional framework, developed by Chrysippus, shifted focus from term-based syllogisms to assertible connections, laying groundwork for equivalence as symmetric inference without relying on categorical forms. Central texts shaping these origins include Aristotle's Organon—notably the Prior Analytics for syllogistic forms and equivalences, and De Interpretatione for oppositional relations like contradictories (propositions that cannot both be true or false) and contraries (that cannot both be true)—as transmitted and interpreted by Boethius in his Latin translations and commentaries.[24]Developments in Modern Logic
In the 19th century, George Boole pioneered the algebraic treatment of logic, formalizing logical equality through equations within what would later be recognized as precursors to Boolean algebra. In his seminal work An Investigation of the Laws of Thought (1854), Boole represented logical propositions as equations involving class symbols, where equality denoted the identical extension of classes, such as expressing that the class is a subset of under certain conditions.[28] This approach treated equality as an operation manipulable via algebraic rules, including idempotence () and the expansion theorem, allowing logical inferences to be derived mechanically without reliance on syllogistic forms.[29] Boole's framework, though not fully ring-theoretic until later developments, established logic as a symbolic algebra where equality served as the foundational relation for deriving truths.[30] Entering the early 20th century, Bertrand Russell and Alfred North Whitehead advanced the formalization of logical equality in their monumental Principia Mathematica (1910–1913), integrating it into a ramified type theory to ground mathematics in logic. They defined identity—or strict logical equality—via the principle of indiscernibility: , where denotes a predicative function, ensuring and share all properties without invoking higher-order impredicative definitions that risked paradox.[31] Equivalence classes emerged in their "no-classes" theory, treating classes as proxies via existential quantification: , which partitioned entities based on shared logical properties while avoiding set-theoretic inconsistencies.[32] This rigorous handling of equivalence classes not only resolved foundational crises but also emphasized equality's role in constructing hierarchical logical structures. Post-World War II, Alfred Tarski's contributions elevated semantic understandings of logical equality within model theory, shifting focus from syntactic derivations to interpretive structures. In works such as his 1936 papers on logical consequence and later expositions like Logic, Semantics, Metamathematics (1956 English edition), Tarski defined two sentences as logically equivalent if they hold in precisely the same models, formalizing equality as model-theoretic invariance: a sentence follows from if every model satisfying also satisfies .[33] This semantic criterion, refined in his Berkeley seminars and collaborative texts, distinguished logical equality from mere syntactic identity by emphasizing preservation under all domain reinterpretations, thus providing a robust framework for equivalence in first-order languages.[34] Tarski's approach profoundly influenced modern logic by linking equality to truth definitions and consequence relations, enabling precise analyses of expressive completeness. The influence of computability theory, particularly through Alan Turing's 1936 paper "On Computable Numbers, with an Application to the Entscheidungsproblem," indirectly shaped developments in logical equality by highlighting limits on decision procedures for equivalence. Turing demonstrated the undecidability of first-order logic's validity problem, implying no general algorithm exists to verify whether two formulas are logically equivalent across all interpretations, as equivalence reduces to checking universal validity of their difference.[35] This result, via Turing machines as models of computation, underscored that while propositional equivalence is decidable, higher-order cases resist mechanical resolution, informing post-war refinements in automated theorem proving and equality checking.[36] Turing's framework thus constrained practical formalizations of equality, emphasizing its non-computable aspects in complex logical systems.[37]Applications
In Propositional Logic
In propositional logic, logical equality, also known as logical equivalence, holds between two propositions if they have the same truth value under every possible truth assignment to their atomic propositions. This relation is denoted by the symbol , and it forms the basis for manipulating and analyzing compound propositions without altering their logical meaning.[8] A primary role of logical equality in propositional logic is simplification, where equivalence laws are applied to rewrite complex formulas into simpler, equivalent forms. For instance, De Morgan's laws state that and , enabling the transformation of negated compound statements. Other laws, such as the distributive law , allow factoring out common terms to reduce redundancy.[8] These simplifications facilitate easier reasoning and verification in logical arguments. Proofs by equivalence involve constructing a chain of applications of known equivalence laws to transform one proposition into another, thereby establishing their equality. This method is particularly useful for demonstrating that a proposition is a tautology by reducing it to (true) or a contradiction by reducing it to (false). For example, to prove , one applies the distributive law followed by the law of excluded middle () and identity ().[8] Each step in the chain must be justified by a specific equivalence law to ensure validity. The problem of checking logical equality in propositional logic is decidable, meaning there exists an algorithm that can always determine whether two propositions are equivalent. This decidability follows from the finite nature of truth assignments for a given set of atomic propositions, allowing exhaustive verification.[22] Truth tables provide a direct method for this check by comparing the truth value columns of the two propositions across all assignments, where is the number of distinct atomic propositions.[8] Although efficient for small , the exponential growth in table size underscores the practical limitations for large formulas, despite theoretical decidability.[22]In Formal Systems and Computing
In proof assistants such as Coq and Isabelle/HOL, logical equality supports the verification of program equivalence by providing mechanisms to prove that two terms or programs behave identically under all inputs. In Coq, based on the Calculus of Inductive Constructions, equality is defined via Leibniz's principle as an inductive typeeq A x y, with reflexivity as a constructor eq_refl, allowing tactics like rewrite to substitute equals in proofs and f_equal to lift equalities over functions, as demonstrated in verifying properties like list reversal equivalence rev (rev xs) = xs. Isabelle/HOL, grounded in higher-order logic, treats equality as a polymorphic infix operator = :: 'a => 'a => bool, which coincides with logical equivalence for propositions, enabling equational reasoning through simplification and induction to confirm functional equivalences, such as add m 0 = m for addition. These systems ensure that proven equalities are definitionally valid, supporting certified software verification in domains like compiler correctness.[38][39]
In computing applications, logical equality checking is central to formal verification tools, where SAT solvers reduce equivalence problems to satisfiability queries by constructing a miter circuit: for two Boolean formulas and , the formula (where are outputs) is unsatisfiable if and are equivalent, leveraging modern solvers like MiniSat for efficient resolution in logic synthesis flows. Model checking employs similar techniques to verify temporal logic properties by checking equivalence between state transition systems. For scalable representation, Binary Decision Diagrams (BDDs) provide a canonical graph-based encoding of Boolean functions, enabling efficient equivalence tests via structural isomorphism or cofactor comparisons; for instance, two BDDs are equivalent if their roots represent the same function under a fixed variable order, as used in tools like VIS for hardware verification, though variable ordering impacts exponential size growth. These methods underpin equivalence checking in EDA tools, ensuring design consistency across refinement stages.[40][41]
A key challenge in formal systems arises in higher-order logics, where deciding equality between terms is undecidable due to the expressive power allowing encodings of Turing-complete computations, such as higher-order unification problems that reduce to the halting problem. In proof search, treating equality as a primitive connective exacerbates this, as automated theorem proving cannot guarantee termination for equivalence queries involving lambda abstractions or higher-type variables. This undecidability limits fully automatic verification in systems like HOL, necessitating interactive guidance or decidable fragments.[42]