The Gold Standard of Mathematical Logic | Arbitrary Objects, Witnesses and Proof Dependencies

A specified name such as a may already denote an object mentioned in a premise. If P(a) is supplied, it establishes P of that object. It does not establish P of every object.

An arbitrary parameter c is used to reason about an unspecified domain object without relying on special assumptions about it. If the proof establishes P(c) independently of any undischarged c-specific assumption, universal introduction may permit ∀x P(x).

A temporary existential witness c is introduced within a subproof from ∃x P(x). Its property P(c) is assumed locally to derive a conclusion that does not depend on which witness was chosen.

The same letter shape does not give the same permission

All three roles may be written with ordinary lowercase names in a textbook. The role comes from how the symbol entered the proof and which assumptions remain open.

A fresh-looking name is not automatically arbitrary. If the proof immediately assumes P(c), then c has received a special property. Generalising P(c) while that assumption remains open would promote a conditional or local fact into a universal one.

Likewise, a witness is not automatically a particular pre-existing named object. From “someone has P,” choosing the familiar person a without justification can be invalid.

The first practical habit is to annotate introduction points: specified by premise, arbitrary parameter, or local witness. The second is to keep an assumption list beside each derived line.

This small amount of bookkeeping explains many quantifier restrictions. The restrictions are not arbitrary obstacles; they prevent a conclusion from claiming independence that the derivation has not earned.

Contents · Next chapter

To establish ∀x Q(x), consider an arbitrary object c and derive Q(c) without relying on an open assumption that singles c out. Then the reasoning can apply to any domain object.

Suppose the premises are ∀x(P(x) → Q(x)) and ∀x P(x). Neither premise mentions c. Instantiate the first to P(c) → Q(c), instantiate the second to P(c), and apply implication elimination to obtain Q(c).

Because c was arbitrary and no c-specific assumption remains, conclude ∀x Q(x). The same chain would work for any object.

A complete proof ledger

The restrictions are checked at the point of generalisation. The parameter may occur in intermediate derived lines; otherwise the method could never use it. What matters is whether the derivation depends on an undischarged assumption that fixes special facts about c.

Proof systems vary in how they mark arbitrary parameters and state side conditions. Some use a named-object convention; others use free variables or explicit parameter declarations. Follow the exact rule of the system being used.

The explanatory question remains constant: could the same reasoning be carried out for any object without adding a special premise about it? If yes, universal generalisation may be warranted. If no, the proof still has a dependency to discharge or retain in the conclusion.

Contents · Previous chapter · Next chapter

The argument from P(a) to ∀x P(x) is invalid. Use domain {u,v}, assign a to u, and let P hold only of u. The premise is true and the conclusion false.

A proof that writes P(a), then applies universal introduction, violates the arbitrariness condition. The premise already singles out a with property P. There is no reason to extend that property to v.

Changing the letter a to c does not repair the argument. If P(c) remains an undischarged premise, the same countermodel construction applies.

Discharge the right assumption

Suppose the goal is ∀x(P(x) → P(x)). Choose arbitrary c, temporarily assume P(c), reiterate P(c), and discharge that assumption to obtain P(c) → P(c). Now universal introduction can produce the target.

The resulting conclusion does not say every object has P. It says every object satisfies the conditional that if it has P, then it has P. The proof has retained the logical role of the assumption in the implication.

This is why discharge matters. It changes what has been proved under which conditions. It does not erase a line’s history while leaving an unconditional conclusion of the same strength.

A learner who overgeneralises often needs help identifying what was special about the example, rather than another reminder to “be careful.” Ask which premise mentions the object and whether that premise remains open.

Then construct the two-object countermodel. Seeing a second object that lacks P makes the lost dependency concrete. A formal side condition and a semantic failure should explain the same problem from different directions.

Contents · Previous chapter · Next chapter

From ∃x P(x), we know at least one P-object exists, but not which pre-existing name denotes one. Existential elimination introduces a fresh temporary witness c inside a subproof with assumption P(c).

If that subproof derives a conclusion C that does not mention c, and the freshness conditions are met, C can be inferred outside the subproof. The conclusion must not depend on the witness’s identity.

Consider premises ∃x P(x) and ∀x(P(x) → Q(x)), with goal ∃x Q(x). Inside the witness subproof, assume P(c). Instantiate the universal to P(c) → Q(c), derive Q(c), and then infer ∃x Q(x).

