Talk:Infimum

Problem with second part of definition

Strangely I considered this problem solved as I deleted this talk page afterwards....
An infimum or greatest lower bound (AKA: g.l.b) of a subset $A\subseteq X$ of a poset $(X,\preceq)$, which we denote: $\text{inf}(A)$ is a value {{M|\in X} such that:

1. $\forall a\in A[\text{inf}(A)\le a]$ (that $\text{inf}(A)$ is a lower bound)
2. $\forall x\in\underbrace{\{y\in X\ \vert\ \forall a\in A[y\le a]\} }_{\text{The set of all lower bounds} }\ \ [\text{inf}(A)\ge x]$ (that $\text{inf}(A)$ is an upper bound of all lower bounds of $A$)

However I have always thought of (rather than condition (2) above):

• condition 1 and $\forall x\in X\exists a\in A[x>\text{inf}(A)\implies a<x]$

I believe this is equivalent, that is:

• $\forall x\in X\exists a\in A[x>\text{inf}(A)\implies a<x]\iff\forall x\in\underbrace{\{y\in X\ \vert\ \forall a\in A[y\le a]\} }_{\text{The set of all lower bounds} }\ \ [\text{inf}(A)\ge x]$

First note:

• $\forall x\in\underbrace{\{y\in X\ \vert\ \forall a\in A[y\le a]\} }_{\text{The set of all lower bounds} }\ \ [\text{inf}(A)\ge x]\iff\forall x\in X\left[\left(\forall a\in A[x\le a]\right)\implies x\le\text{inf}(A)\right]$

Then note that for the statement:

• $\Big[(\forall a\in A[x\le a])\implies x\le\text{inf}(A)\Big]\iff\Big[x>\text{inf}(A)\implies(\exists a\in A[x>a])\Big]$ (by contrapositive), so condition two is simply:
  • $\forall x\in X[x>\text{inf}(A)\implies(\exists a\in A[x>a])]$, this is a stone's throw away from $\forall x\in X\exists a\in A[x>\text{inf}(A)\implies a<x]$.

Claim:

$\Big(\forall x\in X[x>\text{inf}(A)\implies(\exists a\in A[x>a])]\Big)\iff\Big(\forall x\in X\exists a\in A[x>\text{inf}(A)\implies a<x]\Big)$. Warning:(Workings below show this to be false)

LHS $\implies$ RHS:

• Let $x\in X$ be given.
  • If $x\le\text{inf}(A)$ then pick any $a\in A$, as the LHS of the implication is false, we don't care about the right. Warning:This CLEARLY requires that $A\ne\emptyset$, which the LHS of the claim does not!
  • If $x>\text{inf}(A)$ then by hypothesis it is true that "$\exists a\in A[x>a]$" - pick that $a\in A$ and the result follows.

RHS $\implies$ LHS:

• Let $x\in X$ be given.
  • If $x\le\text{inf}(A)$ we do not care about the truth or falseness of $\exists a\in A[x>a]$ - so there may or may not $\exists a\in A$ (at all!) let alone one $<x$ This confirms the above warning
  • If $x>\text{inf}(A)$ then by hypothesis $\exists a<x$ and we're done.

Correct claim:

$\Big(\forall x\in X\exists a\in A[x>\text{inf}(A)\implies a<x]\Big)\implies\Big(\forall x\in X[x>\text{inf}(A)\implies(\exists a\in A[x>a])]\Big)$ or

If $A\ne\emptyset$: $\Big(\forall x\in X\exists a\in A[x>\text{inf}(A)\implies a<x]\Big)\implies\Big(\forall x\in X[x>\text{inf}(A)\implies(\exists a\in A[x>a])]\Big)$

• Which may be said as: $\exists \varphi\in A\Big[\Big(\forall x\in X\exists a\in A[x>\text{inf}(A)\implies a<x]\Big)\iff\Big(\forall x\in X[x>\text{inf}(A)\implies(\exists a\in A[x>a])]\Big)\Big]$

This is an interesting exercise in first-order-logic and shows the importance of being careful!