Propositional & Predicate Logic

Formal logic works because it refuses to blur three different questions: is this a well-formed expression, what makes it true, and can it be derived by stated rules? Propositional logic answers those questions when whole statements can be treated as indivisible atoms. First-order predicate logic opens the atoms and lets us reason about objects, properties, relations, identity, and quantification. The payoff is not notation for its own sake: it is a disciplined way to find exactly where an inference can fail.

This entry uses classical two-valued logic and standard first-order logic with identity, nonempty domains, and denoting constants. Other logics deliberately change some of these choices, so every theorem below is relative to this declared system.

Three layers that must stay separate #

Syntax

The alphabet, formation rules, and parse tree that determine which expressions are formulas.

Semantics

A mathematical account of truth: valuations for propositional formulas, and structures plus variable assignments for first-order formulas.

Proof theory

A calculus whose rules determine which formulas may be derived from which assumptions.

The layers cooperate, but none defines the others:

flowchart TD
  F["Formula<br/>syntax tree"] --> E["Semantic evaluation"]
  V["Valuation or structure<br/>plus assignment"] --> E
  E --> C["Semantic consequence<br/>premises entail conclusion"]
  F --> R["Rules of inference"]
  A["Assumptions"] --> R
  R --> D["Derivability<br/>a formal proof exists"]
  D -- "soundness" --> C
  C -- "completeness" --> D

The horizontal distinction is the important one. A truth table does not constitute a natural-deduction proof, and a sequence of symbols is not a proof merely because its conclusion happens to be true.

Validity preserves truth; it does not assert that the premises are actually true. A valid argument may start from a false premise. Conversely, an argument whose conclusion happens to be true may still be invalid if there is some admissible situation in which its premises are true and its conclusion false.

Propositional syntax: formulas are trees #

Let $p,q,r,\ldots$ be propositional atoms. A formula $\varphi$ is generated inductively:

$$\varphi ::= p \mid \neg\varphi \mid (\varphi\land\varphi) \mid (\varphi\lor\varphi) \mid (\varphi\to\varphi) \mid (\varphi\leftrightarrow\varphi).$$

The final clause is implicit but essential: nothing else is a formula. This makes formation decidable by parsing and gives every compound formula an immediate decomposition. For example,

$$\neg P\lor(Q\land R)$$

has $\lor$ as its main connective when the usual precedence convention is in force. Its left subtree is $\neg P$ and its right subtree is $Q\land R$. The written line is only a compact serialization of that tree.

Parentheses prevent a change of tree:

• $\neg(P\land Q)$ denies that both hold;
• $(\neg P)\land Q$ asserts that $P$ fails while $Q$ holds;
• $(P\to Q)\to R$ and $P\to(Q\to R)$ are different formulas and are not equivalent.

The inductive syntax is more than a grammar. It licenses structural recursion: define a property for atoms, then define it for a compound from the corresponding properties of its immediate subformulas. Formula evaluation, substitution, size, subformula collection, and structural induction all use this same decreasing tree.

Propositional semantics: truth flows up the tree #

A valuation $v$ assigns each propositional atom either $\mathsf{T}$ or $\mathsf{F}$. The assignment extends recursively:

Material implication is false in exactly one local state: a true antecedent and a false consequent. This explains several facts that otherwise look like arbitrary rules:

$$\varphi\to\psi \equiv \neg\varphi\lor\psi \equiv \neg\psi\to\neg\varphi.$$

The last formula is the contrapositive. The converse, $\psi\to\varphi$, is generally different.

Material implication models a truth condition, not causation or time. “If the build passes, the deployment starts” may be intended as a policy, a causal claim, or a temporal guarantee. Symbolization is correct only after that intended relation has been made explicit.

Truth tables enumerate finite propositional models #

If a formula contains $n$ distinct atoms, it has $2^n$ relevant valuations. A complete truth table evaluates the formula under every one, so it can decide propositional validity, satisfiability, equivalence, and consequence.

Consider three atoms:

• $B$: a badge is accepted;
• $O$: an operator override is active;
• $U$: the door unlocks.

The formula $(B\lor O)\to U$ says that accepted authorization is sufficient for unlocking. The converse $U\to(B\lor O)$ says that authorization is necessary for unlocking.

The seventh row is a countervaluation to the converse: the door is unlocked with neither stated authorization. It also exposes a requirements error. The original implication does not prohibit unauthorized unlocking; it only requires unlocking when authorization is present. If the intended policy is both directions, use $U\leftrightarrow(B\lor O)$.

