Formal Logic and Natural Deduction

A mathematical proof uses logic; formal logic makes the language, semantics, and permitted proof steps explicit. This note develops that second viewpoint. It assumes the practical vocabulary of Mathematical Foundations and complements Boolean Algebra and Boolean Functions, whose main task is representing and transforming Boolean functions.

FIT3080’s logic material motivates the progression from a knowledge base to logical consequences and inference procedures. Here we also develop natural deduction and the restrictions on quantifier rules, which need more space than an AI-oriented introduction provides [1][1] Monash, “FIT3080 Artificial Intelligence: Logic, Inference Algorithms, and First Order Logic, Parts I and II,” 2025. Course lecture materials, Semester 2. Part II reading list: AIMA 4th ed., Sections 7.1--7.5, 8.1--8.3, 9.1, 9.2, 9.5., [2][2] OpenLogicProject, The Open Logic Text. 2026. Complete build, revision 9620cc7, July 12, 2026; CC BY 4.0. https://builds.openlogicproject.org/open-logic-complete.pdf. We use classical first-order logic with nonempty domains and total function interpretations.

Syntax: what counts as a formula?

A signature specifies constant, function, and predicate symbols, together with their arities. Terms name objects: variables and constants are terms, and applying an $n$-ary function symbol to $n$ terms gives another term. Atomic formulas assert a relation between terms, or an equality when equality is included. Connectives combine formulas; quantifiers bind object variables.

ExampleTerms and formulas have different jobs

Suppose $a$ is a constant, $f$ a unary function symbol, and $R$ a binary predicate symbol. Then $f(a)$ is a term and $R(a,f(a))$ is a formula. The expression $\neg f(a)$ is ill-formed: negation applies to a formula, not an object-denoting term. Likewise, $f(R(a,a))$ is ill-formed in this signature.

In ordinary first-order logic, quantifiers range over objects, not predicates or functions. The expression $\forall R\,R(a,a)$ therefore belongs to a different language if $R$ is being quantified as a relation. A formalization starts by choosing a language that can express the intended claim without confusing these categories.

A variable occurrence is bound when a quantifier binds that occurrence; otherwise it is free. In $P(x)\land\forall x\,Q(x)$, the first occurrence of $x$ is free and the occurrence inside $Q$ is bound. A sentence has no free variables. Renaming a bound variable consistently changes notation without changing meaning, provided the new name does not capture another variable.

Semantics: interpretations, models, and consequence

An interpretation $\mathcal M$ supplies a nonempty domain, an object for each constant, a total function for each function symbol, and a relation for each predicate symbol. A variable assignment supplies values for free variables. Thus $\mathcal M,s\models\varphi$ means that $\varphi$ is true under interpretation $\mathcal M$ and assignment $s$. For sentences, the assignment is irrelevant and we write $\mathcal M\models\varphi$.

ExampleThe same syntax, different interpretations

Take the sentence $\forall x\,R(x,x)$. On the integers, interpreting $R$ as $\le$ makes it true; interpreting $R$ as $<$ makes it false. The sentence’s syntax did not change. A model of a theory $T$ is an interpretation that makes every sentence in $T$ true.

For a set of sentences $\Gamma$, logical consequence means

$$\Gamma\models\varphi \quad\text{iff}\quad \text{every model of }\Gamma\text{ satisfies }\varphi.$$

A sentence is valid if it is true in every interpretation, satisfiable if it is true in at least one, and unsatisfiable if it is true in none. Truth in one selected model is weaker than validity. A countermodel to $\Gamma\models\varphi$ must satisfy every premise and falsify the conclusion.

For example, $\Gamma=\{P\to Q,P\}$ entails $Q$. In contrast, $\{P\to Q,Q\}$ does not entail $P$: the assignment $P=\mathrm F,Q=\mathrm T$ is a countermodel. If $\Gamma$ has no model, it entails every sentence in classical semantics, so an inconsistent knowledge base cannot distinguish useful consequences from arbitrary ones.

Classical consequence is monotonic: adding premises cannot invalidate an existing consequence. It can, however, destroy satisfiability. This differs from revisable default reasoning and probabilistic inference; a missing fact alone is not evidence for its negation.

Derivations and natural deduction

The notation $\Gamma\vdash\varphi$ says that a finite derivation of $\varphi$ exists from premises $\Gamma$ in a specified proof system. A rule is a licensed local step; a proof is a sequence or tree of such steps; proof search is the process of finding one. These are distinct objects even when they concern the same conclusion.

Natural deduction organizes rules around introducing and eliminating logical connectives. The following are rules or descriptions of rule schemas, not new premises we may assume without justification.

