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.

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

1 Answer 1

Reset to default
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).

Improve this answer
11
  • 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
    Commented 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.
    – Noah Schweber
    Commented 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
    Commented Sep 30, 2019 at 0:03
  • @Conifold See my edit.
    – N. Bar
    Commented 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.
    – Noah Schweber
    Commented Sep 30, 2019 at 0:04

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .