Error in sieve example

[Pietro Braione]

This is a multi-part message in MIME format.
--------------090507010307080605000903
Content-Type: text/plain; charset=us-ascii; format=flowed
Content-Transfer-Encoding: 7bit

Perhaps I found an error in the sieve example.
The "natural language" version contains:

say that the considered natural number is prime, and
consider knowing a natural number not to be a prime as
previously knowing that *and* the considered natural number
*not dividing* this one.

but it should be:

say that the considered natural number is prime, and
consider knowing a natural number not to be a prime as
previously knowing that *or* the considered natural number
*dividing* this one.

Pietro

P.S.
As an extreme exercise of mental masturbation, I've
translated the natural language version, which IMHO
is poorly readable, in, er, multi-epistemic
logic, which is even less readable but perhaps
gives more the idea once grasped. You can find it
in the attachment, hoping for it some use other
than toilet paper (in case, print it on a soft sheet).
Of course I do not guarantee completeness, not even
soundness nor fitness for a particular purpose, so
if your mental state blows out because you tried
to apply the provided axiom system without the
suitable logical omniscience requirement, you're
on your own.
Imagine a scarily comprehensive legal disclaimer.
Double it.
Add two.

--------------090507010307080605000903
Content-Type: text/plain;
 name="sieve_epistemic.txt"
Content-Transfer-Encoding: 7bit
Content-Disposition: inline;
 filename="sieve_epistemic.txt"

%Sieve of Erathostenes in multi-epistemic logic.
%The knowledge at each sieve step is represented by 
%an epistemic modality K{n}, n >= 2. The "null knowledge"
%is represented at step 1, by K{1}. Note that no 
%mental state exists where all the primes are known, 
%but this state it is better refined by increasing values
%of n. Primality of a number is represented by the 
%one-place predicate Pr. Given that we assume S5 
%for epistemic modalities, Pr *is* the predicate 
%of primality for each model since K A -> A (obviously, 
%if everything here works).

1: ForEach p >= 2 . ~K{1}Pr(p) && ~K{1}~Pr(p)
2: ForEach n >= 2 . ForEach A . K{n-1}A -> K{n}A
3: ForEach n >= 2 . ~K{n-1}~Pr(n) -> K{n}Pr(n)
4: ForEach n >= 2 . ForEach p > n . p % n = 0 -> K{n}~Pr(p)
5: ForEach n >= 2 . ForEach p > n . (p % n != 0 && ~K{n-1}Pr(n) && ~K{n-1}~Pr(n)) -> ~K{n}Pr(p) && ~K{n}~Pr(p)

%Comments: Read: ~ as not, -> as if...then, % as remainder, K{n} as
%knows at step n, Pr(p) as p is prime. About the axioms:
% 1: Excludes any a priori hypothesis on primality (and on
%    nonprimality) of numbers.
% 2: Propagates knowledge gained at each step to the next one. 
%    It is a higher order clause, but it could be expanded in two 
%    first order clauses.
% 3: We know that a number n is prime if it has not been sieved 
%    yet at step n.
% 4: If n is prime, all its multiples aren't. Strictly speaking, 
%    it is not necessary for n to be prime to know that its 
%    multiples aren't (if n isn't prime, its multiples have already
%    been sieved before and we already know they arent' prime), so we 
%    omit the K{n}Pr{n} clause in the antecedent of the implication.
% 5: Excludes emergence of unjustified a priori primality 
%    assumptions at steps greater than 1, by propagating ignorance. 
%    In practice it states that if there is no evidence that a 
%    number p is or is not prime at step n (i.e., it isn't a multiple 
%    of n), and at step n-1 we knew nothing about its primality, then 
%    we know nothing about its primality also at step n.

--------------090507010307080605000903--