2
$\begingroup$

I'm working on a software problem and trying to describe it in symbolic logic so that I can get my head around it.

I have

$isnt(n) := \mathbf{F} \neq \emptyset \wedge \forall f \in \mathbf{F} : P(n,f) $

Basically, I'm checking n against all elements in F, unless F is empty.

Is there a way to simplify this so as to have no conjunctions (or disjunctions) outside of the quantifiers

  • 1
    Just today I was wondering whether it would be worthwile having a separate symbol for this.2012-05-11
  • 0
    Well, $\neg(\mathbf{F}=\emptyset\vee\exists f\in\mathbf{F}:\neg P(n,f)).$ But I don't suspect this is what you want. Can you clarify what is allowed?2012-05-11
  • 1
    In the opposite direction, $\exists f\in\mathbf{F}: P(n,f))\wedge\forall f\in\mathbf{F}: P(n,f)).$2012-05-11
  • 0
    I'd like to remove any conjunction or disjunctions outside of the quantifier2012-05-11
  • 0
    @Dancrumb: In that case the quantifier can't be $\forall$, since that's always true on an empty set. It can't be $\exists$ alone, since that can't distinguish between some cases and all cases. Can you use nested quantifiers?2012-05-11
  • 0
    @Charles: yes, nested quantifiers would be acceptable. In short, these quantifiers map onto functions in a programming language: `some` for $\exists$ and `every` for $\forall$... so i can nest these quite easily2012-05-11
  • 0
    @Dancrumb: Of course so does `||` map to $\vee.$2012-05-11
  • 0
    @Dancrumb: Could you please explain _why_ you would prefer nested quantifiers to conjunctions or disjunctions outside of the quantifier?2012-05-11
  • 0
    @Charles: yes... and `&&` maps to $\wedge$2012-05-11
  • 0
    @TaraB: Maybe I won't; I'm looking for an expression that lends itself to a more graceful implementation in code. Rearranging the expression with junctions outside the quantifiers won't change the way the code looks, just the operators that I'm using.2012-05-11
  • 0
    @Dancrumb: So why not `F.length > 0 && every f in F P(n,f)`?2012-05-11
  • 0
    @Dancrumb: Right, well then I don't think that answers to the question as you've phrased it are likely to be very helpful to you. Could you please have a look at my answer and let me know why that's not how you want to do it (if it's not)?2012-05-11

2 Answers 2

3

I don't understand why you're asking for what you seem to be asking for. Surely the efficient way to define the function is something like:

if $F = \emptyset$ then return false;
else for $f\in F$ do
for $f\in F$, if $P(n,f)$ = false then return false;
return true;

  • 0
    That was my thought, and the reason I posted the `||` comment. But perhaps there is some reason.2012-05-11
  • 0
    Yes, I've asked for clarification, and perhaps all will become clear shortly.2012-05-11
  • 0
    In the end, that's what I did; I created a function generator that takes in **F**, *P* and returns a function that takes *n*... appreciate people's efforts though!2012-05-11
  • 0
    Well, it is the natural and efficient way to do it. =]2012-05-11
3

So you can nest quantifiers, but you can't use conjunctions or disjunctions outside the quantifiers. So how about

$$ \exists f\in\mathbf{F}\ \forall g\in\mathbf{F}: P(n,f)\wedge P(n,g) $$

  • 1
    This looks like it could make the program run a lot slower, though.2012-05-11
  • 2
    Why $P(n,f)$? How about just $\exists f \in \textbf{F} \forall g \in \textbf{F} \thinspace \colon \thinspace P(n,g)$?2012-05-11
  • 1
    @TaraB: Yes, substantially. But that seems unavoidable under the constraints, see my comments to the question.2012-05-11
  • 1
    @MartianInvader: Sure, that works too.2012-05-11
  • 1
    @MartianInvader: That's better. =]2012-05-11