Back to the on-screen lesson ·
apply universal instantiation to a named object
Paper packet. Every task here also exists on screen, where it is checked automatically; answers written on paper are not assessed by Nydus. When you are back at a device, enter your answers there.
You will apply universal instantiation to a named object, recording the intermediate model values and the precise reason each conclusion follows.
Recall the truth conditions for not, and, or and if-then. Those rules still govern compound formulas here, but atomic truth now comes from objects and predicate extensions or from a world's valuation. Identify which new structure this lesson introduces before using a familiar propositional rule.
| Term | What it means |
|---|---|
| Interpretation | A declared domain and meanings for the nonlogical symbols; a modal interpretation also specifies worlds, accessibility and valuations. |
| Assignment | A choice of domain object for a free variable during an evaluation; it is not itself another domain object. |
| Witness | An eligible object or accessible world satisfying the property required by an existential or possibility claim. |
| Counterexample | An eligible case where the required condition fails; a countermodel to an inference additionally makes every premise true. |
| Validity | Truth in every interpretation of the specified kind, a stronger claim than truth in one supplied model. |
Universal elimination permits a declared term to replace the quantified variable in its scope. From forall x P(x), P(a) follows for a name denoting a domain object. From forall x (P(x) -> Q(x)), the immediate instance is P(a) -> Q(a), not Q(a). A further premise P(a) is needed for modus ponens.
Replace the relevant free occurrences consistently. If a formula has nested quantifiers, an occurrence already bound by an inner quantifier with the same variable letter belongs to that inner scope. Careful variable naming avoids accidental capture. The simple proof audits here use formulas with one displayed outer quantifier and no term-capture complication, so the rule's direction and the matching antecedent remain visible.
Instantiation does not require a fresh name. It uses a term for an object already eligible under the domain. Freshness restrictions arise in other rules, especially existential elimination and generalization from an arbitrary parameter. Mixing their restrictions can make a learner either forbid a legitimate instance or permit an illegitimate generalization.
The audits ask you to produce the instance and its consequence in a stated canonical notation. They check a bounded proof trace, not every possible first-order derivation. The semantic justification is still general: if every object satisfies the quantified formula, the named object cannot be an exception. What happens after instantiation depends on the content of that instance and any additional premises supplied.
Another way: An explicit audit sheet
Keep four parts on the page: the declared objects or worlds, the meaning of each symbol, the intermediate values, and the conclusion. A changed interpretation belongs on a new sheet so the premises and conclusion are never checked in different models.
Premises: forall x (P(x) -> Q(x)), and P(a). The domain is a, b, with each name denoting an object. Complete a proof audit by entering the named conditional instance, its antecedent, and its consequent. Use exactly the displayed notation, such as P(a) -> Q(a), with the appropriate name.
For a, the universal premise supplies P(a) -> Q(a). The separate premise supplies P(a), so this particular conditional can be used to obtain Q(a).
For b, the universal premise supplies P(b) -> Q(b). No separate premise P(b) is supplied. The conditional alone does not tell us whether Q(b) is true; both a false antecedent and a true consequent could make the conditional true.
Conditional instance: P(a) -> Q(a). Universal elimination replaces each free occurrence of the quantified variable in its scope by the same declared term. The entire conditional is instantiated; the universal premise does not license Q of the named object without the antecedent. Keeping both occurrences consistent matters because the rule connects the same object's P-property to its Q-property, not unrelated objects at the two ends.
Antecedent: P(a). The second premise supplies precisely the antecedent of the conditional instance. Match both predicate and argument before using modus ponens. A statement about a different object would not meet this requirement. The named term is permitted here because it denotes a domain object; universal elimination does not require it to be a fresh name or an arbitrary representative for a later generalization.
Consequent: Q(a). Apply modus ponens to the instantiated conditional and the matching antecedent. This is a two-rule argument: universal elimination first, then propositional implication elimination. The proof's scope remains the named object. It does not establish that every object has Q, since other objects may fail P. An object-specific premise cannot be treated as a fact about an arbitrary member of the domain.
Compare universal elimination with universal introduction. Taking a named instance of a universal is immediate when the term is legitimate. Moving in the reverse direction requires an arbitrary-object argument with the appropriate restrictions. One successful named instance never licenses a universal conclusion by itself. The audit makes these rule directions visible while avoiding the false impression that a three-line named proof has checked every object in the domain.
Premises: forall x (P(x) -> Q(x)), and P(b). The domain is a, b, c, with each name denoting an object. Complete a proof audit by entering the named conditional instance, its antecedent, and its consequent. Use exactly the displayed notation, such as P(a) -> Q(a), with the appropriate name.
For a, the universal premise supplies P(a) -> Q(a). No separate premise P(a) is supplied. The conditional alone does not tell us whether Q(a) is true; both a false antecedent and a true consequent could make the conditional true.
For b, the universal premise supplies P(b) -> Q(b). The separate premise supplies P(b), so this particular conditional can be used to obtain Q(b).
For c, the universal premise supplies P(c) -> Q(c). No separate premise P(c) is supplied. The conditional alone does not tell us whether Q(c) is true; both a false antecedent and a true consequent could make the conditional true.
Conditional instance: P(b) -> Q(b). Universal elimination replaces each free occurrence of the quantified variable in its scope by the same declared term.
Antecedent: P(b). The second premise supplies precisely the antecedent of the conditional instance.
Consequent: Q(b). Apply modus ponens to the instantiated conditional and the matching antecedent.
Compare universal elimination with universal introduction. Taking a named instance of a universal is immediate when the term is legitimate. Moving in the reverse direction requires an arbitrary-object argument with the appropriate restrictions. One successful named instance never licenses a universal conclusion by itself. The audit makes these rule directions visible while avoiding the false impression that a three-line named proof has checked every object in the domain.
Premises: forall x (P(x) -> Q(x)), and P(c). The domain is a, b, c, d, with each name denoting an object. Complete a proof audit by entering the named conditional instance, its antecedent, and its consequent. Use exactly the displayed notation, such as P(a) -> Q(a), with the appropriate name.
For a, the universal premise supplies P(a) -> Q(a). No separate premise P(a) is supplied. The conditional alone does not tell us whether Q(a) is true; both a false antecedent and a true consequent could make the conditional true.
For b, the universal premise supplies P(b) -> Q(b). No separate premise P(b) is supplied. The conditional alone does not tell us whether Q(b) is true; both a false antecedent and a true consequent could make the conditional true.
For c, the universal premise supplies P(c) -> Q(c). The separate premise supplies P(c), so this particular conditional can be used to obtain Q(c).
For d, the universal premise supplies P(d) -> Q(d). No separate premise P(d) is supplied. The conditional alone does not tell us whether Q(d) is true; both a false antecedent and a true consequent could make the conditional true.
Conditional instance: P(c) -> Q(c). Universal elimination replaces each free occurrence of the quantified variable in its scope by the same declared term.
Antecedent: P(c). The second premise supplies precisely the antecedent of the conditional instance.
Consequent: Q(c). Apply modus ponens to the instantiated conditional and the matching antecedent.
Compare universal elimination with universal introduction. Taking a named instance of a universal is immediate when the term is legitimate. Moving in the reverse direction requires an arbitrary-object argument with the appropriate restrictions. One successful named instance never licenses a universal conclusion by itself. The audit makes these rule directions visible while avoiding the false impression that a three-line named proof has checked every object in the domain.
Suppose the domain contains three folders, a, b, and c. The premise forall x (Filed(x) -> Indexed(x)) applies to each folder. Instantiating it at b gives Filed(b) -> Indexed(b). It does not give Indexed(b) by itself, because the conditional does not assert its antecedent. You need a separate Filed(b) premise before a conditional inference can establish the result. Universal elimination preserves the entire internal formula while replacing the bound variable consistently.
This becomes especially important with repeated argument positions. From forall x R(x,x), instantiating at b gives R(b,b), not R(b,c). Both occurrences were bound by the same quantifier. From forall x R(x,c), the instance at b is R(b,c), because c was already a fixed name and is not replaced. Marking the bound occurrences before substitution prevents an apparently minor copying error from changing the relation being asserted.
Instantiation moves from a universal assertion to a case. Generalization moves toward a universal assertion and therefore needs a different justification. Observing Filed(a) for a specially selected folder does not establish forall x Filed(x). A model containing an unfiled b demonstrates the gap. In a proof using an arbitrary name, the name must not gain its property from an undischarged assumption specific to that object. The point of arbitrariness is that the reasoning could apply to any domain member.
A finite model gives another route to checking a universal sentence: inspect every member of its explicitly complete domain. That is exhaustive evaluation of this model, not permission to generalize from a sample of the real world. If the folder list is incomplete, unlisted folders remain untested. Keep three tasks distinct: substituting a name into a universal premise, proving a universal claim by arbitrary-object reasoning, and evaluating it by a complete finite inventory. They can reach related formulas, but their warrants and their limitations are different.
A storage policy says that every fragile item must be placed on a padded shelf. Let F(x) mean x is fragile and P(x) mean x is placed on a padded shelf. The formal rule is forall x (F(x) -> P(x)). A checked inventory also says that the item named a is fragile.
Instantiate the whole rule at a: F(a) -> P(a). Then use F(a) with that conditional to obtain P(a). These are separate moves. The first applies a general rule to a named item; the second uses the item's qualifying fact. Skipping the middle conditional makes it easier to overlook the need for that qualifying fact.
Suppose the inventory gives no information about item b. The universal policy still supplies F(b) -> P(b), but it does not by itself give P(b). The item might be non-fragile, in which case the conditional does not require padded storage for it. Nor does P(b) prove F(b): a robust item could be padded for another reason.
In a practical audit, distinguish the policy from a descriptive statement that everybody complies with it. An ought-style rule and a record of actual placement are different kinds of information. The classical proof exercise treats its premises as asserted conditionals and facts within a formal interpretation. Before applying it to a real policy discussion, state whether the conclusion is a required action or a claim about what has already happened. The same symbol sequence should not quietly switch between those readings.
A correct evaluation answers the stated question for its stated interpretation. Do not turn a true instance into a universal rule or a successful example into a proof of validity. When the task is a proof audit, keep local assumptions and fresh parameters within their declared scope.
Record the interpretation and the question.
Premises: forall x (P(x) -> Q(x)), and P(a). The domain is a, b, c, with each name denoting an object. Complete a proof audit by entering the named conditional instance, its antecedent, and its consequent. Use exactly the displayed notation, such as P(a) -> Q(a), with the appropriate name.
Use the declared objects and meanings throughout this calculation: Conditional instance is the first requested result.
Determine the requested value: Conditional instance.
P(a) -> Q(a)
Universal elimination replaces each free occurrence of the quantified variable in its scope by the same declared term.
Determine the requested value: Antecedent.
P(a)
The second premise supplies precisely the antecedent of the conditional instance.
Determine the requested value: Consequent.
Q(a)
Apply modus ponens to the instantiated conditional and the matching antecedent.
Collect the results in the requested order.
P(a) -> Q(a) / P(a) / Q(a)
Each result belongs to its own entry: Conditional instance; Antecedent; Consequent.
Record the interpretation and the question.
Premises: forall x (P(x) -> Q(x)), and P(a). The domain is a, b, c, d, with each name denoting an object. Complete a proof audit by entering the named conditional instance, its antecedent, and its consequent. Use exactly the displayed notation, such as P(a) -> Q(a), with the appropriate name.
Use the declared objects and meanings throughout this calculation: Conditional instance is the first requested result.
Determine the requested value: Conditional instance.
P(a) -> Q(a)
Universal elimination replaces each free occurrence of the quantified variable in its scope by the same declared term.
Determine the requested value: Antecedent.
P(a)
The second premise supplies precisely the antecedent of the conditional instance.
Determine the requested value: Consequent.
Q(a)
Apply modus ponens to the instantiated conditional and the matching antecedent.
Collect the results in the requested order.
P(a) -> Q(a) / P(a) / Q(a)
Each result belongs to its own entry: Conditional instance; Antecedent; Consequent.
Record the interpretation and the question.
Premises: forall x (P(x) -> Q(x)), and P(a). The domain is a, b, c, d, e, with each name denoting an object. Complete a proof audit by entering the named conditional instance, its antecedent, and its consequent. Use exactly the displayed notation, such as P(a) -> Q(a), with the appropriate name.
Use the declared objects and meanings throughout this calculation: Conditional instance is the first requested result.
Determine the requested value: Conditional instance.
P(a) -> Q(a)
Universal elimination replaces each free occurrence of the quantified variable in its scope by the same declared term.
Determine the requested value: Antecedent.
P(a)
The second premise supplies precisely the antecedent of the conditional instance.
Determine the requested value: Consequent.
Q(a)
Apply modus ponens to the instantiated conditional and the matching antecedent.
Collect the results in the requested order.
P(a) -> Q(a) / P(a) / Q(a)
Each result belongs to its own entry: Conditional instance; Antecedent; Consequent.
Test which alteration would change the conclusion.
Compare universal elimination with universal introduction. Taking a named instance of a universal is immediate when the term is legitimate. Moving in the reverse direction requires an arbitrary-object argument with the appropriate restrictions. One successful named instance never licenses a universal conclusion by itself. The audit makes these rule directions visible while avoiding the false impression that a three-line named proof has checked every object in the domain.
The altered interpretation checks the dependence of these answers on the stated model, rather than replacing it during the calculation.
Determine the requested value: Conditional instance.
P(c) -> Q(c)
Universal elimination replaces each free occurrence of the quantified variable in its scope by the same declared term.
Determine the requested value: Antecedent.
Determine the requested value: Consequent.
Premises: forall x (P(x) -> Q(x)), and P(c). The domain is a, b, c, d, e, with each name denoting an object. Complete a proof audit by entering the named conditional instance, its antecedent, and its consequent. Use exactly the displayed notation, such as P(a) -> Q(a), with the appropriate name.
| Computed result | |
|---|---|
| Conditional instance | |
| Antecedent | |
| Consequent |
Premises: forall x (P(x) -> Q(x)), and P(e). The domain is a, b, c, d, e, f, g, with each name denoting an object. Complete a proof audit by entering the named conditional instance, its antecedent, and its consequent. Use exactly the displayed notation, such as P(a) -> Q(a), with the appropriate name.
Replace the bound variable consistently by the supplied name.
b0
The requested entry concerns conditional instance; retain its stated scope.
Match the separate premise to the antecedent.
b1
The requested entry concerns antecedent; retain its stated scope.
Apply implication elimination to the matching pair.
b2
The requested entry concerns consequent; retain its stated scope.
Premises: forall x (P(x) -> Q(x)), and P(c). The domain is a, b, c, d, e, f, with each name denoting an object. Complete a proof audit by entering the named conditional instance, its antecedent, and its consequent. Use exactly the displayed notation, such as P(a) -> Q(a), with the appropriate name.
Conditional instance: b0
Antecedent: b1
Consequent: b2
Premises: forall x (P(x) -> Q(x)), and P(e). The domain is a, b, c, d, e, with each name denoting an object. Complete a proof audit by entering the named conditional instance, its antecedent, and its consequent. Use exactly the displayed notation, such as P(a) -> Q(a), with the appropriate name.
Conditional instance: b0
Antecedent: b1
Consequent: b2
Premises: forall x (P(x) -> Q(x)), and P(e). The domain is a, b, c, d, e, f, with each name denoting an object. Complete a proof audit by entering the named conditional instance, its antecedent, and its consequent. Use exactly the displayed notation, such as P(a) -> Q(a), with the appropriate name.
Conditional instance: b0
Antecedent: b1
Consequent: b2
In a storage audit, P means fragile and Q means padded, and the premises describe the asserted compliance rule and inventory. The data below form the complete invented audit. Premises: forall x (P(x) -> Q(x)), and P(a). The domain is a, b, c, d, e, f, with each name denoting an object. Complete a proof audit by entering the named conditional instance, its antecedent, and its consequent. Use exactly the displayed notation, such as P(a) -> Q(a), with the appropriate name.
Conditional instance: b0
Antecedent: b1
Consequent: b2
Lesson test: one question per skill, one attempt each, no hints. Your answers are checked when you submit.
Premises: forall x (P(x) -> Q(x)), and P(g). The domain is a, b, c, d, e, f, g, with each name denoting an object. Complete a proof audit by entering the named conditional instance, its antecedent, and its consequent. Use exactly the displayed notation, such as P(a) -> Q(a), with the appropriate name.
Conditional instance: b0
Antecedent: b1
Consequent: b2
You can apply universal instantiation to a named object. Reconstruct the three audit entries from a fresh model without consulting the examples; explain what change to the interpretation would change one answer.
14. Complete the next model audit, step 2
P(c)
The second premise supplies precisely the antecedent of the conditional instance.
14. Complete the next model audit, step 3
Q(c)
Apply modus ponens to the instantiated conditional and the matching antecedent.