Connective	Introduction	Elimination
$\land$	From $P$ and $Q$, infer $P\land Q$	From $P\land Q$, infer either conjunct
$\lor$	From $P$, infer $P\lor Q$	From $P\lor Q$ and proofs of $R$ in each case, infer $R$
$\to$	Assume $P$, derive $Q$, then discharge the assumption to infer $P\to Q$	From $P\to Q$ and $P$, infer $Q$
$\neg$	Assume $P$, derive $\bot$, then discharge the assumption to infer $\neg P$	From $P$ and $\neg P$, infer $\bot$

The symbol $\bot$ denotes contradiction. From $\bot$ one may infer any formula in this system. To obtain classical logic, also include a classical principle, such as double-negation elimination from $\neg\neg P$ to $P$. The other listed rules alone do not license every classical argument. Treat $P\leftrightarrow Q$ as an abbreviation for the conjunction of the two implications.

Discharging an assumption

A temporary assumption belongs to a subproof. Discharging it closes that subproof and records a conditional conclusion; it does not make the assumed statement true without conditions.

ProofA conjunction implies its first conjunct

We derive $(P\land Q)\to P$ with no premises.

Line	Formula	Reason and scope
1	$P\land Q$	Temporary assumption, open subproof
2	$P$	$\land$ elimination from 1, inside subproof
3	$(P\land Q)\to P$	$\to$ introduction, discharge lines 1–2

Line 2 is available only while its assumption is active. The final conclusion is the implication, not an unconditional proof of $P$.

For disjunction elimination, there are two temporary assumptions. From $P\lor Q$, prove $R$ under $P$ and separately prove $R$ under $Q$, then discharge both assumptions. It is invalid to pick the more convenient disjunct and proceed as if it were known.

Quantifier rules and their side conditions

Substitution $\varphi[t/x]$ replaces free occurrences of $x$ with the term $t$, avoiding variable capture. The side conditions below are part of the rules, not optional cautions.

• Universal elimination: from $\forall x\,\varphi(x)$ infer $\varphi(t)$, with capture-avoiding substitution.
• Existential introduction: from $\varphi(t)$ infer $\exists x\,\varphi(x)$, for a legitimate instance.
• Universal introduction: prove $\varphi(a)$ for an arbitrary fresh parameter $a$, then infer $\forall x\,\varphi(x)$. The parameter must not occur in any undischarged assumption on which the proof depends, or remain in the generalized conclusion.
• Existential elimination: from $\exists x\,\varphi(x)$, open a subproof assuming $\varphi(a)$ for a fresh parameter $a$. If it yields $\psi$ without $a$ occurring in $\psi$ or the other active assumptions, close the subproof and infer $\psi$.

The last rule allows reasoning with an unknown witness, but prevents smuggling a claim about that particular witness into the conclusion. The quantifier chapters of forall x: Calgary give detailed derivations with these restrictions [3][3] OpenLogicProject, “forall x: Calgary, Chapter 36: Basic Rules for First-Order Logic,” . Natural deduction quantifier rules and their side conditions; accessed September 6, 2026. https://forallx.openlogicproject.org/html/Ch36.html.

ExampleWhy capture matters

In $\forall y\,R(x,y)$, replace free $x$ by $y$. Naively writing $\forall y\,R(y,y)$ would bind the inserted variable and change the claim. First rename the bound variable to $z$, then substitute to obtain $\forall z\,R(y,z)$. The inserted $y$ remains free.

ProofFrom an existing member to an existing qualified member

Suppose $\forall x\,(P(x)\to Q(x))$ and $\exists x\,P(x)$. We prove $\exists x\,Q(x)$.

Line	Formula	Reason and scope
1	$\forall x\,(P(x)\to Q(x))$	Premise
2	$\exists x\,P(x)$	Premise
3	$P(a)$	Fresh witness assumption, open subproof
4	$P(a)\to Q(a)$	$\forall$ elimination from 1
5	$Q(a)$	$\to$ elimination from 3 and 4
6	$\exists x\,Q(x)$	$\exists$ introduction from 5
7	$\exists x\,Q(x)$	$\exists$ elimination from 2 and subproof 3–6

The conclusion contains no $a$, and neither premise mentions it. We have proved existence, without claiming that a previously named individual has property $Q$.

With equality, add reflexivity and substitution of equals: $t=t$, and replacement of a term by an equal term in a formula, avoiding capture. Equality means identity of objects; two different constant symbols need not denote different objects unless distinctness is specified.

Quantifiers: useful laws and invalid moves

Besides the negation laws introduced in the foundations, the following distributions hold:

$$\forall x\,(P(x)\land Q(x)) \equiv (\forall x\,P(x))\land(\forall x\,Q(x)),$$ $$\exists x\,(P(x)\lor Q(x)) \equiv (\exists x\,P(x))\lor(\exists x\,Q(x)).$$

For the first, an arbitrary object satisfies both predicates exactly when each predicate holds of every object. For the second, a witness satisfies at least one predicate exactly when at least one predicate has a witness. The same substitutions with the other connectives are not general equivalences.

