Re: Decidability of monadic fragment of FOL

On Sun, 18 Nov 2007 15:51:14 +0000, Alan Smaill
<smaill@xxxxxxxxxxxxxxxx> wrote:

David C. Ullrich <ullrich@xxxxxxxxxxxxxxxx> writes:

On Sat, 17 Nov 2007 12:49:23 -0800 (PST), Charles
<niburu1@xxxxxxxxxxx> wrote:

On Nov 17, 4:35 pm, David C. Ullrich <ullr...@xxxxxxxxxxxxxxxx> wrote:
On Fri, 16 Nov 2007 09:15:20 -0800 (PST), nibu...@xxxxxxxxxxx wrote:
I don't get the proof of the decidability of the monadic fragment of
FOL in Boolos, Burgess and Jeffrey (BBJ). First they prove

1. for every formula A of L (L = the language of the monadic fragment
without identity, say), if A has a model, then it has a finite model.

And then they prove

2. for every A of L involving exactly one variable, if A has a model,
then it has a finite model;
3. every A of L is equivalent to a B of L involving only one variable.

Then they claim that the decidability of L is "immediate" from (2) and
(3). Why can't I see the immediate proof? I can only see it giving one
half of the solution to the decision problem (i.e. for proving that
there is an effective procedure for showing invalidity). For suppose A
is not valid. Then ~A has a finite model. Then run through an
enumeration M_1,... of the finite models (perhaps just those in the
signature of A) testing at each M_i to see whether or not M_i |= ~A.
In a finite amount of time we will discover that for some j, M_j |= ~A
by (1). Hence A is not valid.

The other half follows by *completeness*--i.e. we can give a finite
*effective* proof of A. Ok. But BBJ claims that the decidability of L
comes from (2) and (3). How?

I haven't read the other replies carefully - whether they're
correct or not, it's much simpler than that, has nothing to
do with having a bound on the size of the model:

Say (M_j) is an enumeration of all the finite structures, as above.
Say (P_j) is an enumeration of all the proof. Do this:

Check whether M_1 is a model of ~A.
Check whether P_1 is a proof of A.
Check whether M_2 is a model of ~A.
Check whether P_2 is a proof of A.
etc.

Each step returns "yes" or "no" in an effective way.
And (assuming the things you say above) it must
happen that some step returns "yes"; when that
happens you know whether or not A is a theorem.

(If A _is_ a theorem then at some point you
discover that P_j is a proof of A. If A is
not a theorem then at some point you discover
that M_j is a model of ~A.)

************************

David C. Ullrich

Well, that is what I meant by the completeness remark in my original
post. What I was curious about how decidability fell immediately out
of the model-theoretic result. That relies on the upper bound of the
size of the model.

Oh.

It could be that what the authors had in mind is 2 and 3 with
an upper bound on the size of the model.

particularly when they did in fact prove a bound on the size of the models
concerned, as has been pointed out in the thread.

I missed that - didn't appear in the OP or the top-level replies.
Yes, that certainly makes a difference to what one would conjecture
they had in mind.

But I think it's more
likely that when they say the result is immediate from 2 and 3
what they had in mind was the procedure I sketched above.
"Immediate from whatever" doesn't necessarily mean that
you're supposed to forget _everything_ except whatever...

In general, yes, but here there is a model-theoretic argument available
immediately, so introducing proof notions at all is a conceptual
diversion.


************************

David C. Ullrich


************************

David C. Ullrich
.

Relevant Pages

  • Re: Decidability of monadic fragment of FOL
    ... FOL in Boolos, Burgess and Jeffrey (BBJ). ... without identity, say), if A has a model, then it has a finite model. ... Why can't I see the immediate proof? ... an upper bound on the size of the model. ...
    (sci.logic)
  • Re: A Quickie Poll: Whether Help Desk, Bug Track or CRM?
    ... > immediate things come to mind: Doing diffs should work against my ... and only prompt me when a conflict is detected. ...
    (borland.public.delphi.non-technical)
  • Re: Road Traffic Act Offence
    ... > Peter Crosland wrote: ... > I normally find your posts quite informative but you appear to be making ... and so are you the immediate one that come to my mind is the op is a muppet ...
    (uk.legal)
  • Re: 4th stage
    ... designers have in mind with the immediate HC climb, ...
    (rec.bicycles.racing)
  • Re: x^(x^(x^(x^x^...)))....)))) = 2
    ... Sujit wrote: ... One immediate thing comes to mind is: ... I think there is a result due to Euler that the equation ...
    (sci.math)