The conclusion ∃x Q(x) no longer contains c. It says a Q-object exists, regardless of which original P-witness was used. Existential elimination closes the subproof and exports that witness-independent conclusion.

The witness name is local

The proof does not export P(c) or Q(c) as unconditional facts about a permanently identified object. It exports the quantified conclusion that survived removal of the temporary name.

A familiar everyday analogy is a proof about a lost item: “Some box contains the key. Whichever such box we consider, it is in the storage room. Therefore a box in the storage room contains the key.” The reasoning need not identify the box.

The analogy is explanatory rather than a substitute for the rule. In the formal proof, inspect whether c occurs in the conclusion, the existential premise or other relevant undischarged assumptions, according to the chosen calculus.

Freshness prevents the temporary witness from inheriting unrelated facts attached to an old name. Independence of the conclusion prevents the proof from revealing more identity information than the existential premise supplied.

Contents · Previous chapter · Next chapter

From ∃x P(x) and ∃x Q(x), it does not follow that ∃x(P(x) ∧ Q(x)). The first witness and the second witness may be different objects.

Let domain {u,v}, with P = {u} and Q = {v}. Both existential premises are true, but no object has both properties.

A false proof may use the same temporary name c for the witness of each premise, obtaining P(c) and Q(c), then conjoining them. This silently assumes that the two existential claims share a witness.

Use fresh local names c and d to keep the possibilities separate. The proof can establish that a P-object and a Q-object exist, but it cannot merge them without an additional premise.

What would repair the conclusion?

One repair is ∀x(P(x) → Q(x)) together with ∃x P(x). Then a P-witness also has Q, so the same witness supports the conjunction.

Another is a premise explicitly asserting shared existence, but that already supplies the desired relationship. The point is to identify the missing overlap rather than hide it in notation.

Distinct names do not, conversely, prove distinct objects. Fresh witness parameters are syntactically different for proof control; they need not denote different domain members. Two existential premises might share a witness even though they do not guarantee one.

Thus the correct conclusion is neither “the witnesses are the same” nor “the witnesses are different.” Their identity relation remains unspecified unless further assumptions settle it.

This is a useful bridge to the existence and identity guide: names, witnesses and counts must be interpreted through explicit sameness and distinctness conditions.

Contents · Previous chapter · Next chapter

From ∃x P(x), one cannot infer ∀x P(x). A witness subproof may begin with P(c), but c represents a suitable object, not an arbitrary object about which nothing special was assumed.

Attempting universal introduction while the witness assumption P(c) is open violates the independence condition. The proof would treat an object selected because it has P as representative of every object.

The two-object model with P true only of u refutes the proposed inference. One witness exists, while v lacks the property.

A subtler escape

Suppose from ∃x P(x) a proof claims P(a) for a previously named a. This also overreaches unless other premises connect a to a witness. The existential statement does not locate its witness at a.

In a temporary subproof, even a conclusion containing a fresh c cannot simply be carried outside unchanged. A sentence such as Q(c) depends on the local choice. Generalising it existentially may yield an exportable statement, as in the earlier complete proof.

Ask two questions before closing a witness subproof. Does the proposed external conclusion still contain the temporary name? Does the derivation use any property of that name beyond the permitted witness assumption and the standing premises?

The exact formal restrictions depend on the calculus, but these questions expose the intended safeguard. The external conclusion should hold regardless of which witness the existential premise happens to provide.

An effective correction preserves the valid local work. If Q(c) was legitimately derived, add existential introduction to obtain ∃x Q(x), then discharge through existential elimination. This often turns an invalid witness escape into a correct quantified conclusion.

Contents · Previous chapter · Next chapter

An open assumption is one on which the current derivation still depends. A discharged assumption has been incorporated into a conclusion through a rule such as implication introduction or existential elimination.

Nested proofs create several layers of dependence. A line derived inside a subproof may rely on both its local assumption and outer premises. Closing one layer does not automatically close the others.

For example, to prove ∀x(P(x) → Q(x)) from ∀x(P(x) → R(x)) and ∀x(R(x) → Q(x)), choose arbitrary c. Assume P(c). Derive R(c), then Q(c), using universal instances of the two premises.

