Indefinite Consequent First Order Logic

Question

Suppose I want to make the statement:

For every index $i$ in the ordered Array $A$, $A[i]\leq A[i+1]$

Using first order logic I'd write it like:

$\forall i($inRange$(i) \implies A[i]\leq A[i+1]) $

Which intuitively should be true under the interpretation where the universe is $\mathbb{N}$, inRange($i$) is a predicate that states that $0\leq i < size(A)-1$ and $A[i]$ is a function that returns the element in the $i$-th position of A.

However, this would be true iff for every $i$ in $ \mathbb{N}$, the formula:

$ $inRange$(i) \implies A[i]\leq A[i+1] $

is true under the same interpretation. But if we have $j\in \mathbb{N}$, $j> size(A)$, then the formula

$ $inRange$(j) \implies A[j]\leq A[j+1] $

would have an 'indefinite' consequent, since $A[j]$ is not defined. Should I consider it true just because the antecedent is false, or there is some special consideration to be taken?

Answer 1

There're at least 3 ways to deal with your partial function extension problem:

1. formally using free logic (a variant of first order logic whose term can denote nothing).

2. using a total function to represent your partial function.

3. using a higher arity relation symbol to emulate your partial function.

I found this old post described all three approaches in detail already.

Answer 2

For every index $i$ in the ordered Array $A$, $A[i]\leq A[i+1]$

Hint: Somehow define a function $a:N\to A ~~~$ (not sure how you do this in FOL)

$\forall x: [x\in N \implies a(x)\leq a(x+1)]$