Easy model finder for FOL

Nice to know
1

This is a famous logic puzzle: There is a barber who shaves a person if and only if he does not shave himself. Then does the barber shaves himself?

I “solved” this puzzle by enumerating models using my private ZDD library.

First, enumerate all models for a barber who shaves
a person if and only if he does not shave himself with a fixed small domain D={a, b, c}, too small. The experiment returns 512 as the number of such models.

Next, I count the number M of the given model, i.e., in which the barber shaves himself. It returns M = 0 (no model found) as we all might expected.

The idea behind this model finder is simple. As the domain is small enough, FOL formula is expanded a quantifier-free ground formula (i.e. a proposition). Then convert it a DNF (disjunctive normal form like ab + cd*e + … ), the point is here that the required number is calculated from the DNF easily. I think everything is clear, aside my presentation. ZDD contribution here is only its capacity to keep a big DNF and efficient form for counting models from the DNF.

I believe this is one of the most naive model finders. There may be many smart ones, but unfortunately they might be too advanced and difficult for me to catch up.

% ?- time((dnf_model([a,b,c], (all(x, barbar(x) =:= all(y, -shave(y,y) =:= shave(x, y)))), Z, S), ltr_card(Z, C, S), get_key(atomnum, Count, S))).
%@ [-barbar(a),-shave(c,c),-shave(a,c),-barbar(b),-shave(b,c),-barbar(c)]
%@ [-barbar(a),shave(c,c),shave(a,c),-barbar(b),shave(b,c),-barbar(c)]
%@ [-barbar(a),-shave(b,b),-shave(c,c),-shave(a,c),-barbar(b),-barbar(c)]

<snip>


% ?- time((dnf_model([a,b,c], (all(x, barbar(x) =:= all(y, -shave(y,y) =:= shave(x, y))), some(z, (shave(z, z), barbar(z)))), Z, S), ltr_card(Z, C, S), get_key(atomnum, Count, S))).
%@ atomnum(12)
%@ % 114,915 inferences, 0.008 CPU in 0.008 seconds (98% CPU, 14958995 Lips)
%@ Z = C, C = 0,
%@ S = ..,
%@ Count = 12.
3

No. Function symbols are not handled.

I tested others with domain {a,b,c}. C is the number of model.

% ?- dnf_model([a,b,c], (a; -a)).
%@ [-a]
%@ [a]
%@ true.

% ?- dnf_model([a,b,c], a-> -a, Z, S), ltr_card(Z, C, S).
%@ [-a]
%@ Z = 2,
%@ S = ..,
%@ C = 1.

% ?-  F = all(x, some(y, p(y)->p(x))),
%	dnf_model([a,b,c], F, Z, S), ltr_card(Z, C, S).
%@ [-p(c)]
%@ [-p(b)]
%@ [p(b),-p(c)]
%@ [-p(a)]
%@ [p(a),-p(c)]
%@ [p(a),-p(b)]
%@ [p(a),p(b),-p(c)]
%@ [p(a),p(b),p(c)]
%@ F = all(x, some(y,  (p(y)->p(x)))),
%@ Z = 60,
%@ S = ..,
%@ C = 8.

% ?-  F = some(x, all(y, p(y)->p(x))),
%	dnf_model([a,b,c], F, Z, S), ltr_card(Z, C, S).
%@ [p(c)]
%@ [-p(b),p(c)]
%@ [p(b)]
%@ [-p(a),p(c)]
%@ [-p(a),-p(b),-p(c)]
%@ [-p(a),-p(b),p(c)]
%@ [-p(a),p(b)]
%@ [p(a)]
%@ F = some(x, all(y,  (p(y)->p(x)))),
%@ Z = 43,
%@ S = ..,
%@ C = 8.
4

By coincidence, I’ve been writing notes for myself on FOL which touched on the barber puzzle. (A learning exercise in classical logic and some web technologies).

https://www.seatavern.co.za/classical-logic/negation/#the-barber-puzzle

My view is the statement doesn’t prevent the barber from shaving himself as I’ve tried to explain with a Venn diagram. Also, why can’t the barber be a she?

5

I have checked barber sentence:
Barber paradox - Wikipedia
“one who shaves all those, and those only, who do not shave themselves”.

and checked. My easy model finder answered “There is no barber in the village with three people.” I hope it is correct answer.

% ?- BarberSentence = 
%	(all(x, barber(x) =:=  all(y,  -shave(y, y) =:= shave(x, y)))),
%	dnf_model([a,b,c], ( BarberSentence, some(x,  (barber(x), shave(x, x)))), Z, S),  ltr_card(Z, C, S).
%@ Z = C, C = 0,
1 Like
7

I should be careful for that. Also one should be careful for number of propositional variables. It is necessary n+nn propositional variables for barber/1, shave/2, where n is the size of village, which means 2^(n+nn) possible model ! I don’t know feasible n for this kind of easy finders. For exampe, 4096 for the barber case n=3, but N = 1298074214633706907132624082305024 possible models for n = 10, which I never should try.

9

In fact, I did it with leanTAP.

As the Barber example seems not interesting as I expected, I take another example from “Everybody loves somebody.” My easy model finder shows that two readings on quantifier scope of the sentence are not equivalent with two counter examples using a domain {a, b}.

% ?- dnf_model([a,b], - (all(x, some(y, love(x, y))) =:= some(y, all(x, love(x, y)))), Z, S), ltr_card(Z, C, S).
%@ [-love(a,a),love(a,b),love(b,a),-love(b,b)]
%@ [love(a,a),-love(a,b),-love(b,a),love(b,b)]
%@ Z = 42,
%@ S = ..,
%@ C = 2.