For example, on $D=\{0,1\}$ let $P$ mean “is $0$” and $Q$ mean “is $1$.” Every object satisfies $P\lor Q$, but neither predicate holds of every object. Each predicate has a witness, but no object satisfies $P\land Q$. This refutes both the unrestricted distribution of $\forall$ over $\lor$ and of $\exists$ over $\land$.

For a finite, explicitly enumerated domain, a universal quantifier can be expanded into a finite conjunction, and an existential quantifier into a finite disjunction. This is not a general elimination procedure for quantification over an arbitrary or infinite domain. Unique existence is written $\exists!x\,P(x)$ and expands as

$$\exists x\bigl(P(x)\land \forall y\,(P(y)\to y=x)\bigr).$$

Quantifier order controls dependence: $\forall x\exists y\,R(x,y)$ permits a different witness for each $x$, whereas $\exists y\forall x\,R(x,y)$ requires a single common witness. These distinctions become operational when a theorem prover introduces Skolem functions.

Predicates as program specifications

Predicates can describe a program’s precondition and postcondition. A Hoare triple $\{P\}\ C\ \{Q\}$ expresses partial correctness: if execution starts in a state satisfying $P$ and command $C$ terminates, the resulting state satisfies $Q$. It does not by itself prove termination. Total correctness requires that additional property.

For a procedure intended to compute an integer factorial, require input $n\ge 0$ and postcondition $r=n!$, with $0!=1$. These are a specification, not a proof that an arbitrary implementation meets it. The program must be checked against its operational meaning and relevant invariants. This is one application of logical reasoning, beyond treating a predicate simply as a Boolean-valued test.

Consistency, independence, and two meanings of completeness

Consistency and soundness

DefinitionConsistency

A theory $T$ is consistent if there is no sentence $\varphi$ for which both $T\vdash\varphi$ and $T\vdash\neg\varphi$. In classical logic, a contradiction entails every conclusion; consistency excludes this collapse.

Soundness is the assertion that the proof system respects semantics: if $T\vdash\varphi$, then $T\models\varphi$. It does not declare arbitrary axioms true. It says that in a model where the axioms hold, a valid derivation cannot lead to a false conclusion.

ProofSoundness of the listed natural-deduction rules

Induct on the derivation tree, maintaining this invariant: every interpretation and assignment satisfying the undischarged assumptions satisfies the conclusion. An assumption leaf satisfies it immediately. Conjunction introduction and elimination, disjunction introduction, implication elimination, and negation elimination preserve it by their truth tables. For disjunction elimination, at least one disjunct is true, so the induction hypothesis for that branch gives the common conclusion. For implication introduction, either the discharged assumption is false and the implication is true, or it is true and the subproof gives the consequent. Negation introduction works because a true discharged assumption would make the subproof produce falsehood. Falsehood elimination has no interpretation satisfying its premise; double-negation elimination preserves classical truth.

For quantifiers, capture-avoiding substitution obeys the substitution lemma: evaluating $\varphi[t/x]$ equals evaluating $\varphi$ with $x$ assigned the value of $t$. To see this, induct first on terms (variables, constants, then function application), then on formulas: atomic predicates use the term result; connectives preserve equality of truth values; at a quantifier, first rename its bound variable away from the substitution, so varying its value commutes with substituting for $x$. Universal elimination and existential introduction now follow by selecting the value of $t$.

For universal introduction, interpret the fresh parameter as any object. Freshness keeps all active assumptions true, so the subproof establishes the formula for every object. For existential elimination, choose a witness supplied by the existential premise and interpret the fresh parameter as that witness. The subproof gives the conclusion; freshness ensures that changing this parameter affects neither the other assumptions nor that conclusion. Equality reflexivity follows from identity, and substitution of equals preserves term values and hence formula truth by the same structural induction. These cover every listed rule, completing the induction.

Consequently, for a sound proof system, exhibiting a model of $T$ establishes its consistency. Otherwise a sentence and its negation would both have to hold in that model. This method depends on the background mathematics used to construct the model; finitely many successful checks do not establish the consistency of an arbitrary theory.

Independent axioms and independent sentences

An axiom $A\in T$ is independent of the other axioms when

$$T\setminus\{A\}\nvdash A.$$

One way to establish this is to find a model satisfying the remaining axioms in which $A$ is false. Soundness rules out such a model if the other axioms derive $A$.

The related expression “$\varphi$ is independent of $T$” usually requires that neither side be provable:

$$T\nvdash\varphi \quad\text{and}\quad T\nvdash\neg\varphi.$$

For $T=\{P\}$, the assignments $P=\mathrm T,Q=\mathrm T$ and $P=\mathrm T,Q=\mathrm F$ both satisfy the axioms. They show that $Q$ is independent of $T$. Adding either $Q$ or $\neg Q$ selects a smaller class of models. By contrast, in the axiom set $\{P,P\to Q,Q\}$, the final axiom $Q$ follows from the first two and is redundant.

