The old Google Groups will be going away soon, but your browser is incompatible with the new version.
Message from discussion Quantifier free sets

From:
To:
Cc:
Followup To:
Subject:
 Validation: For verification purposes please type the characters you see in the picture below or the numbers you hear by clicking the accessibility icon.

More options Oct 14 2012, 10:08 pm
Newsgroups: sci.logic
From: Graham Cooper <grahamcoop...@gmail.com>
Date: Sun, 14 Oct 2012 19:08:25 -0700 (PDT)
Local: Sun, Oct 14 2012 10:08 pm
Subject: Re: Quantifier free sets
On Oct 14, 5:17 pm, Zuhair <zaljo...@gmail.com> wrote:

> In quantifier free FOL, you don't have any symbol representing
> universal quantification or existential quantification. However there
> is "Quantification" of course, and this can be seen by noticing that
> the variables are "ranging" over a domain! and this is a form of
> subtle quantification by itself, and it is universal in a sense. But
> still there is no explicit quantifier symbol to represent this subtle
> kind of universal quantification, so for example you cannot use
> negation in a manner as to derive existential quantification, the
> absence of symbols for quantification (i.e. quantifiers) does affect
> the machinery of the language, it WEAKENS it further, for instance, as
> you mentioned, you cannot speak of existential quantification, unless
> perhaps by some very twisted ways in some particular instances like by
> using constants or functions, or (Skolem_Herbrand)ization, etc....

> I hope that helps

> Zuhair

Right pure PROLOG is weaker than quantified logic as a VAR is used to
find a value that EXISTS over ALL possible solutions.

SUBSET is impossible in pure PROLOG, but simply by adding
NOT(predicate(..))

then full FOL quantification is possible.

------------------------------------

> You have to use  BAGOF  and  LIST RECURSION (for SUBSET)

[JAN]

Or negation as failure:
FOL:
forall x(male(x) <-> rower(x)

Prolog
?- \+ (male(X), \+ rower(X)), \+ (rower(Y), \+ male(Y)).

Some Prolog systems (*) even provide a shortcut:
forall(X,Y) :- \+ (X, \+ Y).
?- forall(male(X),rower(X)), forall(rower(Y), male(Y)).

Cheers!
Herc