The basic semantic classifications are different questions over table rows:

Tautology

True under every valuation.

Contradiction / unsatisfiable formula

False under every valuation.

Contingent formula

True under some valuations and false under others.

Logical equivalence

Two formulas have the same truth value under every valuation.

Joint consistency

There is at least one valuation making all formulas in the set true.

For a finite set of propositional premises, consequence has a simple diagnostic row condition:

$$\Gamma\vDash\varphi \quad\Longleftrightarrow\quad \text{no row makes every }\gamma\in\Gamma\text{ true and }\varphi\text{ false}.$$

Truth tables are decisive, but not magically cheap. Doubling the number of atoms squares the row count: 10 atoms need 1,024 rows; 20 need 1,048,576. Decidable by exhaustive enumeration does not mean operationally convenient.

Normal forms expose truth conditions #

A literal is an atom or its negation. A formula is in:

• disjunctive normal form (DNF) when it is a disjunction of conjunctions of literals;
• conjunctive normal form (CNF) when it is a conjunction of disjunctions of literals.

A canonical DNF can be built from satisfying table rows: for each row, conjoin the literals that describe that valuation, then disjoin the row terms. Canonical CNF is dual: for each falsifying row, construct a clause false exactly on that row, then conjoin the clauses.

For exclusive-or of $P$ and $Q$:

$$(P\land\neg Q)\lor(\neg P\land Q) \equiv (P\lor Q)\land(\neg P\lor\neg Q).$$

The left is DNF; the right is CNF. They are two representations of the same truth function. Canonical conversion can grow exponentially, so normal form is not automatically a compression or optimization.

Why first-order logic is a genuine extension #

Propositional logic treats “Mira owns device 1” and “Noah owns device 2” as unrelated atoms. It cannot express that the same relation connects different objects, or quantify over all devices. First-order logic adds internal structure.

A first-order signature declares nonlogical symbols and their arities:

• constant symbols such as $a$;
• $n$-ary function symbols such as $f$;
• $n$-ary predicate symbols such as $P$ or $R$;
• identity $=$.

Terms name or compute objects:

$$t ::= x \mid c \mid f(t_1,\ldots,t_n).$$

Atomic formulas assert predicates or identity:

$$P(t_1,\ldots,t_n) \qquad\text{or}\qquad t_1=t_2.$$

Formulas then close under the propositional connectives and quantifiers:

$$\forall x\,\varphi \qquad\text{and}\qquad \exists x\,\varphi.$$

Arity and argument order are semantic commitments. If $Owns(x,y)$ means “$x$ owns $y$,” then $Owns(m,d)$ and $Owns(d,m)$ need not agree.

Scope, binding, and safe substitution #

A quantifier binds occurrences of its variable inside its scope. Occurrences outside that scope are free. Binding is about occurrences, not merely variable names:

$$P(x)\land\exists x\,Q(x)$$

contains a free occurrence of $x$ in $P(x)$ and a bound occurrence in $Q(x)$. A formula with no free variable occurrences is a sentence or closed formula.

Quantifier order matters:

$$\forall x\,\exists y\,R(x,y)$$

allows the witness $y$ to depend on $x$, while

$$\exists y\,\forall x\,R(x,y)$$

requires one common witness for every $x$.

Substitution must respect binding. Suppose

$$\varphi(x)=\exists y\,Owns(y,x).$$

Naively replacing $x$ with the variable $y$ produces $\exists y\,Owns(y,y)$: the formerly free $y$ has been captured by the quantifier. Rename the bound variable first:

$$\exists z\,Owns(z,x) \quad\Longrightarrow\quad \exists z\,Owns(z,y).$$

The Open Logic substitution module gives this guarded, partial operation explicitly. It does not by itself define the stronger total algorithm that first alpha-renames obstructing binders. Alpha-renaming a bound variable changes notation, not meaning, provided the fresh name does not capture anything: $\forall x\,P(x)$ and $\forall z\,P(z)$ are equivalent.

Structures give the symbols meaning #

Syntax alone leaves $a$, $f$, and $R$ uninterpreted. In the single-sorted Open Logic structure contract, a structure $\mathcal M$ for a signature supplies:

1. a nonempty domain $D$;
2. an element $c^{\mathcal M}\in D$ for each constant $c$;
3. a total function $f^{\mathcal M}:D^n\to D$ for each $n$-ary function symbol;
4. a relation $R^{\mathcal M}\subseteq D^n$ for each $n$-ary predicate;
5. ordinary equality on $D$ for identity.

