# Proof Using Model Universe

Suppose I am trying to prove the following argument

(∀x)(Cx → Dx), (∀x)(Ex → ~Dx), /∴ (∀x)(Ex → ~Cx)

Now, let's also assume that I don't know if this argument is valid or not. Because of this, I try to check for invalidity using the model universe method (even though it would be easy enough to construct a direct proof).

I start by restricting the domain to D = {a}, and I check the following argument for a situation where I have true premises and a false conclusion.

Ca → Da, Ea → ~Da, /∴ Ea → ~Ca

Obviously, I can't find a counter-example, so I continue to expand the domain to D = {a, b}, D = {a, b, c}, etc.

Now, there is a theorem for the model universe method that states, "If n is the number of predicate variables in an argument, 2^n is the upper bound of elements you can test in a domain before you can determine that the argument is valid."

If I test the above argument using the model universe method to the point that my domain includes 8 (2^n) elements, have I just constructed a formal proof? Would I be able to use the model universe method as a means to formally prove an argument?

Thanks.

Edit:

This problem was not taken from a book, but we're going to define a formal proof as "a finite sequence of well-formed formulas, each of which is an axiom, an assumption, or follows from the preceding sentences in the sequence by a rule of inference." And yes, this is in the context of monadic predicate calculus.

• Are you following some text or other source? The answer may depend on what their definition of "formal proof" is. Sep 29, 2019 at 23:58
• @Conifold Thanks for your interest in the question. I just edited it for clarification. Sep 30, 2019 at 0:05
• So are you only allowed to use axioms and rules of inference of monadic predicate calculus in a "formal proof"? Because setting up models and proving the completeness theorem you mentioned requires other means, such as set theory and maybe induction. Using them will not make a "formal proof in monadic predicate calculus". Sep 30, 2019 at 0:10

• @Conifold It is, though: for each of the finitely many isomorphism types we can find a sentence $\psi$ characterizing it up to isomorphism (every finite structure in a finite language has such a sentence); the model checking then amounts to proving that each such $\psi$ implies the theorem we want, together with the proof of the model checking theorem above. The casework is entirely formalizable inside the object theory. Sep 29, 2019 at 23:59