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?



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.
    – Conifold
    Sep 29, 2019 at 23:58
  • @Conifold Thanks for your interest in the question. I just edited it for clarification.
    – N. Bar
    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".
    – Conifold
    Sep 30, 2019 at 0:10

1 Answer 1


Yes-ish: it takes some work to formalize it, but it can be done.

Specifically, the proof of the relevant model checking theorem gives a general method for proving, for an appropriate sentence p, a sentence of the form "If q_i implies p for each i < n, then p is true" where n is the appropriate bound and {q_i: i < n} are sentences characterizing each of the relevant finite isomorphism types. Each individual model check in turn is formalized as a proof of "q_i implies p." Putting this together gives a formal proof of p.

However, keep in mind that that theorem only holds when our language consists entirely of unary relation (or predicate, if you prefer) symbols. Since that's really a very rare situation, I'd say it's a good idea to avoid it when possible (especially in a case like this where it's much harder than the proof not using the theorem).

  • I am not sure what the intended meaning of a "formal proof" is in the OP. Using a model argument, even together with a proof of the completeness (meta)theorem, is not really a "formal proof" in the object theory (monadic predicate calculus, I presume).
    – Conifold
    Sep 29, 2019 at 23:57
  • @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
  • This uses metatheoretic means beyond the ones of the theory itself. I am just not sure what his textbook allows as "formal proofs". If it interprets "formal proof" as syntactic, semantic means are off-limits. But if it just means "rigorous" in some loose sense, they would be ok.
    – Conifold
    Sep 30, 2019 at 0:03
  • @Conifold See my edit.
    – N. Bar
    Sep 30, 2019 at 0:04
  • @Conifold No it doesn't: the formalized version of that instance of the model checking theorem does exactly this. It really is straightforwardly formalizable. Sep 30, 2019 at 0:04

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.