Hubbry Logo
Logical equalityLogical equalityMain
Open search
Logical equality
Community hub
Logical equality
logo
8 pages, 0 posts
0 subscribers
Be the first to start a discussion here.
Be the first to start a discussion here.
Logical equality
Logical equality
from Wikipedia
Logical equality
EQ, XNOR
Venn diagram of Logical equality
Definition
Truth table
Logic gate
Normal forms
Disjunctive
Conjunctive
Zhegalkin polynomial
Post's lattices
0-preservingno
1-preservingyes
Monotoneno
Affineyes
Self-dualno

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:

The Venn diagram of A EQ B (red part is true)
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 (xy) ∨ (¬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]
[edit]
Revisions and contributorsEdit on WikipediaRead on Wikipedia
from Grokipedia
Logical equality, also known as , is a in propositional logic and that holds between two propositions if they have identical truth values for every possible assignment of truth values to their constituent atomic propositions. This equivalence is denoted by the symbol ≡, and it means that the biconditional connective (↔) between the two propositions forms a tautology—always true regardless of the inputs. The concept is foundational for simplifying complex logical expressions and proving the validity of arguments by transforming one form into another without altering meaning. Key and laws underpin this, including commutative laws (e.g., PQQPP \lor Q \equiv Q \lor P), associative laws (e.g., (PQ)RP(QR)(P \lor Q) \lor R \equiv P \lor (Q \lor R)), (e.g., ¬(PQ)¬P¬Q\neg (P \land Q) \equiv \neg P \lor \neg Q), and the of implication (e.g., PQ¬PQP \to Q \equiv \neg P \lor Q). These equivalences can be verified using truth tables, which enumerate all possible truth assignments, or through algebraic manipulation via the laws themselves. In practice, logical equality plays a critical role in fields such as for optimizing digital circuits—reducing the number of logic gates needed for efficiency and reliability—and in for analyzing the structure of arguments and entailments. It also extends to normalizing expressions into standard forms like (DNF) or (CNF), facilitating and theorem proving.

Fundamentals

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. 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 PP and QQ such that PP and QQ share identical truth values under every possible interpretation of the propositional variables involved. This means PP is true if and only if QQ is true across all possible assignments of truth values to the atomic propositions. In other words, the propositions are indistinguishable in terms of their logical consequences and truth conditions, regardless of the specific circumstances. As a in logic, logical equality connects pairs of propositions and is distinct from other forms of equality in , 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 s for logical statements. This relation ensures that logically equal propositions can be substituted for one another in any logical argument without altering the overall .

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 \equiv, representing material equivalence or , and the double arrow \leftrightarrow, representing the biconditional or "" relation. The symbol \equiv is widely used in texts to express that two formulas are logically equivalent, emphasizing their identical semantic across interpretations. In contrast, \leftrightarrow appears frequently in philosophical writings on logic, where it underscores the mutual implication between propositions in arguments about . In constructing logical formulas, operator precedence conventions treat equivalence as having the lowest priority among common connectives, below implication (\rightarrow), disjunction (\lor), conjunction (\land), and negation (¬\lnot). For example, the expression PQRSP \land Q \rightarrow R \equiv S is parsed as (PQ)(RS)(P \land Q) \rightarrow (R \equiv S) without parentheses, requiring explicit grouping to alter this order and avoid ambiguity.

Properties and Relations

Equivalence Relations

Logical equality, also known as , constitutes an equivalence relation on the set of within propositional logic. This means it satisfies three fundamental properties: reflexivity, , and transitivity. Reflexivity holds because for any PP, PPP \equiv P. To see this, consider that under any truth assignment (interpretation), PP receives the same as itself, ensuring identical truth tables for both sides. Symmetry follows from the definition: if PQP \equiv Q, then PP and QQ have the same in every interpretation, so QPQ \equiv P. For transitivity, suppose PQP \equiv Q and QRQ \equiv R; then PP and QQ match in all interpretations, and QQ and RR match, implying PP and RR match everywhere, so PRP \equiv R. These properties partition the set of into equivalence classes, where each class contains formulas indistinguishable semantically. Logical equivalence relates closely to material implication. Specifically, PQP \equiv Q if and only if (PQ)(QP)(P \to Q) \land (Q \to P). This biconditional captures mutual entailment: PP implies QQ and vice versa under all interpretations. Expanding the biconditional fully using the definition of implication (AB¬ABA \to B \equiv \neg A \lor B) yields: (PQ)    (¬PQ)(¬QP)(P \equiv Q) \iff (\neg P \lor Q) \land (\neg Q \lor P) This form highlights the truth-functional , as the conjunction ensures both directions hold tautologically. In logical systems, equivalence relations like logical equality differ from partial orders. While both are reflexive and transitive, partial orders require antisymmetry (if ABA \leq B and BAB \leq A, then A=BA = B) instead of , enabling hierarchical structures such as logical entailment (\models), where PQP \models Q does not imply QPQ \models P unless equivalence holds. Logical equality's thus supports grouping rather than strict ordering.

