4

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.

N. Bar
  • 297
  • 1
  • 7
  • Are you following some text or other source? The answer may depend on what their definition of "formal proof" is. – Conifold Sep 29 '19 at 23:58
  • @Conifold Thanks for your interest in the question. I just edited it for clarification. – N. Bar Sep 30 '19 at 00: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 '19 at 00:10

1 Answers1

5

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).

Noah Schweber
  • 3,220
  • 1
  • 15
  • 19
  • 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 '19 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. – Noah Schweber Sep 29 '19 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 '19 at 00:03
  • @Conifold See my edit. – N. Bar Sep 30 '19 at 00: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. – Noah Schweber Sep 30 '19 at 00:04
  • I agree that it is formalizable, and that it can be converted into a formal proof in the narrow sense. But it isn't itself a formal proof in monadic predicate calculus. For one, the latter does not even have expressive means to talk about sets, i.e. models. – Conifold Sep 30 '19 at 00:13
  • @Conifold That's fair - I've added a bit to say what needs to go into the formalization. – Noah Schweber Sep 30 '19 at 00:13
  • Maybe a preamble on the dependence of "formal proof" on a formal system it is given in might also help, I think the OP is somewhat inexperienced. – Conifold Sep 30 '19 at 00:15
  • @Conifold Not inexperienced (though I might be in more general philosophy), I think this question just got a bit out of hand as I was asking something much simpler than was interpreted. Basically, could I hand a mathematician a "proof" using the model universe method and have him not laugh at me and go, "this isn't a proof!" – N. Bar Sep 30 '19 at 00:17
  • @N.Bar Ah - in *that* sense, it's certainly a proof. But it's important to distinguish between the informal notion of "rigorous proof" and actual *formal proofs*. – Noah Schweber Sep 30 '19 at 00:24
  • @Conifold I think you're right (regardless of the OP, certainly for other readers) - I don't have time to do that right now, but within the next couple hours I'll improve this. – Noah Schweber Sep 30 '19 at 00:24