A variable assignment $s$ maps every variable to a domain element. Term values are recursive:

$$\begin{aligned} \mathop{\mathrm{Val}}^{\mathcal M}_s(c) &= c^{\mathcal M},\\ \mathop{\mathrm{Val}}^{\mathcal M}_s(x) &= s(x),\\ \mathop{\mathrm{Val}}^{\mathcal M}_s(f(t_1,\ldots,t_n)) &=f^{\mathcal M}(\mathop{\mathrm{Val}}^{\mathcal M}_s(t_1),\ldots, \mathop{\mathrm{Val}}^{\mathcal M}_s(t_n)). \end{aligned}$$

Satisfaction, written $\mathcal M,s\vDash\varphi$, follows the formula tree. Atomic predicates inspect relation membership; connectives use the classical clauses. Quantifiers change one assigned variable at a time. If $s[x\mapsto d]$ agrees with $s$ except that it maps $x$ to $d$, then:

$$\begin{aligned} \mathcal M,s\vDash\forall x\,\varphi &\Longleftrightarrow \text{for every }d\in D,\ \mathcal M,s[x\mapsto d]\vDash\varphi,\\ \mathcal M,s\vDash\exists x\,\varphi &\Longleftrightarrow \text{for some }d\in D,\ \mathcal M,s[x\mapsto d]\vDash\varphi. \end{aligned}$$

This assignment machinery is necessary because a domain element need not have a constant symbol naming it. Quantifiers range over objects, not over the written names available in the language.

For a sentence, all variable occurrences are bound. Its truth therefore does not depend on the initial assignment: every relevant variable value is supplied by a quantifier. This can be proved by structural induction; the stronger induction statement says that satisfaction depends only on assignments to variables free in the formula.

A finite model makes quantifier order visible #

Use one domain containing both people and devices:

$$D=\{\text{mira},\text{noah},d_1,d_2\}.$$

Interpret predicates as:

$$\begin{aligned} Person^{\mathcal M}&=\{\text{mira},\text{noah}\},\\ Device^{\mathcal M}&=\{d_1,d_2\},\\ Owns^{\mathcal M}&=\{(\text{mira},d_1),(\text{noah},d_2)\}. \end{aligned}$$

Now compare:

$$\forall x\bigl(Device(x)\to \exists y(Person(y)\land Owns(y,x))\bigr) \tag{1}$$

and

$$\exists y\bigl(Person(y)\land \forall x(Device(x)\to Owns(y,x))\bigr). \tag{2}$$

Sentence (1) is true: for $d_1$, choose Mira; for $d_2$, choose Noah. The witness may change with $x$. Sentence (2) is false: neither person owns both devices. The formulas differ only in dependency structure, but that is exactly what quantifier order expresses.

The predicates Person and Device are guards because this is single-sorted FOL. Without Device(x)\to, the universal would assert the ownership condition for people as well as devices.

Translation patterns follow from semantics #

Patterns are useful only when their truth conditions are understood:

The universal conditional is vacuously true when there are no $P$ objects. That is not a loophole; it reflects that “every P is Q” makes no existence assertion. Add $\exists xP(x)$ if existence is part of the requirement.

Quantifier negation is also semantic, not a symbol-shuffling trick:

$$\neg\forall x\,P(x)\equiv\exists x\,\neg P(x), \qquad \neg\exists x\,P(x)\equiv\forall x\,\neg P(x).$$

“Not every request succeeded” means at least one failed; it does not mean every request failed.

Models, theories, and countermodels #

A structure is a model of a sentence when it satisfies it, and a model of a theory $T$ when it satisfies every sentence in $T$. The semantic notions lift from propositional valuations to all first-order structures:

• $\varphi$ is satisfiable if some structure and assignment satisfy it;
• a sentence is valid if every structure satisfies it;
• $\Gamma\vDash\varphi$ if every structure and variable assignment satisfying every formula in $\Gamma$ also satisfies $\varphi$; when $\Gamma$ and $\varphi$ are sentences, the assignment is irrelevant and this reduces to the usual model formulation.

This distinction defeats a common error: truth in one intended structure is not logical validity. The sentence “every device has an owner” may be true in the model above, but another perfectly admissible structure can make it false.

Consider the inference

$$\forall x(P(x)\to Q(x)),\quad \exists xQ(x) \quad\therefore\quad \exists xP(x).$$