Logical Inequality

Logical inequality in propositional logic refers to the relation between two propositions PP and QQ where PQP \neq Q holds if there exists at least one interpretation in which one proposition is true and the other is false. This contrasts with logical equality, where propositions share the same across all interpretations. The relation of logical inequality exhibits irreflexivity, as no can differ from itself (PPP \neq P is always false, since PPP \leftrightarrow P is a tautology). It is symmetric—if PQP \neq Q then QPQ \neq P—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 \oplus, also known as XOR, which produces a true value precisely when the operands differ in truth value under an interpretation. This operator is defined by the equivalence PQ(PQ)¬(PQ)P \oplus Q \equiv (P \lor Q) \land \lnot (P \land Q), or alternatively PQ(P¬Q)(¬PQ)P \oplus Q \equiv (P \land \lnot Q) \lor (\lnot P \land Q). A representative example is the pair pp and ¬p\lnot p, where p¬pp \neq \lnot p because under any interpretation assigning true to pp, ¬p\lnot p is false, and vice versa. Thus, p¬pp \oplus \lnot p is a tautology, always true.

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 PP and QQ, the truth table for logical equality PQP \equiv Q (also denoted as the biconditional PQP \leftrightarrow Q) consists of four rows, corresponding to the 222^2 possible assignments of truth values to PP and QQ. The operation yields true precisely when PP and QQ share the same —both true or both false—and false otherwise. The following table illustrates this:
PPQQPQP \equiv Q
TTT
TFF
FTF
FFT
This tabular representation confirms that logical equality holds the propositions are simultaneously true or simultaneously false. Logical inequality, often denoted as PQP \oplus Q (exclusive or), is the negation of logical equality and is true exactly when PP and QQ have differing truth values. Its truth table mirrors that of equality but inverts the outcomes, producing true in the two cases where one proposition is true and the other false. The truth table for PQP \oplus Q is as follows:
PPQQPQP \oplus Q
TTF
TFT
FTT
FFF
This form highlights the complementary nature of equality and inequality in propositional logic. For an extension to multiple propositions, say kk atomic propositions P1,P2,,PkP_1, P_2, \dots, P_k, a truth table enumerates all 2k2^k possible truth assignments, partitioning the rows into subsets where a given compound formula involving logical equality evaluates to true. For instance, with three propositions, the table has eight rows, and the equality P1(P2P3)P_1 \equiv (P_2 \wedge P_3) would be true only in those assignments where P1P_1 matches the conjunction of P2P_2 and P3P_3. This exhaustive enumeration allows for precise analysis of how equality constraints divide the logical space. Truth tables also serve to verify tautologies, where a ϕ\phi is a tautology if ϕ\phi \equiv \top (the constant true), meaning its column is true across all 2n2^n rows for nn atomic propositions. For example, the (PQ)(PQ)(P \equiv Q) \vee (P \oplus Q) evaluates to true in every row, confirming it as a tautology since equality and inequality exhaustively cover all possibilities. This method provides a mechanical proof of such universal validity without relying on semantic interpretations.

Alternative Descriptions