The parallel postulate provides a classical geometric example, but the axioms being retained must be specified. Within a suitable axiomatization of neutral geometry, models satisfying and failing the parallel postulate demonstrate independence. Simply replacing lines with great circles on a sphere does not leave every other postulate unchanged: antipodal points, for example, lie on more than one great circle. The other conditions must also be checked.

Completeness of a theory and completeness of a logic

DefinitionSyntactic completeness of a theory

A theory $T$ is complete if, for every sentence $\varphi$ of its language, either $T\vdash\varphi$ or $T\vdash\neg\varphi$. Consistency additionally prevents both from holding. In the propositional language containing $P,Q$, the theory $T=\{P\}$ is incomplete because it does not decide $Q$.

Semantic completeness of a logic is a different property: every consequence holding in all models of the premises can be obtained using that logic’s proof rules. In symbols,

$$T\models\varphi\quad\Longrightarrow\quad T\vdash\varphi.$$

Classical first-order logic has standard proof systems that are sound and complete. This does not make every first-order theory decide every sentence. If models of a theory disagree about $\varphi$, semantic completeness does not require the theory to prove one side.

Gödel’s incompleteness theorems concern a different limitation: a consistent, effectively axiomatized theory with sufficient arithmetic strength cannot decide every sentence in its language. This does not contradict the completeness theorem for first-order logic, nor does it make every ordinary mathematical problem unsolvable. For now, distinguish the questions answered by the two meanings of completeness; their metamathematical proofs belong to further study [2][2] OpenLogicProject, The Open Logic Text. 2026. Complete build, revision 9620cc7, July 12, 2026; CC BY 4.0. https://builds.openlogicproject.org/open-logic-complete.pdf.

Exercises

ExerciseFind a countermodel

Does $\exists x\,P(x)$ entail $P(a)$? Give a model supporting your answer, and explain why existential elimination does not license this inference.

Show solution

Solution

No. Take domain $\{0,1\}$, interpret $a$ as $0$, and let only $1$ satisfy $P$. The premise is true and conclusion false. Existential elimination uses a fresh parameter inside a subproof; it does not identify the witness with an already interpreted constant.

ExerciseTrack the temporary assumptions

From $P\to R$ and $Q\to R$, derive $(P\lor Q)\to R$ using natural deduction.

Show solution

Solution

Assume $P\lor Q$. In a subproof assuming $P$, use $P\to R$ to derive $R$; in another assuming $Q$, use $Q\to R$ to derive $R$. Discharge the two case assumptions by disjunction elimination. Finally discharge the assumption $P\lor Q$ by implication introduction. The two original implications remain premises.

ExerciseGeneralization is not extrapolation

A proof assumes $P(a)$ and immediately concludes $\forall x\,P(x)$. Which side condition fails? Give a two-object countermodel.

Show solution

Solution

The parameter $a$ occurs in an undischarged assumption on which the conclusion depends, so it is not arbitrary in the required sense. Let $a$ denote $0$ in domain $\{0,1\}$ and let $P$ hold only of $0$. The assumption holds but the proposed conclusion fails.

ExerciseCompleteness does not settle every sentence

In propositional logic with letters $P,Q$, let $T=\{P\}$. Explain why completeness of the proof system does not require a proof of $Q$ or a proof of $\neg Q$ from $T$.

Show solution

Solution

There are models of $T$ with either truth value for $Q$. Therefore neither sentence is a semantic consequence of $T$. Completeness requires proofs of semantic consequences, not a decision between statements on which the models disagree.

From a valid rule to an inference algorithm

A rule tells us which steps are allowed, but does not tell us which step to try first or when a failed search is conclusive. Propositional Automated Reasoning turns model checking, Horn rules, resolution, and SAT into explicit procedures. First-Order Resolution and Theorem Proving then adds substitutions, witness dependencies, and the limits of termination.

References

1. [1] Monash, “FIT3080 Artificial Intelligence: Logic, Inference Algorithms, and First Order Logic, Parts I and II,” 2025. Course lecture materials, Semester 2. Part II reading list: AIMA 4th ed., Sections 7.1--7.5, 8.1--8.3, 9.1, 9.2, 9.5. ↩
2. [2] OpenLogicProject, The Open Logic Text. 2026. Complete build, revision 9620cc7, July 12, 2026; CC BY 4.0. https://builds.openlogicproject.org/open-logic-complete.pdf a b
3. [3] OpenLogicProject, “forall x: Calgary, Chapter 36: Basic Rules for First-Order Logic,” . Natural deduction quantifier rules and their side conditions; accessed September 6, 2026. https://forallx.openlogicproject.org/html/Ch36.html ↩