Absorbing bounded quantifiers, formal proof?

Question

Intuitively I get in arithmetic aka the natural numbers that:

$\exists n\,\exists m\,(m < n \wedge P(m)) \Leftrightarrow \exists k\,P(k)$

But I am having problems finding a formal proof.

What I tried so far, is using $P(j) \Leftrightarrow \neg Q(j)$, and then this is the same as $\forall n\,\forall m (m < n \Rightarrow Q(m)) \Leftrightarrow \forall k\,Q(k)$. The $\Leftarrow$ direction looks like specialization, weakening and generalization. The $\Rightarrow$ direction could work with changing the quantifier order and then using a specialization.

Answer 1

A proof which I just verified in Agda so is pretty much as formal as they come:

The forward direction is trivial: take $k = m$.

The backward direction: take $m = k$ and $n = k+1$.

That's really all there is to it.

Preamble to set up the appropriate definitions of equality, $+$, $<$ and so on:

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)

infix 5 _≡_
data _≡_ {a} {A : Set a} (x : A) : A → Set a where
    refl : x ≡ x

data Sg {n : _} {m : _} (A : Set m) (B : A → Set n) : Set (m ⊔ n) where
  _,_ : (a : A) → (b : B a) → Sg A B

infix 15 _&&_
record _&&_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  constructor _,,_
  field
    fst : A
    snd : B

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

infix 15 _+N_
infix 100 succ
_+N_ : ℕ → ℕ → ℕ
zero +N y = y
succ x +N y = succ (x +N y)

infix 5 _<N_
record _<N_ (a : ℕ) (b : ℕ) : Set where
    constructor le
    field
      x : ℕ
      proof : (succ x) +N a ≡ b

The actual proof:

lemm : (P : ℕ → Set) → Sg ℕ (λ i → Sg ℕ (λ j → (j <N i) && P j)) → Sg ℕ (λ k → P k)
lemm P (n , (m , (fst ,, snd))) = m , snd

lemm' : (P : ℕ → Set) → Sg ℕ (λ k → P k) → Sg ℕ (λ i → Sg ℕ (λ j → (j <N i) && P j))
lemm' P (k , b) = (succ k , (k , record { fst = le zero refl ; snd = b }))

Answer 2

Ok, I tried a translation, of the Agda proof, to natural deduction. From arithmetic I only assume k < k+1, there are different ways to define "<", I didn't replicate the arithmetic part:

Here is a natural deduction proof.

<= Direction:

                       ----------         ------------
                       |- k < k+1         P(k) |- P(k)       
                       -------------------------------
                           P(k) |- k < k+1 /\ P(k)
                         ---------------------------
                         P(k) |- ∃m(m < k+1 /\ P(m))
  ------------------     -----------------------------
  ∃k P(k) |- ∃k P(k)     P(k) |- ∃n ∃m(m < n /\ P(m))
  ----------------------------------------------------
           ∃k P(k) |- ∃n ∃m(m < n /\ P(m))

=> Direction:

                                        ------------------------------
                                        m < n /\ P(m) |- m < n /\ P(m)
                                        ------------------------------
                                              m < n /\ P(m) |- P(m)
 -------------------------------------------  -------------------------
 ∃n∃m(m < n /\ P(m)) |- ∃n∃m(m < n /\ P(m))  m < n /\ P(m) |- ∃k P(k) 
 ----------------------------------------------------------------------
                      ∃n∃m(m < n /\ P(m)) |- ∃k P(k)