Rules

If R(x,y) means x trusts y, R(a,b) says a trusts b; R(b,a) says something different. Repeating a term, as in R(a,a), fills both places with the same object. A ternary relation such as S(x,y,z) keeps three roles separate.

Each variable occurrence belongs to its nearest matching quantifier. A sentence has no free variables. Renaming a bound variable preserves meaning only when the renaming avoids capture: ∀x R(x,y) can become ∀z R(z,y), but not ∀y R(y,y).

∀x∃y R(x,y) permits a different y for each x. ∃y∀x R(x,y) requires one shared y. The latter entails the former in a nonempty domain; the converse fails when each of two objects relates only to itself. Consecutive universals can exchange order, as can consecutive existentials.

Use ∀x(Fx → …) for every F, and ∃x(Fx ∧ …) for some F. For a mixed domain of people and projects, ∀x(Px → ∃y(Cy ∧ R(x,y))) requires a coordinator for each project without claiming everything is a project.

Negation switches each quantifier: ¬∀x∃y R(x,y) is equivalent to ∃x∀y ¬R(x,y). To move quantifiers outward into prenex form, rename bound variables apart and never capture a free variable. Moving a quantifier across a conditional's antecedent can switch its kind; simply copying it outward is unsafe.

Reflexive: ∀x R(x,x). Symmetric: ∀x∀y(R(x,y) → R(y,x)). Transitive: ∀x∀y∀z((R(x,y) ∧ R(y,z)) → R(x,z)). Together these define an equivalence relation. Antisymmetry instead says that R(x,y) and R(y,x) imply x=y; it does not prohibit loops.

A strict partial order is irreflexive and transitive. A linear order additionally compares every two distinct objects. Do not confuse a two-step chain with two arrows leaving the same object.

A function is total and single-valued. Injectivity says ∀x∀y(f(x)=f(y) → x=y); surjectivity says ∀y∃x f(x)=y. Neither condition comes for free. Names may denote the same object, and the domain can contain unnamed objects.

Identity substitution works in any argument place, including inside nested functions. From a=b, infer f(a)=f(b); the converse requires injectivity. Replacing an occurrence must not capture a variable.

At most one F: ∀x∀y((Fx ∧ Fy) → x=y). Exactly one F: ∃x(Fx ∧ ∀y(Fy → y=x)). Exactly two Fs: ∃x∃y((Fx ∧ Fy) ∧ (¬x=y ∧ ∀z(Fz → (z=x ∨ z=y)))). Existence, distinctness, and exhaustion are separate requirements.

On the Russellian reading used here, “the F is G” asserts that exactly one F exists and it is G. Negating that entire assertion allows there to be no unique F; asserting that the unique F is not G still requires its existence.

An interpretation supplies a nonempty domain, denotations for names, a set of ordered tuples for each relation, and a total table for each function. Evaluate an open formula relative to a variable assignment. Quantifiers vary their own variable while keeping the other assignments fixed.

A countermodel makes every premise true and the conclusion false. One countermodel disproves validity. Passing every test on a few small domains does not prove validity over all domains: some distinctions require larger or infinite interpretations.

For a universal conclusion, begin with an arbitrary variable using UD. For an existential premise, use a fresh witness inside an open proof; the witness must not escape in the conclusion or justify an unrestricted generalization. To establish a result used by a shortcut rule, prove it with the permitted underlying rules.

□A is true at a world when A holds at every accessible world; ◇A requires at least one accessible world where A holds. With no successors, a box is true and a diamond is false. An argument's local premises constrain the evaluation world. A countermodel keeps every premise true there and makes the conclusion false.

Euclidean means: if w sees u and v, then u sees v. These systems do not form a single linear ladder. KB does not require self-loops; B does. Belief in KD45 can be mistaken, while knowledge in S5 is factive.

∃x□Fx says one object has F at every accessible world; □∃xFx permits different witnesses at different worlds. The exercises state their domain policy. Quantifiers range over the local domain; names and free-variable assignments are rigid across worlds. Predicate extensions are supplied over the outer domain, so predication is meaningful even for an object absent from a world's local domain.

The Barcan formula ∀x□Fx → □∀xFx holds with constant or decreasing domains; its converse □∀xFx → ∀x□Fx holds with constant or increasing domains. Arbitrary varying domains validate neither in general.

KₐA: agent a knows A. E_G A: every agent in G knows A. D_G A: A follows from the group's pooled information, using the intersection of their alternatives. C_G A: A holds throughout all worlds reachable by any finite sequence of group alternatives, including the current world.

[!A]B: after a truthful public announcement of A, B holds in the model restricted to A-worlds. If A is false initially, this announcement conditional is vacuously true. Updating may change whether agents know A.

On an infinite trace, X A means next, F A eventually, G A always, and A U B means strong until: B must eventually occur and A must hold before it. CTL adds path quantifiers A (every path) and E (some path). The displayed finite trace repeats its marked loop forever.

O A: A holds in every ideal alternative; permission is ¬O¬A. These do not imply actual A. In STIT, an agent ensures A when every history in that agent's current choice cell satisfies A; deliberative STIT also requires that A is not already settled across all histories.

[α]A covers every terminating execution of program α; ⟨α⟩A needs one. Semicolon composes programs, ∪ offers a choice, ?A tests A, and α* permits any finite number of repetitions, including zero. μX.A is a least fixed point; νX.A is a greatest fixed point, with X occurring positively.

A □→ B checks B at all closest A-worlds, including all ties. Neighborhood □A asks whether the entire set of A-worlds belongs to the current world's supplied neighborhoods. These exercises state their conventions rather than silently using normal K rules.

In provability logic, □A expresses provability in a specified formal arithmetic theory. GL adds Löb's axiom □(□A → A) → □A. Finite GL frames are transitive and irreflexive; on infinite frames the relevant restriction also excludes infinite forward chains.