Proposition

A proposition is a statement to which a logical truth value can be assigned.

A logical connective forms a compound proposition from component propositions; logical truth and logical falsity are the zero-input cases. Logical negation has one input, while logical conjunction, logical disjunction, and logical implication each have two. In classical propositional logic, these logical connectives are truth-functional: their output value is determined by their input values, as listed in a truth table. This does not characterize every kind of logical connective in every logic. See forall x: Calgary, section 10.1.

A binary logical connective true exactly when its two arguments have the same truth value. It is logically equivalent to $(P\to Q)\wedge (Q\to P)$, and hence to $(\neg P\vee Q)\wedge (\neg Q\vee P)$. Its truth table has value one on input pairs $(0,0)$ and $(1,1)$, and zero on $(0,1)$ and $(1,0)$.

Logical implication forms the proposition $A\to B$, read “if $A$, then $B$”. In classical propositional logic, it is false exactly when $A$ is true and $B$ is false. Equivalently, it has the same truth table as $\neg A\vee B$, using logical negation and logical disjunction. A false hypothesis makes the logical implication true regardless of its conclusion; thus it asserts neither the hypothesis nor a causal connection.

For example, for every natural number $n$, divisibility by four implies that $n$ is an even number: $n=4k=2(2k)$. At $n=8$, both statements are true. At $n=6$, the hypothesis is false and the conclusion true; at $n=3$, both are false. The only forbidden case is a multiple of four that is not an even number.

In Intuitionistic propositional logic, a proof of $A\to B$ consists of a construction transforming any proof of $A$ into a proof of $B$. The implication introduction rule proves $B$ under a temporary assumption $A$; the modus ponens rule applies the result when $A$ is available. The classical identification with $\neg A\vee B$ is not generally intuitionistically valid.

For distinct propositional variables, eliminate each right-associated logical implication to obtain $\neg A_n\vee \cdots \vee \neg A_2\vee A_1$. Exactly one Boolean valuation falsifies all these disjuncts: $A_1=0$ and $A_2=\cdots =A_n=1$. Of the $2^n$ assignments, the other $2^n-1$ are satisfying assignments. Left-associated implication chains have a different meaning and need not have the same count.

The contrapositive of a logical implication $A\to B$ reverses the direction and applies logical negation to both sides: $\neg B\to \neg A$. In classical propositional logic they are equivalent, so either can be proved in place of the other. The contrapositive of “divisibility by four implies being an even number” says that a number that is not an even number cannot be divisible by four.

In Intuitionistic propositional logic, $A\to B$ still implies its contrapositive: assumptions $A$ and $\neg B$ would yield $B$ and hence a contradiction. The reverse direction is not generally valid. From $\neg B\to \neg A$ and $A$, one obtains only $\neg \neg B$; obtaining $B$ additionally requires double-negation elimination.

The converse implication of $A\to B$ is $B\to A$. It exchanges hypothesis and conclusion without logical negation. It need not follow from the original logical implication: $n=2$ is an even number but is not divisible by four. Thus “being an even number implies divisibility by four” is false, although the original implication holds for all natural numbers. Proving both directions establishes an “if and only if” statement; proving a contrapositive establishes the original implication classically, without establishing its converse implication.

A logical implication holds whenever its premise is false. For partial correctness, an execution that never terminates supplies no final state violating the postcondition.

The conjunction $A\wedge B$ holds when both $A$ and $B$ hold.

An AND gate computes $a\wedge b=ab$ for bits $a,b$. It is irreversible when only its one-bit output is retained. The Toffoli gate embeds the operation reversibly as $(a,b,c)\mapsto (a,b,c\oplus ab)$; setting $c=0$ preserves the inputs while recording their logical conjunction.

The disjunction $A\vee B$ holds when at least one of $A$ and $B$ holds. Constructively, a proof records which disjunct holds and provides its proof.

A logic gate computing inclusive logical disjunction: its output is one exactly when at least one input is one.

Logical truth is the nullary connective that is always true.

A logical matrix specifies truth values, designated values, and operations interpreting the primitive connectives. To prove nonderivability from an axiom set, it suffices that every axiom instance is designated and every inference rule preserves designation, while the proposed conclusion is not designated under some valuation. The primitive connective symbols need not receive their intended classical meanings: preservation by the displayed rules is what makes the syntactic obstruction valid. Rules with discharged assumptions, such as a deduction theorem for propositional logic, must also preserve consequence for arbitrary assumption sets.

Take ordinary material logical implication on $\{0,1\}$, designate $1$, and interpret negation by the constant-zero operation $N$. Then $A\to (B\to A)$ and $(NB\to A)\to (NA\to B)$ are always designated, and modus ponens rule and logical implication discharge preserve consequence. But $(NB\to NA)\to (A\to B)$ is false for $A=1,B=0$. Thus the first two schemes and the deduction rule do not derive the last scheme. This detects the loss of a genuine classical-negation principle even though all the displayed schemes are tautologies under the usual classical negation.

Logical falsity, written $\perp$, is a zero-input logical connective interpreted as false under every Boolean valuation. In standard Intuitionistic propositional logic and classical propositional logic, it has no introduction rule that produces it without premises. The logical falsity elimination rule permits deriving any logical formula from it.

A formal proof can derive $\perp$ from contradictory assumptions: $P$ together with $\neg P$ gives it by the negation elimination rule. A first-order theory is first-order consistent when it has no assumption-free proof of $\perp$ from its own axioms. Thus having no proof is a consistency property of a specified formal proof system, rather than an unconditional definition of logical falsity.

In classical propositional logic, a truth value is false or true, encoded by a bit as zero or one. A Boolean valuation assigns these values to primitive propositions and extends to compound propositional formulas through logical connectives.