It is invalid. Take $D=\{a,b\}$, $P^{\mathcal M}=\varnothing$, and $Q^{\mathcal M}=\{a\}$. The universal premise is vacuously true, the existential premise is true, and the conclusion is false. This is predicate-level affirming the consequent.

A formal theory fixes the syntactic game #

A convenient presentation of a formal deductive theory is a triple

$$\mathcal D=(\mathcal L,\mathsf{Ax},\mathsf R),$$

where:

1. $\mathcal L$ specifies the alphabet, finite expressions, and formation rules;
2. $\mathsf{Ax}$ is a set of axioms or axiom schemata in that language;
3. $\mathsf R$ is a set of inference rules, including every side condition that controls their use.

The axioms need not be a finite list: they may be given by finitely many schemata or as another specified set. Whether axiom instances and rule applications are effectively recognizable is an additional computational property. Nor are axioms automatically “truths.” The triple first defines a syntactic object; an interpretation and a soundness theorem are needed before its derivations acquire a truth-preservation guarantee.

A derivation from assumptions $\Gamma$ is a finite sequence or finite proof tree in which every line is an assumption from $\Gamma$, an axiom instance, or the result of an allowed rule applied to earlier lines. A theorem is a formula with a derivation from no undischarged assumptions. Thus the theorem set is generated by the presentation:

$$\mathop{\mathrm{Th}}(\mathcal D) =\{\varphi\mid \varnothing\vdash_{\mathcal D}\varphi\}.$$

Some texts use “theory” instead for a set $T$ of sentences, often one already closed under consequence. Context must therefore reveal whether $T$ names premises to be modelled, or $\mathcal D$ names the language-and-rules machinery that generates proofs.

Derivability and consequence are different relations #

A proof system gives local inference rules. For example, implication elimination (modus ponens) is:

$$\frac{\varphi\qquad\varphi\to\psi}{\psi}.$$

From premises $P\to Q$ and $P$, a three-line derivation records both premises and derives $Q$ by that rule. More complex natural-deduction systems use subproofs: assume a formula temporarily, derive a consequence, then discharge the assumption under an introduction rule.

Quantifier rules need side conditions. To infer a universal statement, the chosen object must be genuinely arbitrary; it cannot depend on a special undischarged assumption. To instantiate a universal, the substituted term must be free for the bound variable. These restrictions are what make the rules preserve meaning.

Write $\Gamma\vdash_{\mathcal D}\varphi$ when a derivation exists in the selected calculus. This is a finite syntactic certificate and can change when the calculus changes; in an effective calculus, a proposed certificate is mechanically checkable. By contrast, $\Gamma\vDash\varphi$ quantifies over models and does not mention proof rules. For a standard classical natural-deduction calculus, two separate metatheorems connect the relations:

$$\underbrace{\Gamma\vdash_{\mathcal D}\varphi \Longrightarrow\Gamma\vDash\varphi}_{\text{soundness}}, \qquad \underbrace{\Gamma\vDash\varphi \Longrightarrow\Gamma\vdash_{\mathcal D}\varphi}_{\text{semantic completeness}}.$$

Soundness says the calculus cannot certify a semantic counterexample. Completeness says semantic consequence is not stronger than what the calculus can prove. These are properties to establish for a specified language, semantics, and calculus—not definitions that make axioms true by decree.

The definition of consequence does not require satisfiable premises. If no model satisfies every member of $\Gamma$, then $\Gamma\vDash\varphi$ holds vacuously for every $\varphi$. Standard classical calculi mirror this through explosion, but the resulting argument says nothing informative about which conclusion holds in an intended real-world model; it exposes an inconsistent premise set.

The craft of direct proof, contradiction, contrapositive, and induction belongs in Proof Techniques & Induction. Here the essential point is the contract between a formal derivation and semantics.

Resolution turns consequence into refutation #

Resolution works with clauses. Treat a clause as a finite set of literals, interpreted as their disjunction. Repeated literals therefore disappear, order is irrelevant, and the empty clause $\square$ is the empty disjunction—false under every valuation. A clause set $S$ is interpreted conjunctively:

$$v\vDash S \quad\Longleftrightarrow\quad \forall C\in S:\ v\vDash C.$$

The empty set of clauses is therefore true under every valuation, while a clause set containing the empty clause is unsatisfiable. Confusing those two empty objects reverses the meaning of a refutation.

