Re: decidable fragments of first order logic?



On Nov 25, 7:31 pm, Ace0f_5pades <m4de...@xxxxxxxxxxx> wrote:
On Nov 25, 7:02 pm, Ace0f_5pades <m4de...@xxxxxxxxxxx> wrote:





On Nov 25, 4:23 pm, Marshall <marshall.spi...@xxxxxxxxx> wrote:

As I understand it, first order logic in general is not decidable.
However various fragments of FOL are decidable. There's a
decision procedure if all predicates have arity 1, for example.

Are there other fragments of FOL that are decidable?
Are the limits of decidable fragments known? Which
raises the question for me of whether it might be possible
to characterize the "size" of a decidable fragment, and
then ask what the "largest" such fragment might be.

Answers, discussion, and/or pointers to further reading welcome.

Marshall

Yes, there is.

within the context of my last couple of post, there's a statement that
needs such definition. the time factor is a point needing clarity.

How can a state exist in one moment, and another moment -equally in
values -cardinal -ordinal and elemential. for states that satisfy
bijection, injection, and surjection.

On the elemential level, the atomic life along its scale becomes
questionable with each passing moment when time is viewed along the
natural progression time line. questioning the validity of elemential
equality and pairing thereof.

cardinal and ordinal values may still cary the same value, except when
they're paired on the elemential level?

in more complex systems, it becomes even more difficult to plot
changes.

when you introduce time or not time?
if or_not_time then one could simply set a base value of an,an-1 ...
a1,a0 --the digit string for M>0. and that leaves time I=0. the reason
being the total weight of time is an impossible quantity, except as M
and I and R/I.

wouldn't you pair elements with time?- Hide quoted text -

- Show quoted text -

let me put it this way, I'd pair it with time, and I have my
reasons. the instant I do that, a whole bunch of cardinal
contridiction will surface... so, does one create a new function... or
redefine?
.