Every term the calculator, the guides and the exercises use, defined in one place.
Look a term up, see its notation, and open the example in the calculator to watch it behave. Terms defined here are highlighted the first time they appear in a guide.
All 62 terms
The study of which conclusions genuinely follow from which assumptions.
Logic studies the form of reasoning rather than its subject matter. Formal logic replaces sentences with symbols so that whether a conclusion follows can be settled by the shape of the argument alone, and checked mechanically.
A statement that is either true or false, and not both.
A proposition is a declarative statement with exactly one truth value. “It is raining” is a proposition; a question or a command is not, because there is nothing about it to be true or false.
One of the two values a proposition can take: true or false.
Classical logic gives every proposition exactly one of two truth values, written ⊤ and ⊥ (or 1 and 0). Every row of a truth table is one assignment of truth values to the variables, and the result the formula takes there.
A proposition with no connectives inside it.
An atomic proposition cannot be broken into smaller propositions: it has no negation, conjunction or other connective in it. Everything else is compound, built from atoms by connectives, and its truth value is fixed by theirs.
A letter such as p or A standing in for an arbitrary proposition.
A propositional variable is a placeholder for any proposition whatever. The calculator accepts single letters as variables and gives each one a column of the truth table, with a row for every combination of values they could take.
In the calculatorp → qA string of symbols the grammar of the language actually allows.
A well-formed formula is built by the rules: a variable is one, and so is any formula made from smaller ones by a connective. “p ∧ ∨ q” is not, which is why the calculator reports a parse error rather than guessing.
One assignment of truth values to every variable in a formula.
An interpretation says what each variable is worth, and so fixes the value of the whole formula. A formula with n variables has 2ⁿ interpretations, which is exactly the set of rows in its truth table.
A set of premises offered in support of a conclusion.
An argument claims that its conclusion follows from its premises. Type one into the calculator with a turnstile — premises before it, conclusion after — and every row is checked for a case where the premises hold and the conclusion fails.
In the calculatorp → q, p ⊨ qA statement an argument assumes in order to reach its conclusion.
Premises are what an argument starts from. Validity asks only whether the conclusion holds wherever all the premises do; whether the premises are actually true is a separate question, and the one soundness adds.
In the calculatorp → q, p ⊨ qThe statement an argument is trying to establish.
The conclusion is what the premises are offered in support of. In the calculator it is the expression after the turnstile, and an argument is valid when no interpretation makes the premises true while making it false.
In the calculatorp → q, p ⊨ qA symbol that builds a compound proposition out of simpler ones.
A connective such as ¬, ∧, ∨, → or ↔ combines propositions into a larger one whose truth value depends only on theirs. That dependence is what a truth table records, one row per combination of inputs.
Reverses a truth value: ¬p is true exactly when p is false.
Negation is the only one-place connective in propositional logic. Written ¬p, ~p or !p, it turns true into false and false into true, so negating twice returns the original proposition.
In the calculator¬pTrue only when both parts are true: p ∧ q.
A conjunction asserts both of its parts, called conjuncts. It is true in exactly one row of its truth table — the one where both conjuncts are true — which makes it the strictest of the binary connectives.
In the calculatorp ∧ qTrue when at least one part is true: p ∨ q.
Disjunction in logic is inclusive: p ∨ q is true when p is true, when q is true, and when both are. The exclusive reading of “or”, true only when the parts differ, is a separate connective.
In the calculatorp ∨ qTrue when exactly one of two propositions is true.
Exclusive disjunction, written ⊕ or XOR, holds when its parts differ and fails when they agree. It is the negation of the biconditional, and it can be written out as (p ∨ q) ∧ ¬(p ∧ q).
In the calculator(p ∨ q) ∧ ¬(p ∧ q)p → q, false only when p is true and q is false.
The material conditional says nothing more than “not: antecedent true and consequent false”, so it holds automatically whenever the antecedent fails. That is why p → q is equivalent to ¬p ∨ q.
In the calculatorp → qp ↔ q, true when both parts have the same truth value.
The biconditional asserts each side conditional on the other: it is true when both parts are true and when both are false. A biconditional that is a tautology is exactly a statement of logical equivalence.
In the calculatorp ↔ qThe “if” part of a conditional — the p in p → q.
The antecedent is the condition a conditional depends on. When it is false the whole conditional is true regardless of the consequent, which is the source of most surprises in the truth table for →.
In the calculatorp → qThe “then” part of a conditional — the q in p → q.
The consequent is what a conditional claims to follow if its antecedent holds. A true consequent makes the conditional true, but it does not make the antecedent true — inferring that is a formal fallacy.
In the calculatorp → qThe conditional with its two parts swapped: q → p.
The converse of p → q is q → p, and the two are not equivalent: the calculator finds a row where one holds and the other fails. Treating them as interchangeable is affirming the consequent.
In the calculatorq → p¬q → ¬p, which always has the same truth value as p → q.
The contrapositive negates both parts of a conditional and swaps them. Unlike the converse it is genuinely equivalent to the original, which is what makes proof by contraposition a legitimate move in mathematics.
In the calculator(p → q) ≡ (¬q → ¬p)The negation of a conjunction: true unless both inputs are true.
NAND, written ↑, is ¬(p ∧ q). It is functionally complete: every other connective can be built out of NAND alone, which is why it is a workhorse of digital circuit design.
In the calculator¬(p ∧ q)The negation of a disjunction: true only when both inputs are false.
NOR, written ↓, is ¬(p ∨ q). Like NAND it is functionally complete on its own, so a circuit can be built entirely from NOR gates and nothing else.
In the calculator¬(p ∨ q)Which connective binds first when brackets are left out.
Negation binds tightest, then conjunction, disjunction, the conditional and finally the biconditional. So ¬p ∧ q ∨ r reads as ((¬p) ∧ q) ∨ r; brackets override the order whenever the intended reading differs.
In the calculator¬p ∧ q ∨ rA row for every assignment of values, with the formula's value in each.
A truth table lists all 2ⁿ interpretations of a formula's n variables and works out its value in each. Because it is exhaustive it settles every semantic question in propositional logic: equivalence, validity, satisfiability and the rest.
In the calculatorp → qA formula true under every interpretation.
A tautology comes out true in every row of its truth table, so it says nothing about the world — p ∨ ¬p is true whatever p is. Two formulas are equivalent exactly when the biconditional between them is a tautology.
In the calculatorp ∨ ¬pA formula false under every interpretation.
A contradiction such as p ∧ ¬p is false in every row of its truth table. Deriving one from a set of assumptions shows the assumptions cannot all hold, which is the engine of proof by contradiction.
In the calculatorp ∧ ¬pA formula true under some interpretations and false under others.
A contingent formula is neither a tautology nor a contradiction: its truth table has at least one true row and at least one false one. Most formulas anyone writes are contingent, which is what makes them informative.
In the calculatorp ∧ qWhether any interpretation makes the formula true.
A formula is satisfiable when at least one row of its truth table is true, and that row is a model of it. Deciding satisfiability is the central problem of SAT solvers and, through them, of much automated reasoning.
In the calculatorp ∧ (p → q)Two formulas with identical truth tables.
Equivalent formulas agree under every interpretation, so either can replace the other anywhere without changing what is said. Type an equals sign between two expressions and the calculator compares their columns row by row.
In the calculator(p → q) ≡ (¬p ∨ q)The conclusion holds in every interpretation where the premises do.
Written Γ ⊨ φ, logical consequence is what a valid argument claims. It is checked by looking for a counterexample: an interpretation making every premise true and the conclusion false. If there is none, the entailment holds.
In the calculatorp → q, p ⊨ qNo interpretation makes the premises true and the conclusion false.
Validity is a property of the form of an argument, not of the facts: a valid argument can have false premises and a false conclusion. What it cannot have is true premises alongside a false conclusion.
In the calculatorp → q, p ⊨ qA valid argument whose premises are also actually true.
Soundness adds a factual claim to a formal one: the argument is valid, and its premises hold. Logic alone can settle the first half; the second belongs to whatever the argument is about.
An interpretation making the premises true and the conclusion false.
A countermodel is proof that an argument is invalid — one row is enough. The calculator reports the row it finds, which turns “this does not follow” into a concrete assignment you can check by hand.
In the calculatorp → q ⊨ q → pSome interpretation makes every statement in the set true at once.
A set of premises is consistent when they can all hold together. Inconsistent premises entail everything whatsoever, so an argument built on them is technically valid and worth nothing.
In the calculatorp → q, ¬q ⊨ ¬pA variable or its negation, such as p or ¬p.
Literals are the atoms of the normal forms: a clause is a disjunction of literals and a minterm is a conjunction of them. A literal is positive when the variable stands bare and negative when it is negated.
In the calculator¬pA disjunction of literals, such as p ∨ ¬q ∨ r.
A clause is one of the bracketed groups a conjunctive normal form is built from. Since a conjunction is true only when every part is, a CNF formula holds exactly when every one of its clauses does.
In the calculatorp ∨ ¬q ∨ rAn OR of ANDs: a disjunction of conjunctions of literals.
Every formula has a disjunctive normal form, and it can be read straight off the truth table: one conjunction per true row, joined by ∨. The calculator also reports a minimized DNF, which says the same thing in fewer literals.
In the calculator(p ∧ q) ∨ (¬p ∧ r)An AND of ORs: a conjunction of clauses.
Conjunctive normal form is read off the false rows of the truth table, one clause per row. It is the input format SAT solvers expect, which makes the conversion into CNF a routine step in automated reasoning.
In the calculator(p ∨ q) ∧ (¬p ∨ r)A conjunction naming exactly one row of the truth table.
A minterm mentions every variable once, negated or not, so precisely one interpretation satisfies it. Collecting the minterms of the true rows and joining them with ∨ gives the formula's disjunctive normal form.
In the calculatorp ∧ ¬q ∧ rA disjunction ruling out exactly one row of the truth table.
A maxterm mentions every variable once and is false in a single interpretation. Taking the maxterm of each false row and joining them with ∧ gives the formula's conjunctive normal form.
In the calculatorp ∨ ¬q ∨ rNegation turns ∧ into ∨ and ∨ into ∧: ¬(p ∧ q) ≡ ¬p ∨ ¬q.
De Morgan's laws push a negation inwards across a conjunction or a disjunction, flipping the connective as it goes. They are how a formula is driven towards a normal form, and how negations are simplified in code and in circuits.
In the calculator¬(p ∧ q) ≡ ¬p ∨ ¬qNegating twice returns the original: ¬¬p ≡ p.
Double negation holds in classical logic in both directions, so ¬¬p and p can always be swapped. Intuitionistic logic keeps only the direction from p to ¬¬p, which is where the two systems part company.
In the calculator¬¬p ≡ pThe algebra of two values, with ∧, ∨ and ¬ as its operations.
Boolean algebra is propositional logic written as arithmetic on 0 and 1, with laws — commutativity, distributivity, absorption, De Morgan — that let expressions be rewritten and simplified. It is the mathematics digital circuits are designed in.
In the calculator(p ∧ q) ∨ (p ∧ ¬q) ≡ pA grid layout of a truth table that makes simplifications visible.
A Karnaugh map arranges the rows so that neighbouring cells differ in one variable, and the edges wrap. It is also written K-map, or kmap. Rectangular groups of adjacent 1s of size 1, 2, 4 or 8 then read directly as terms of a minimal expression.
In the calculator(p ∧ q) ∨ (p ∧ ¬r)A group on the map that cannot be enlarged any further.
An implicant is a conjunction of literals that forces the formula true; it is prime when dropping any literal would stop it doing so. On a Karnaugh map the prime implicants are the maximal rectangles of 1s.
The only prime implicant covering some particular 1.
When a 1 on the map belongs to just one maximal group, that group has to appear in every minimal cover, so it is taken first. What is left over is the part of the cover that genuinely has to be searched.
A circuit element computing one connective on its inputs.
AND, OR, NOT, NAND, NOR and XOR gates are the hardware counterparts of the connectives. A formula and a circuit are the same object drawn twice, which is why the calculator can render an expression as a gate diagram.
In the calculator(p ∧ q) ∨ ¬rA licensed step from formulas already derived to a new one.
A rule of inference is a pattern such as modus ponens that may be applied whenever formulas of the right shape are available. Proof systems are built from a handful of them, chosen so that only entailed conclusions can be derived.
From p → q and p, infer q.
Modus ponens is the basic conditional rule: given a conditional and its antecedent, the consequent follows. Its validity is visible in the truth table — the only row with both premises true has the conclusion true as well.
In the calculatorp → q, p ⊨ qFrom p → q and ¬q, infer ¬p.
Modus tollens runs a conditional backwards: if the consequent fails, the antecedent cannot have held. It is the contrapositive at work, and it is the shape of every argument that refutes a hypothesis by testing its predictions.
In the calculatorp → q, ¬q ⊨ ¬pFrom p → q and q → r, infer p → r.
Hypothetical syllogism chains conditionals together, which is what makes long derivations possible: each link carries the argument one step further without any premise being asserted outright.
In the calculatorp → q, q → r ⊨ p → rFrom p ∨ q and ¬p, infer q.
Disjunctive syllogism eliminates the ruled-out option: if one of two alternatives holds and the first does not, the second must. It is the rule behind reasoning by elimination.
In the calculatorp ∨ q, ¬p ⊨ qProving a conclusion by applying inference rules step by step.
Natural deduction derives a conclusion from premises with introduction and elimination rules for each connective, allowing temporary assumptions to be made and later discharged. It proves what a truth table checks, but without enumerating every row.
Assume the opposite, derive a contradiction, conclude the original.
To prove φ, assume ¬φ and derive something of the form ψ ∧ ¬ψ. Since no interpretation makes a contradiction true, the assumption cannot hold, and φ follows. It is how irrationality and infinitude proofs usually go.
In the calculatorp ∧ ¬pThe invalid step from p → q and q to p.
A true consequent does not establish the antecedent: something else may have brought it about. The calculator exhibits the countermodel — p false, q true — which is the row that separates this from modus ponens.
In the calculatorp → q, q ⊨ pThe invalid step from p → q and ¬p to ¬q.
A conditional says nothing about what happens when its antecedent fails, so ruling the antecedent out leaves the consequent open. The countermodel is the row where p is false and q is true.
In the calculatorp → q, ¬p ⊨ ¬qLogic that looks inside propositions, at objects and their properties.
Predicate logic adds predicates, terms and quantifiers, so “every prime greater than two is odd” becomes a formula rather than a single letter. It is strictly more expressive than propositional logic, and no truth table can decide it.
A symbol saying how many objects a predicate holds of.
The two classical quantifiers are ∀ (all) and ∃ (at least one), and each is the negation of the other with a negated body. The variable a quantifier binds is what distinguishes predicate logic from propositional logic.
∀x φ: φ holds of every object in the domain.
A universal claim is refuted by a single counterexample, and it holds vacuously over an empty domain. ∀x φ is equivalent to ¬∃x ¬φ, which is the quantifier counterpart of De Morgan's laws.
∃x φ: φ holds of at least one object in the domain.
An existential claim is established by producing one witness. ∃x φ is equivalent to ¬∀x ¬φ, so either quantifier can be defined from the other together with negation.
Logic extended with “necessarily” (□) and “possibly” (◇).
Modal logic evaluates formulas at possible worlds rather than at a single interpretation: □φ holds when φ holds at every accessible world, ◇φ when it holds at some. Varying what “accessible” means gives the different modal systems.
