Practical guide
Existential Elimination: Keep the Witness Inside Its Subproof
An existential witness is temporary, not an identified named object. A complete seven-line proof shows how to discharge the witness and preserve only the name-free conclusion.
On this page
Use an unnamed witness without identifying it
An existential premise supplies some witness, but it does not identify that witness with a chosen named object. In the cited system, existential elimination opens a subproof using a fresh temporary name. Derive a conclusion that does not contain that name, then discharge the subproof.
From ∃xPx alone, you cannot infer Pa for an already chosen a. Even if a is the first name you write, nothing in the existential premise says the witness is the object a denotes. A temporary c is a proof device, not a discovered real identity.
Definitions and rules: [1] [2].
We use classical nonempty-domain FOL and the existential-elimination rule stated in forall x: Calgary. Proof systems may use different layouts or names for the restriction; check the exact rule your course uses.
See why an arbitrary chosen name can be wrong
Consider the complete original model D={A,B}, a naming A, and P={B}. Then ∃xPx is true because B is P. Pa is false because a denotes A. The existential claim does not let you select A as its witness.
On a narrow screen, scroll inside this table. Keyboard users can focus the region and use the arrow keys.
| Object | P? | Q? | Named by a? |
|---|---|---|---|
| A | False | False | Yes |
| B | True | True | No |
For later comparison, let Q={B} too. The second premise ∀x(Px→Qx) is true: B satisfies both properties, and A is not P. Yet Qa remains false. What follows from the two premises is that some Q exists, not that a is Q.
This separates a valid existence conclusion from an invalid identity commitment. Both depend on the same supplied model; no statistical or real-world assumption is hidden in the example.
Follow the whole seven-line witness subproof
Start with “some P exists” and “every P is Q.” Choose c fresh: it occurs in neither premise. Assume Pc only inside the marked subproof, derive that some Q exists, and carry that name-free result outside.
Download this original labelled diagram
On a narrow screen, scroll inside this table. Keyboard users can focus the region and use the arrow keys.
| Line | Scope | Formula | Rule and dependencies |
|---|---|---|---|
| 1 | Outside | ∃xPx | Premise |
| 2 | Outside | ∀x(Px→Qx) | Premise |
| 3 | Subproof opens | Pc | Assumption; c fresh |
| 4 | Inside | Pc→Qc | ∀E from 2 |
| 5 | Inside | Qc | →E from 3,4 |
| 6 | Inside | ∃xQx | ∃I from 5 |
| 7 | Outside; 3 discharged | ∃xQx | ∃E from 1 and subproof 3–6 |
Download the complete proof and countermodel
Line 6 uses existential introduction to remove c from the result: if this temporary witness is Q, some Q exists. Line 7 cites both the original existential premise and the entire subproof. Simply copying Qc outside at line 7 would not satisfy the rule.
Definitions and rules: [1].
Check three places where the temporary name must be absent
At elimination, check that c does not occur in the existential premise being eliminated, in any undischarged assumption outside the witness subproof, or in the conclusion you carry outside. The local Pc assumption is the intended exception: it is discharged by ∃E.
On a narrow screen, scroll inside this table. Keyboard users can focus the region and use the arrow keys.
| Item checked | Contains c? | Why it matters |
|---|---|---|
| Source ∃xPx | No | c is not already fixed by the source formula |
| Outside premise ∀x(Px→Qx) | No | No open outside assumption privileges c |
| Outside result ∃xQx | No | The witness identity does not escape |
| Local assumption Pc | Yes | Allowed inside the subproof and then discharged |
Freshness is a dependency condition, not an instruction to pick a different real person. Reusing c from another still-open assumption would mix information about a particular object into the existential reasoning. Choose an unused name and record the subproof boundary clearly.
Definitions and rules: [1].
Separate existential elimination from introduction and universal introduction
Existential introduction goes from a permitted instance Qc to ∃xQx; it only asserts that at least one object meets the condition. Existential elimination goes from an existential premise through a fresh-witness subproof to a conclusion independent of its temporary name. They are different operations.
Universal introduction also has a name restriction, but its job is to establish every object satisfies a formula. Do not infer ∀xPx from the witness assumption Pc: that assumption is still open and singles out a P witness. Knowing something exists does not make every object have that property.
The semantic reason for the seven-line proof is simple: a P witness exists, and every P is Q, so that witness is Q. Some Q therefore exists. The proof preserves that reason without pretending to know which previously named object is the witness.
Try three witness-scope checks
Use the model and the fully displayed proof, with no additional premises.
Case 1
From ∃xPx, may an already named a be declared P?
Show answer and explanation for case 1
No.
The two-object countermodel has a naming A while only B is P. Existence alone does not identify a.
Case 2
Could line 7 carry Qc outside instead of ∃xQx?
Show answer and explanation for case 2
No under the displayed ∃E rule.
Qc contains the temporary name c. The outside conclusion must be independent of that name; line 6’s existential conclusion supplies a suitable result.
Case 3
May c appear in the local Pc assumption that ∃E discharges?
Show answer and explanation for case 3
Yes.
That is the purpose of the witness subproof. The forbidden appearances are in the source existential, outside undischarged assumptions and the exported conclusion.
Sources and further reading
- forall x: Calgary, chapter 36: Basic rules for FOLFormal background in complete explanatory chapter, excluding practice exercises. The records, explanations and worked examples on this page are original additions, rather than copied textbook exercises.
- forall x: Calgary, chapter 37: Proofs and strategies for FOLFormal background in complete explanatory chapter, excluding practice exercises. The records, explanations and worked examples on this page are original additions, rather than copied textbook exercises.
- forall x: Calgary — credits, editions and CC BY 4.0 licenseBased on work by P. D. Magnus and Tim Button, revised and expanded by Aaron Thomas-Bolduc and Richard Zach, with further contributions credited by the textbook. Referenced HTML revision: Fall 2025, bb86fe9 (2026-10-22). No author endorsement is implied.