Logical equality, or , 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. 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 . Specifically, two formulas φ and ψ are syntactically equivalent if each can be derived from the other using the axioms and rules of of the , or equivalently, if the biconditional φ ↔ ψ is a of the . By the 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. In a set-theoretic framework, particularly within possible worlds semantics, are represented as subsets of the set of all possible worlds, where a corresponds to the collection of worlds in which it is true. Logical equality then holds when two denote identical subsets, as they are satisfied in precisely the same possible worlds. This description underscores the extensional nature of , 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. 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. 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. 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. 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. 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 of the consequent, allowing the biconditional (p q) to arise as the paired use of a conditional and its converse to express mutual implication. This propositional framework, developed by , 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.

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 x=vyx = vy expressing that the class xx is a subset of yy under certain conditions. This approach treated equality as an operation manipulable via algebraic rules, including idempotence (x2=xx^2 = x) and the expansion theorem, allowing logical inferences to be derived mechanically without reliance on syllogistic forms. 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. Entering the early 20th century, and advanced the formalization of logical equality in their monumental (1910–1913), integrating it into a ramified to ground mathematics in logic. They defined identity—or strict logical equality—via the principle of indiscernibility: x=y\eqdfϕ(ϕ!xϕ!y)x = y \eqdf \forall \phi \, (\phi!x \supset \phi!y), where ϕ!\phi! denotes a predicative function, ensuring xx and yy share all properties without invoking higher-order impredicative definitions that risked . Equivalence classes emerged in their "no-classes" theory, treating classes as proxies via : ϕ{xψ(x)}\eqdfχ(x(χ!xψ(x))ϕ(λxχ(x)))\phi \{x \mid \psi(x)\} \eqdf \exists \chi \, (\forall x \, (\chi!x \equiv \psi(x)) \land \phi(\lambda x \, \chi(x))), which partitioned entities based on shared logical properties while avoiding set-theoretic inconsistencies. 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 , shifting focus from syntactic derivations to interpretive structures. In works such as his 1936 papers on 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 Γ\Gamma follows from Δ\Delta if every model satisfying Δ\Delta also satisfies Γ\Gamma. 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 languages. 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. 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. Turing's framework thus constrained practical formalizations of equality, emphasizing its non-computable aspects in complex logical systems.

Applications

In Propositional Logic

In propositional logic, logical equality, also known as , holds between two propositions if they have the same under every possible truth assignment to their atomic propositions. This relation is denoted by the symbol \equiv, and it forms the basis for manipulating and analyzing compound propositions without altering their logical meaning. A primary of logical equality in propositional logic is simplification, where equivalence laws are applied to rewrite complex formulas into simpler, equivalent forms. For instance, state that ¬(PQ)¬P¬Q\neg (P \land Q) \equiv \neg P \lor \neg Q and ¬(PQ)¬P¬Q\neg (P \lor Q) \equiv \neg P \land \neg Q, enabling the transformation of negated compound statements. Other laws, such as the distributive law (PQ)(P¬Q)P(Q¬Q)PP(P \land Q) \lor (P \land \neg Q) \equiv P \land (Q \lor \neg Q) \equiv P \land \top \equiv P, allow factoring out common terms to reduce redundancy. 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 \top (true) or a contradiction by reducing it to \bot (false). For example, to prove (PQ)(P¬Q)P(P \land Q) \lor (P \land \neg Q) \equiv P, one applies the distributive law followed by the law of excluded middle (Q¬QQ \lor \neg Q \equiv \top) and identity (PPP \land \top \equiv P). 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 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. Truth tables provide a direct method for this check by comparing the columns of the two propositions across all 2n2^n assignments, where nn is the number of distinct atomic propositions. Although efficient for small nn, the exponential growth in table size underscores the practical limitations for large formulas, despite theoretical decidability.

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 eq 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 , treats equality as a polymorphic infix operator = :: 'a => 'a => bool, which coincides with 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 in domains like correctness. In computing applications, logical equality checking is central to tools, where SAT solvers reduce equivalence problems to queries by constructing a miter circuit: for two ϕ\phi and ψ\psi, the i(oioi)\bigwedge_{i} (o_i \oplus o_i') (where oi,oio_i, o_i' are outputs) is unsatisfiable if ϕ\phi and ψ\psi are equivalent, leveraging modern solvers like MiniSat for efficient resolution in logic synthesis flows. employs similar techniques to verify properties by checking equivalence between state transition systems. For scalable representation, Binary Decision Diagrams (BDDs) provide a canonical graph-based encoding of functions, enabling efficient equivalence tests via structural 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. 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 . In proof search, treating equality as a primitive connective exacerbates this, as cannot guarantee termination for equivalence queries involving abstractions or higher-type variables. This undecidability limits fully automatic verification in systems like HOL, necessitating interactive guidance or decidable fragments.

References

Add your contribution
Related Hubs
User Avatar
No comments yet.