For propositional clauses, choose a pivot atom $A$ that occurs positively in one parent and negatively in the other. If the parents are written as $C\cup\{A\}$ and $D\cup\{\neg A\}$, the binary resolution rule is exactly

$$\frac{C\cup\{A\}\qquad D\cup\{\neg A\}} {C\cup D}.$$

The chosen complementary pair is removed and the remainders are united. If the resolvent contains both some atom and its negation, it is a tautological clause and contributes no constraint.

The rule is sound. Let a valuation satisfy both parents. If it makes $A$ false, the first parent can be true only through some literal in $C$; if it makes $A$ true, the second parent can be true only through some literal in $D$. In either case it satisfies $C\cup D$. Adding a resolvent therefore cannot destroy any model of the current clause set, and deriving $\square$ certifies that the original set had no model.

Refutation workflow #

To prove a finite propositional consequence $\Gamma\vDash\varphi$:

1. Add the failure case $\neg\varphi$ to the premises.
2. Convert $\Gamma\cup\{\neg\varphi\}$ to a clause set. Equivalence-preserving CNF conversion is sufficient; a transformation that is only equisatisfiable is also sufficient for refutation, but it does not license claiming that the transformed formula is logically equivalent to the original.
3. Repeatedly add sound resolvents, recording both parent clauses and the pivot literal.
4. Derive $\square$. Then $\Gamma\cup\{\neg\varphi\}$ is unsatisfiable, so no countervaluation to $\Gamma\vDash\varphi$ exists.

A Tseitin-style conversion illustrates the distinction in step 2. It introduces a fresh atom $p_\psi$ for a subformula $\psi$, adds clauses constraining $p_\psi\leftrightarrow\psi$, and asserts the atom naming the root. Every model of the original formula extends to a model of the new clause set, and projecting every model of that clause set onto the original atoms recovers a model of the original. That is equisatisfiability across vocabularies, not ordinary equivalence under one unchanged valuation space.

The logical reduction behind the procedure is

$$\Gamma\vDash\varphi \quad\Longleftrightarrow\quad \Gamma\cup\{\neg\varphi\}\text{ is unsatisfiable}.$$

Worked refutation: a three-step implication chain #

Prove

$$(P\to Q),(Q\to R),P\vDash R.$$

Clausify the premises and add the negated goal:

Now resolve while preserving the proof trace:

$$\begin{aligned} C_5&=\neg Q && \mathop{\mathrm{res}}(C_2,C_4;R),\\ C_6&=\neg P && \mathop{\mathrm{res}}(C_1,C_5;Q),\\ C_7&=\square && \mathop{\mathrm{res}}(C_3,C_6;P). \end{aligned}$$

The last line is not merely “a contradiction appeared.” It is a checkable certificate: every possible valuation satisfying the four input clauses would also have to satisfy each sound resolvent, but no valuation satisfies $\square$. Hence the premises semantically entail $R$.

Completeness requires a complete search #

Propositional resolution is refutation-complete:

$$S\text{ is unsatisfiable} \quad\Longleftrightarrow\quad S\vdash_{\mathrm{res}}\square$$

for a finite propositional clause set $S$. This is narrower than saying that any sequence of resolution choices will find the refutation. A search is fair when every eligible inference whose parents remain available is eventually considered, unless a sound redundancy rule makes it unnecessary. A clause set is saturated when every possible nonredundant resolvent is already present or redundant.

With $n$ propositional atoms there are at most $3^n$ non-tautological set-clauses: each atom is absent, positive, or negative. Exhaustive closure therefore terminates after duplicate and tautology removal. If that saturated closure contains no $\square$, refutation completeness licenses the conclusion that the clause set is satisfiable. Stopping one branch, reaching one nonempty clause, or merely failing to notice another resolvable pair licenses no such conclusion. For example, doing nothing useful with the unit clause $\{Q\}$ in the clause set $\{\{P\},\{\neg P\},\{Q\}\}$ does not erase the immediate refutation between $\{P\}$ and $\{\neg P\}$.

First-order resolution crosses the unification boundary #

The propositional rule matches complementary atoms literally. First-order clauses contain variables and terms, so literals may become complementary only after substitution. For example, the atoms $P(x)$ and $P(f(a))$ have most-general unifier

$$\theta=\{x\mapsto f(a)\}.$$

Applying $\theta$ to the entire parents before deleting the pivot turns

$$\{P(x),Q(x)\}, \qquad \{\neg P(f(a)),R(a)\}$$

