How to present the properties of a piecewise function in first order logic

logicnotation

I am unsure on how to present the properties ofa piecewise function in first order logic with equality (FOL=).

As an example I will use the function that computes the $nth$ number in the Fibonacci sequence.

\begin{align*}
\forall n \colon \mathbb{N} \colon \mathsf{fib}(n) = \begin{cases}
0 & \text{if $n=0$}, \\
1 & \text{if $n=1$}, \\
\mathsf{fib}(n-2)+\mathsf{fib}(n-1) & \text{if $n>1$}. \\
\end{cases}
\end{align*}
I ignore the fact that subtraction is a partial function in $\mathbb{N}$.

Attempt 1

My first attempt is to write each case as a implication and then write the entire function as a conjunction of cases. When the antecedent is false then the case is true. Given the domain is $\mathbb{N}$ I think all cases are covered.

\begin{align*}
(\forall n \colon \mathbb{N} \colon ((n=0) \implies (\mathsf{fib}(n) = 0))) \land \\
(\forall n \colon \mathbb{N} \colon ((n=1) \implies (\mathsf{fib}(n) = 1))) \land \\
(\forall n \colon \mathbb{N} \colon (\neg((n=1) \lor (n=0)) \implies (\mathsf{fib}(n) = \mathsf{fib}(n – 1)+\mathsf{fib}(n – 2))))
\end{align*}

Attempt 2