Discharge P(c) to obtain P(c) → Q(c). Only then generalise over c. The final result does not assume that every object has P; it says the conditional holds for every object.

A dependency summary

At Q(c), the proof depends on P(c) and the two universal premises. At P(c) → Q(c), the local P(c) dependency has been discharged. The remaining premises contain no c-specific information.

This summary explains why universal introduction is allowed at the later point but not simply on Q(c) while P(c) remains open.

A visual indentation convention or a formal proof checker can help track layers. Neither removes the need to understand which assumptions a line uses. A copied line from a closed subproof may be unavailable outside unless a rule specifically exports it.

The learner should be able to read the proof backwards: identify the final rule, the formula it required and the side conditions it checked. This often reveals a missing discharge earlier than a forward-only reading does.

Contents · Previous chapter · Next chapter

A proof can contain correct formulas but an invalid step where a name’s role changes. Locate that first change rather than treating the entire proof as useless.

If a specified object becomes arbitrary, inspect universal introduction. If a local witness becomes a permanent named object, inspect existential elimination. If two witnesses are merged, inspect their introductions and whether equality was justified.

A formal repair may require weakening the conclusion. That is appropriate when the premises never supplied the stronger result. Adding a new premise simply to save the desired conclusion changes the argument and needs its own justification.

For teaching, pair a syntactic explanation with a finite model. The rule violation identifies the proof error; the model shows that ignoring it can turn true premises into a false conclusion.

Then ask the learner to explain the corrected permission: “c is arbitrary here because no remaining assumption singles it out,” or “the exported existential sentence no longer depends on the witness name.”

Those statements are more transferable than a rule number alone. They connect the formal calculus with the logical promise that the conclusion makes.

Contents · Previous chapter · Next chapter

Exercise 1: legitimate generalisation

From ∀x P(x) and ∀x(P(x) → Q(x)), derive ∀x Q(x). Use a fresh arbitrary c, instantiate both premises, derive Q(c), and generalise. No c-specific assumption remains open.

Exercise 2: a blocked generalisation

From P(a), can ∀x P(x) follow? No. Domain {u,v}, a = u and P = {u} supplies a countermodel. The specific premise prevents treating a as arbitrary.

Exercise 3: an existential conclusion

From ∃x P(x) and ∀x(P(x) → Q(x)), derive ∃x Q(x). Introduce local witness c, derive Q(c), infer ∃x Q(x) inside the subproof, and close it with existential elimination.

Exercise 4: separate witnesses

From ∃x P(x) and ∃x Q(x), assess ∃x(P(x) ∧ Q(x)). It is invalid in general. Use a two-object model with disjoint P and Q extensions.

Exercise 5: discharge before generalising

From ∀x(P(x) → R(x)) and ∀x(R(x) → Q(x)), prove ∀x(P(x) → Q(x)). The local P(c) assumption must be discharged into the conditional before universal introduction.

Transfer check

Take a short proof with a quantified premise. Label each name’s role and list the open assumptions at its final line. Identify one step where a name disappears from the conclusion and explain which rule permits that disappearance.

Then deliberately break the freshness or arbitrariness condition and construct a model showing why the stronger conclusion need not follow. The exercise is complete when rule checking and model checking identify the same dependency mistake.

Contents · Previous chapter · Next chapter

Frequently asked questions

Does fresh mean distinct from every existing object? No. It concerns the parameter’s syntactic role and independence. A fresh name does not assert inequality.

Can a temporary witness be generalised existentially? Yes, when the relevant introduction rule is satisfied. The resulting sentence can help remove the temporary name from the exported conclusion.

Why cannot a witness be treated as arbitrary? It was selected under a special property. The proof may rely on that property.

Do all textbooks write the same side conditions? No. Follow the exact calculus, while understanding which dependencies its restrictions protect.

Connected reading

Return to Mathematical Logic. The quantifier-dependence guide explains witness choices, and the countermodel guide tests invalid promotions.

Sources and scope

Quantifier rules and their side conditions were checked against forall x: Calgary, Basic Rules for FOL and Proofs with Quantifiers, accessed 22 October 2026. The derivations and repairs here are original teaching examples. Rule notation varies; the explanations are not a substitute for a course’s exact formal proof conventions.

Contents · Previous chapter · Continue to Mathematical Logic