Does a particular statement in Lambda calculus count as a proof?

Question

Context: I'm writing a blog post on Lambda calculus for working programmers (like me) that want an insight into some of the truths from planet formal-proofs, but are reluctant to deep dive into all the weird syntax :-)

I have a formal system set up (below) where I'd like to prove(?) 1 + 2 = 3.

Given that, would the following statement be true?

• I have a formal system of symbols that all make up single argument functions.
• The value of a function that has been called is the value obtained by repeatedly applying β-reduction.
• We arbitrarily draw a correspondence between certain functions and integers (Church numerals).
• We arbitrarily decide what it means to increment an integer, and based on that, what it means to do addition on two integers.
• We write out 1 + 2 in the formal system, and it β-reduces to our representation of 3.
• Therefore we have proven 1 + 2 = 3 (within our system).

I'm slightly reluctant to say it, because things like this hint I need to be e.g. using simply typed lambda calculus.

1. Do I need to introduce the idea of booleans (see my blog post), and then a proof is something that evaluates to true?
2. Is there any connection to proofs at all with what I've laid out?
3. Is it simply too fuzzy to be saying things like "we proved 1 + 2 = 3?
4. Is it correct that choosing to represent integers as Church numerals and choosing how to define addition are arbitrary (although obviously handy)? If you say "given this arbitrary way we defined addition, 1 + 2 = 3", is that even saying much of substance?
5. If it is a proof, which bits below correspond to which formal-proof-y words?

// Proving(?) 1 + 2 = 3
// Lambda calculus syntax:     λx.f x
// Corresponds to JavaScript:  x => f(x)

// Church numerals
_0 = f => a => a
_1 = f => a => f(a)
_2 = f => a => f(f(a))
_3 = f => a => f(f(f(a)))
// ...

// Define what it means to increment a integer
// and to add two integers together
inc  = n => f => a => f(n(f)(a))
plus = n => m => n(inc)(m) 

// Substitute and β-reduce
plus(_1)(_2)                                                   // substitute plus, _1, _2
(n => m => n(inc)(m))(f => a => f(a))(f => a => f(f(a)))       // β n
(m => (f => a => f(a))(inc)(m))(f => a => f(f(a)))             // β m
(f => a => f(a))(inc)(f => a => f(f(a)))                       // substitute inc
(f => a => f(a))(n => f => a => f(n(f)(a)))(f => a => f(f(a))) // β first f
(a => (n => f => a => f(n(f)(a)))(a))(f => a => f(f(a)))       // β first a
(n => f => a => f(n(f)(a)))(f => a => f(f(a)))                 // β n
f => a => f((f => a => f(f(a)))(f)(a))                         // β second f
f => a => f((a => f(f(a)))(a))                                 // β second a
f => a => f(f(f(a)))
// This final form is the Church numeral 3
// ∴ 1 + 2 = 3
```