My second attempt uses the disjunction of 3 equations, the first two equations are for constants 0 and 1:
\begin{align*}
(\mathsf{fib}(0) = 1) \lor \\
(\mathsf{fib}(1) = 1) \lor \\
\forall n \colon \mathbb{N} \colon((n>1) \implies (\mathsf{fib}(n + 2) =\mathsf{fib}(n) + \mathsf{fib}(n+1)). \\
\end{align*}

Are either of these valid approaches to presenting the properties of the function in FOL=?

What would be an appropriate approach?

Maybe I need to rewrite the equalities as relations?

Best Answer

If you just want to express the property of the function $\mathsf{fib}$, the following may be ok.

$$ \forall n\,[(n=0\to\mathsf{fib}(n)=0)\vee (n=1\to\mathsf{fib}(n)=1)\vee(n>1\to \mathsf{fib}(n)=\mathsf{fib}(n-1)+\mathsf{fib}(n-2))]. $$

Note that the premises is that the signature of the first order language is $\{+,-,\mathsf{fib},0,1,2\}$ and $n$ is a variable of the first order language.

But I don't know what's the meaning of your "represent"!!!

Related Solutions

Translating from First Order Logic to Order-Sorted Logic

I don't know about the OSA system specifically. However, here's a proof that I wrote up in Coq using types. Most of the length of this is just the setup, then the actual proof becomes very short.

Parameters Horse Dog Greyhound Rabbit Animal : Type.
Parameter Horse_inc_Animal : Horse -> Animal.
Parameter Dog_inc_Animal : Dog -> Animal.
Parameter Greyhound_inc_Dog : Greyhound -> Dog.  (* 3a *)
Parameter Rabbit_inc_Animal : Rabbit -> Animal.

Coercion Horse_inc_Animal : Horse >-> Animal.
Coercion Dog_inc_Animal : Dog >-> Animal.
Coercion Greyhound_inc_Dog : Greyhound >-> Dog.
Coercion Rabbit_inc_Animal : Rabbit >-> Animal.

Parameter Faster : Animal -> Animal -> Prop.

Axiom stmt_1a : forall (x : Horse) (y : Dog),
  Faster x y.
Axiom stmt_2a : exists y : Greyhound,
  forall z : Rabbit, Faster y z.
Axiom stmt_4a : forall x y z : Animal,
  Faster x y -> Faster y z -> Faster x z.

Parameter Harry : Horse. (* 5a *)
Parameter Ralph : Rabbit. (* 6a *)

(* Main result... *)
Goal Faster Harry Ralph.
Proof.

(* existential elimination on (2a) *)
destruct stmt_2a as [g].

(* specialization of (4a), and also implicitly applies ->E (modus ponens)
   a couple of times *)
apply stmt_4a with (y := g).

(* Subgoal: Faster Harry g,
   proved by specializing (1a) *)
+ apply stmt_1a.

(* Subgoal: Faster g Ralph,
   proved by specializing the statement
   H : forall z : Rabbit, faster g z
   gotten from the existential elimination *)
+ apply H.
Qed.

Again, I don't know how much this would help in constructing a proof in your particular system - I'm just posting in the hopes that it might be close enough to be of some help. (Do keep in mind that Coq is often oriented towards top-down programming of a proof, as in this case, whereas Fitch-style systems are often closer to bottom-up serializations of the same proof term.)

Determine the validity of statements in First Order Logic. Is there a general method

The torturous chain of comments has reached a point where an attempt at an Answer seems appropriate.

Note again that the incompleteness theorem, in the guise of the unsolvability of the "decision problem", shows that it's impossible to give a perfect answer, in the form "To decide whether $\phi$ is valid do the following", where "the following" can be done in a mechanical way regardless of $\phi$ and always returns the right answer. But the OP has asked what I actually do to figure these things out, and I can attempt to answer that.

First recall that by definition $\phi$ is valid if it's true in any interpretation. (Newbies should note that there is a precise formal definition of "interpretation". For our purposes we can leave the notion informally "defined" by example; e.g. if I say "Let $x$ range over the integers, let $P(x)$ be $x=x$ and let $Q(x) $ be $x>x$" I have specified an "interpretation" for the language used in (7).)

So what do I do to try to decide whether $\phi$ is valid?

Note I do not start by looking for an interpretation where $\phi$ is true!

Because if I find an interpretation where $\phi$ is true that says nothing about whether $\phi$ is valid - there may or may not be some other interpretation where $\phi$ is false. (This is why your proofs that various things are valid are wrong; in each case you just give one interpretation where the formula is true, which proves nothing.)

What I do do is this:

Heuristic: To try to determine whether $\phi$ is valid: If the answer's not obvious, look for an interpretation where $\phi$ is false.

I succeed or not.

(i) If I do find an interpretation where $\phi$ is false, I'm done: $\phi$ is not valid.

(ii) If I cannot find an interpretation where $\phi$ is false, I ask myself why not. When I get lucky, looking for what goes wrong when I try to "falsify" $\phi$ allows me to prove that it's impossible to give an interpretation where $\phi$ is false; when that happens I've proved that $\phi$ is valid.

Three examples:

Formula (1): This seems "obvious" to me. Yes, it's valid, but your explanation "Because LHS will always be false." is wrong. LHS is false in the one interpretation you're considering, but to use that sentence to explain why $\phi$ is valid you'd have to show that LHS is false in every interpretation, which of course is not so.

But (1) is obviously valid: If $P(x)$ is true for every $x$ (that is, for every $x$ in the domain of some interpretation) then $P(x)$ is true for $x=c$.

Formula (7): I look for an interpretation where (7) is false. Looking at truth tables, this means I need an interpretation where $\exists x(P(x)\lor Q(x))$ is true, $\forall xP(x)$ is true and $\exists xQ(x)$ is false. An obvious way to make $\forall xP(x)$ true and $\exists xQ(x)$ false is to say $P(x)$ is $x=x$ and $Q(x)$ is $x>x$; I get lucky that with that interpretation $\exists x(P(x)\lor Q(x))$ is true, and I'm done: I have an interpretation where (7) is false, so (7) is not valid.

Formula (3): This seems to me like the most interesting example, because it looks wrong at first: How can $P(x)$ imply $\forall xP(x)$? But in fact this explains why $\exists x P(x)\implies\forall xP(x)$ is not valid, and that's not the same as (3). In fact it turns out that (3) is valid:

First I say to myself that using the same letter in both (nested) quantifiers may lead to confusion over what "$x$" means in an informal discussion. Since $\forall xP(x)$ is equivalent to $\forall yP(y)$ (technicality: and neither contains a free variable), (3) is equivalent to

3': $\exists x(P(x)\implies \forall yP(y))$.

Can we find an interpretation where (3') is false? Hmm. The negation of (3') is

$\lnot$3': $\forall x(P(x)\land \exists y(\lnot P(y)))$.

Since $\forall x$ does distribute over $\land$ and there is no $x$ free in $\forall yP(y)$, this is equivalent to

$(\lnot 3')'$: $\forall xP(x)\land \exists y(\lnot P(y))$

And $(\lnot 3')'$ is obviously false in every interpretation: If we can find $y$ such that $\lnot P(y)$ is true then $\forall xP(x)$ is false, since $x=y$ gives a counterexample.

Digression: That last bit shows why I changed one of the $x$'s to $y$ at the start: If I hadn't done that then expressing what I mean by "$x=y$ is a counterexample" would have been trickier.

So $\lnot$(3) is false in every interpretation, so (3) is true in every interpretation: (3) is valid.

Edit: I wrote all that out to illustrate the utility of the heuristic above. Of course one can give a simpler and probably more intuitive explanation of why (3') is valid:

In a given interpretation $\forall yP(y)$ is true or false. If it's true then $P(x)\implies \forall yP(y)$ is true regardless of $x$.

Suppose otoh that $\forall yP(y)$ is false in our interpretation. Choose $y$ so that $P(y)$ is false; then if $x=y$, $P(x)$ is false, so $P(x)\implies\forall yP(y)$ is again true. Since it's true for some $x$ in the interpretation it follows that $\exists x(P(x)\implies\forall yP(y))$ is true.

Best Answer

Related Solutions

Translating from First Order Logic to Order-Sorted Logic

Determine the validity of statements in First Order Logic. Is there a general method

Related Question