into a resolvent $\{Q(f(a)),R(a)\}$. Variables in different parent clauses must first be standardized apart. A candidate substitution must also pass the occurs check: $x$ cannot denote the finite term $f(x)$. Robinson's original resolution calculus makes this combination of substitution, most-general unification, and clause resolution explicit.

This extra machinery is not optional decoration. A complete first-order resolution calculus must state its clausification, Skolemization, variable-renaming, unification, and factoring conventions. Factoring unifies same-sign literals within one clause and retains one common instance. For example, factoring

$$\{P(x),P(f(y)),Q(x)\}$$

with $\{x\mapsto f(y)\}$ yields $\{P(f(y)),Q(f(y))\}$. Robinson's generalized rule instead selected and unified nonempty literal subsets from both parents, absorbing the multi-literal merge into the resolution inference. The separate factoring rule above is the common modern decomposition, not a verbatim rule named in the 1965 paper.

Skolemization preserves satisfiability for the refutation task; it is not in general an equivalence-preserving rewrite in the original vocabulary. The bare propositional pivot rule does not, by itself, establish first-order completeness.

Even with a sound and refutation-complete first-order calculus, proof search changes character. A fair search will eventually derive $\square$ from an unsatisfiable finite clause set, but the space of terms and clauses can be infinite. On a satisfiable input it may run forever. First-order resolution is therefore a semi-decision procedure for unsatisfiability, not a terminating satisfiability test.

Completeness, decidability, and incompleteness are different axes #

A theory $T$ is syntactically consistent in a specified classical calculus when $T\nvdash\bot$. Equivalently, there is no sentence $\varphi$ for which both $T\vdash\varphi$ and $T\vdash\neg\varphi$. This proof-theoretic notion is distinct from merely having premises that sound plausible. Soundness gives satisfiable $\Rightarrow$ syntactically consistent; the completeness theorem for standard classical first-order logic supplies the converse.

Three results that sound similar must not be collapsed:

The first-order completeness theorem says

$$\Gamma\vDash\varphi\Longrightarrow\Gamma\vdash\varphi.$$

Syntactic completeness of a theory $T$ is a different property:

$$\text{for every sentence }\varphi, \quad T\vdash\varphi\text{ or }T\vdash\neg\varphi.$$

There is no conflict between a semantically complete proof calculus for first-order logic and an arithmetical theory that is syntactically incomplete. In a standard form, the first incompleteness theorem applies to a consistent, effectively axiomatized theory strong enough to represent an adequate amount of computable arithmetic; it yields a sentence that the theory neither proves nor refutes. Under further standard derivability conditions, the second theorem says that such a theory cannot prove an appropriate internal statement expressing its own consistency.

These conclusions do not apply to every formal system, and in particular not to ordinary classical propositional logic. They do not say that the independent sentence is merely difficult, that every undecidable computational problem is a Gödel sentence, or that “all thought is impossible to formalize.” Nor do they make model semantics exclusive to classical logic: nonclassical systems, including intuitionistic logic, have semantics designed for their proof principles. The dedicated treatment is Gödel Numbering & Incompleteness Theorems.

Failure diagnostics #

When a formalization or inference looks suspicious, check in this order:

1. Language: Which symbols and arities exist? What semantic conventions were chosen?
2. Parse: Is the expression well formed? What is its main connective and quantifier scope?
3. Binding: Which occurrences are free? Would a substitution capture any variable?
4. Question type: Truth in one model, satisfiability, validity, consequence, or derivability?
5. Counterexample: Can a small valuation or finite structure make the premises true and conclusion false?
6. Rule side conditions: Were assumptions discharged correctly? Was the generalized object arbitrary?
7. Translation: Did natural-language ambiguity get resolved, or merely hidden behind symbols?

Exercises #

1. Parse $\neg(P\to Q)\lor R$ as a tree and identify the scope of each connective.
2. Find a countervaluation to $P\to Q\vDash Q\to P$.
3. Express exclusive-or in CNF and DNF, then verify their equivalence.
4. In the people/device model, add $(\text{mira},d_2)$ to Owns. Which of sentences (1) and (2) change truth value?
5. Decide whether $\forall x\exists y\,R(x,y)\vDash\exists y\forall x\,R(x,y)$ and justify with a proof or countermodel.
6. Explain why substituting $y$ for free $x$ in $\forall y\,R(x,y)$ is unsafe, and perform a safe substitution.
7. Refute or validate: $\forall x(P(x)\lor Q(x))\vDash(\forall xP(x))\lor(\forall xQ(x))$.