A possible finite universe is made by choosing an appropriate number of constants and then using them to translate or expand the quantified function into a proposition. In that model universe it has the meaning expressed by the quantifier. The proposition either states that ALL instantiations are true, or that SOME are. So, an expansion consists of a number of instantiations of the quantified function. There is one instantiation per individual constant in the model.

If there is more than one individual, then the instantiations are separated by a • for a universal quantifier or by a ∨ for an existential.

{ } are needed to build well formed translations and will be added by LogicCoach if you leave them out.

Thus Aa ∨ Ab ∨ Ac will become {Aa ∨ Ab} ∨ Ac.

But mixtures of operators, such as Aa ∨ Ab • Ac, will be rejected.

To make this construction easier, use the instantiation editor (in the Options Menu) to copy the function in the scope of the quantifier. Move the cursor underneath the quantifier in the line ABOVE the cursor and press <Alt>+O + I.

Then when you press the key for a constant in the possible universe, it will produce an instantiation to that constant.

A second press of <Alt>+ O + I in the SAME line will clear it.

An alernative is found on the tool bar at the top of the screen. There, pressing the button for a function of the constant will instantiate (without having to first place the cursor under the quantifier).

xyz are individual variables and not individual constants. So, they canNOT appear in an expansion. A list of acceptable constants appears on the toolbar and at the top of the work screen after <Alt>+ O + I has been used to copy. Using the wrong constant will result in an error message

It is important to pick a large enough finite universe. One way to do this is to count constraining features of the argument. These are:

1. Individual constants such as the n in the first premise of

2. Premises with existential main operators such as the second premise above.

3. Conclusions with universal main operators such as the one above.

For the argument above the count is 3 so a 3 member possible finite universe would be created. A smaller number might do, but 3 will be enough. The translated argument is

Note that each translated (expanded) line preserves the structure of the original line. Thus the main operators correspond. In the original argument and in the expansion, PREMISE 1 has a ≡ main operator (MO).

The original PREMISE 2 has an existential MO. So, the MO of the translated premise is the ∨ that connects the instantiations of the quantifier.

The original CONCLUSION has a universal MO. So, the MO of the expanded conclusion is the • that connects the instantiations of the quantifier.

The goal for the translated argument is to prove it invalid by proving that it can have TRUE premises and a FALSE conclusion. If this goal cannot be met, then return to the expansion screen and RESIZE the finite universe. A universe that is too SMALL will constrain the model to be valid.

The text suggests using multiple cases as in Section 6.5. However, this is never necessary. If you think that you need multiple cases, then either you have overlooked a consistent set of assignments or the size of the finite universe is too small. The LogicCoach has no provision in this Section for creating multiple cases.

One trick is too satisfy the goal for each expanded quantifier with the properties of a DIFFERENT constant. For example, try to make PREMISE 1 true with the properties of a and then use b to make PREMISE 2 true. But, in dealing with quantifiers, do NOT assign any values to an individual constant in the statement of the original argument unless it is necessary.

In the example above, do not use the properties of n to make premise 2 true or to make the conclusion false since in the original argument those lines did not contain n. Instead assign Fa in one and Fb in the other.

Start with the lines WITHOUT quantifiers. Then do the existential main operators in the premises, followed by a conclusion with a universal main operator. Only when these goals are met, look at the other parts of the argument. Then, if the finite universe is big enough, you should be able to find additional assignments to prove the model invalid.

Finish by assigning Fn true which will make premise one true.