Or, as I like to say,
(∀c₀∀c₁∀c₂∀c₃∀c₅)((∀e)(¬(e∈c₀))∧(∀e)(e∈c₁↔e∈c₀∨e=c₀)∧(∀e)(e∈c₂↔e∈c₁∨e=c₁)∧(∀e)(e∈c₃↔e∈c₂∨e=c₂)∧(∀e)(e∈c₄↔e∈c₃∨e=c₃)∧(∀e)(e∈c₅↔e∈c₄∨e=c₄))(∀N)((∀n)(n∈N↔(∀I)(c₀∈I∧(∀k)(k∈I→(∃z)((∀m)(m∈z↔m∈k∨m=k)∧z∈I))→n∈I)))→(∀f)((∀a,b)((∀t)((∀e)(e∈t↔(∀s)(s∈e↔s=b)∨(∀s)(s∈e↔s=a∨s=b))∧t∈f→(∃a₁,a₂)(a₁∈N∧a₂∈N∧(∀e)(e∈a↔(∀s)(s∈e↔s=a₂)∨(∀s)(s∈e↔s=a₁∨s=a₂)))∧b∈N))∧(∀n)(n∈N→(∀r)((∀t)((∀e₁)(e₁∈t↔(∀s₁)(s₁∈e₁↔s₁=r)∨(∀s₁)(s₁∈e₁↔s₁=r∨(∀e)(e∈s₁↔(∀s)(s∈e↔s=c₀)∨(∀s)(s∈e↔s=n∨s=c₀))))∧t∈f→r=n)))∧(∀n,k)(n,k∈N→(∀r)((∀t)((∀e₁)(e₁∈t↔(∀s₁)(s₁∈e₁↔s₁=r)∨(∀s₁)(s₁∈e₁↔s₁=r∨(∀e)(e∈s₁↔(∀s)(s∈e↔(∀m)(m∈s↔m∈k∨m=k))∨(∀s)(s∈e↔s=n∨(∀m)(m∈s↔m∈k∨m=k)))))∧t∈f→(∀r₁)((∀t₁)((∀e₁)(e₁∈t₁↔(∀s₁)(s₁∈e₁↔s₁=r₁)∨(∀s₁)(s₁∈e₁↔s₁=r₁∨(∀e)(e∈s₁↔(∀s)(s∈e↔s=k)∨(∀s)(s∈e↔s=n∨s=k))))∧t₁∈f→(∀m)(m∈r↔m∈r₁∨m=r₁)))))))→(∀r)((∃t)((∀e₁)(e₁∈t↔(∀s₁)(s₁∈e₁↔s₁=r)∨(∀s₁)(s₁∈e₁↔s₁=r∨(∀e)(e∈s₁↔(∀s)(s∈e↔s=c₃)∨(∀s)(s∈e↔s=c₂∨s=c₃))))∧t∈f)→r=c₅)
(That's not just random symbols; that's an actual first-order expression of "2 + 3 = 5", assuming I didn't make any mistakes)
Start with
2+3 = 5
Then characterize addition as a function f abiding by (1) dom(f) = ℕ×ℕ; (2) ran(f) = ℕ; (3) for every n∈ℕ have f(n, 0) = n; (4) for every n,k∈ℕ have f(n, S(k)) = S(f(n, k))
Since there exists exactly one such function, we can replace 2+3 = 5 with (∀f)( f meets the characterization → f(2, 3) = 5 )
This gives:
(∀f)
(
dom(f) = ℕ×ℕ
∧ ran(f) = ℕ
∧ (∀n)( n∈ℕ → f(n, 0) = n )
∧ (∀n, k)( n,k∈ℕ → f(n, S(k)) = S(f(n, k)) )
) → f(2, 3) = 5
Now replace:
- dom(f) = X ∧ ran(f) = Y with (∀a,b)( [a, b] ∈ f → a∈X ∧ b∈Y )
- F(A) = R with (∀r)( (A, r) ∈ F → r = R )
(note that by [a, b] I mean the two-tuple of a and b)
(∀f)
(
(∀a, b)( [a, b] ∈ f → a∈ℕ×ℕ ∧ b∈ℕ )
∧ (∀n)( n∈ℕ → (∀r)( [[n, 0], r] ∈ f → r = n ) )
∧ (∀n, k)( n,k∈ℕ → (∀r)( [[n, S(k)], r] ∈ f → r = S(f(n, k)) ) )
) → (∀r)( [[2, 3], r] ∈ f → r = 5 )
Looking good!
Now we're gonna "factor out" ℕ like we did to f. We characterize it as the set N abiding by: for all n, n is in N if and only if n is in every inductive set.
(∀N)
(
(∀n)( n∈N ↔ (∀I)( I is inductive → n∈I ) )
) →
(∀f)
(
(∀a, b)( [a, b] ∈ f → a∈N×N ∧ b∈N )
∧ (∀n)( n∈N → (∀r)( [[n, 0], r] ∈ f → r = n ) )
∧ (∀n, k)( n,k∈N → (∀r)( [[n, S(k)], r] ∈ f → r = S(f(n, k)) ) )
) →
(∀r)( [[2, 3], r] ∈ f → r = 5 )
ok, now let's:
- include the definition of inductive. A set is inductive if it contains the empty set and if whenever n is in the set, so is S(n).
- remove the expression f(n, k) by characterizing it as the unique value r such that [[n, k], r] ∈ f
- replace a∈N×N with (∃a₁,a₂)( a₁∈N ∧ a₂∈N ∧ a=[a₁, a₂] )
(∀N)
(
(∀n)( n∈N ↔ (∀I)( ∅∈I ∧ (∀k)(k∈I → S(k)∈I) → n∈I ) )
) →
(∀f)
(
(∀a, b)( [a, b] ∈ f → (∃a₁,a₂)( a₁∈N ∧ a₂∈N ∧ a=[a₁, a₂] ) ∧ b∈N )
∧ (∀n)( n∈N → (∀r)( [[n, 0], r] ∈ f → r = n ) )
∧ (∀n, k)( n,k∈N → (∀r)( [[n, S(k)], r] ∈ f → (∀r₁)( [[n, k], r₁]∈f → r = S(r₁) ) ) )
) →
(∀r)( [[2, 3], r] ∈ f → r = 5 )
Great! Now let's deal with those pesky tuples.
Each expression [x,y] needs to be factored out as a new variable t, which between you and me is exactly the set {{y},{x,y}}, but needs to be characterized as:
(∀e)(e∈t ↔ (∀s)(s∈e ↔ s=y) ∨ (∀s)(s∈e ↔ s=x ∨ s=y)
While I'd love to push that mess to the very beginning of the formula (like I did with f and N), this time I can't since I'll be using some deeply-nested variables.
it's gonna get messy!
(Usually pairs are encoded as [x,y]={{x},{x,y}} but for us it will be more convenient to use [x,y]={{y},{x,y}} so that dealing with nested tuples like [[a,b],c] is less messy)
(I'm also gonna rewrite a=[a₁, a₂] while I'm at it)
(∀N)
(
(∀n)( n∈N ↔ (∀I)( ∅∈I ∧ (∀k)(k∈I → S(k)∈I) → n∈I ) )
) →
(∀f)
(
(∀a, b)( (∀t)( (∀e)(e∈t ↔ (∀s)(s∈e ↔ s=b) ∨ (∀s)(s∈e ↔ s=a ∨ s=b)) ∧ t∈f → (∃a₁,a₂)( a₁∈N ∧ a₂∈N ∧ (∀e)(e∈a ↔ (∀s)(s∈e ↔ s=a₂) ∨ (∀s)(s∈e ↔ s=a₁ ∨ s=a₂)) ) ∧ b∈N ) )
∧ (∀n)( n∈N → (∀r)( (∀t)( (∀e₁)(e₁∈t ↔ (∀s₁)(s₁∈e₁ ↔ s₁=r) ∨ (∀s₁)(s₁∈e₁ ↔ s₁=r ∨ (∀e)(e∈s₁ ↔ (∀s)(s∈e ↔ s=0) ∨ (∀s)(s∈e ↔ s=n ∨ s=0)))) ∧ t∈f → r = n ) ) )
∧ (∀n, k)( n,k∈N → (∀r)( (∀t)( (∀e₁)(e₁∈t ↔ (∀s₁)(s₁∈e₁ ↔ s₁=r) ∨ (∀s₁)(s₁∈e₁ ↔ s₁=r ∨ (∀e)(e∈s₁ ↔ (∀s)(s∈e ↔ s=S(k)) ∨ (∀s)(s∈e ↔ s=n ∨ s=S(k))))) ∧ t∈f → (∀r₁)( (∀t₁)( (∀e₁)(e₁∈t₁ ↔ (∀s₁)(s₁∈e₁ ↔ s₁=r₁) ∨ (∀s₁)(s₁∈e₁ ↔ s₁=r₁ ∨ (∀e)(e∈s₁ ↔ (∀s)(s∈e ↔ s=k) ∨ (∀s)(s∈e ↔ s=n ∨ s=k)))) ∧ t₁∈f → r = S(r₁) ) ) ) ) )
) →
(∀r)( (∃t)( (∀e₁)(e₁∈t ↔ (∀s₁)(s₁∈e₁ ↔ s₁=r) ∨ (∀s₁)(s₁∈e₁ ↔ s₁=r ∨ (∀e)(e∈s₁ ↔ (∀s)(s∈e ↔ s=3) ∨ (∀s)(s∈e ↔ s=2 ∨ s=3)))) ∧ t∈f ) → r = 5 )
nice. Just look at how long that scroll bar is.
The non-first-order-logic symbols we have left to remove are:
- ∅
- 0
- S
- 2
- 3
- 5
We'll handle the empty set and the numbers by factoring them out into variables c₀, c₂, c₃, c₅
And we'll handle S by replacing x=S(n) with (∀m)(m∈x ↔ m∈n ∨ m=n)
I'd just like to note that factoring out c₀ will be the FIRST time we introduce a negation. cool!
(∀c₀, c₁, c₂, c₃, c₅)
(
(∀e)(¬(e∈c₀))
∧ (∀e)(e∈c₁ ↔ e∈c₀ ∨ e=c₀)
∧ (∀e)(e∈c₂ ↔ e∈c₁ ∨ e=c₁)
∧ (∀e)(e∈c₃ ↔ e∈c₂ ∨ e=c₂)
∧ (∀e)(e∈c₄ ↔ e∈c₃ ∨ e=c₃)
∧ (∀e)(e∈c₅ ↔ e∈c₄ ∨ e=c₄)
)
(∀N)
(
(∀n)( n∈N ↔ (∀I)( c₀∈I ∧ (∀k)(k∈I → S(k)∈I) → n∈I ) )
) →
(∀f)
(
(∀a, b)( (∀t)( (∀e)(e∈t ↔ (∀s)(s∈e ↔ s=b) ∨ (∀s)(s∈e ↔ s=a ∨ s=b)) ∧ t∈f → (∃a₁,a₂)( a₁∈N ∧ a₂∈N ∧ (∀e)(e∈a ↔ (∀s)(s∈e ↔ s=a₂) ∨ (∀s)(s∈e ↔ s=a₁ ∨ s=a₂)) ) ∧ b∈N ) )
∧ (∀n)( n∈N → (∀r)( (∀t)( (∀e₁)(e₁∈t ↔ (∀s₁)(s₁∈e₁ ↔ s₁=r) ∨ (∀s₁)(s₁∈e₁ ↔ s₁=r ∨ (∀e)(e∈s₁ ↔ (∀s)(s∈e ↔ s=c₀) ∨ (∀s)(s∈e ↔ s=n ∨ s=c₀)))) ∧ t∈f → r = n ) ) )
∧ (∀n, k)( n,k∈N → (∀r)( (∀t)( (∀e₁)(e₁∈t ↔ (∀s₁)(s₁∈e₁ ↔ s₁=r) ∨ (∀s₁)(s₁∈e₁ ↔ s₁=r ∨ (∀e)(e∈s₁ ↔ (∀s)(s∈e ↔ (∀m)(m∈s ↔ m∈k ∨ m=k)) ∨ (∀s)(s∈e ↔ s=n ∨ (∀m)(m∈s ↔ m∈k ∨ m=k))))) ∧ t∈f → (∀r₁)( (∀t₁)( (∀e₁)(e₁∈t₁ ↔ (∀s₁)(s₁∈e₁ ↔ s₁=r₁) ∨ (∀s₁)(s₁∈e₁ ↔ s₁=r₁ ∨ (∀e)(e∈s₁ ↔ (∀s)(s∈e ↔ s=k) ∨ (∀s)(s∈e ↔ s=n ∨ s=k)))) ∧ t₁∈f → (∀m)(m∈r ↔ m∈r₁ ∨ m=r₁) ) ) ) ) )
) →
(∀r)( (∃t)( (∀e₁)(e₁∈t ↔ (∀s₁)(s₁∈e₁ ↔ s₁=r) ∨ (∀s₁)(s₁∈e₁ ↔ s₁=r ∨ (∀e)(e∈s₁ ↔ (∀s)(s∈e ↔ s=c₃) ∨ (∀s)(s∈e ↔ s=c₂ ∨ s=c₃)))) ∧ t∈f ) → r = c₅ )
there is ONE non-FOL symbol remaining, which is S in S(k)∈I
we'll re-express this as (∃z)(z=S(k) ∧ z∈I), using the same trick as before to deal with z=S(k)
(∀c₀, c₁, c₂, c₃, c₅)
(
(∀e)(¬(e∈c₀))
∧ (∀e)(e∈c₁ ↔ e∈c₀ ∨ e=c₀)
∧ (∀e)(e∈c₂ ↔ e∈c₁ ∨ e=c₁)
∧ (∀e)(e∈c₃ ↔ e∈c₂ ∨ e=c₂)
∧ (∀e)(e∈c₄ ↔ e∈c₃ ∨ e=c₃)
∧ (∀e)(e∈c₅ ↔ e∈c₄ ∨ e=c₄)
)
(∀N)
(
(∀n)( n∈N ↔ (∀I)( c₀∈I ∧ (∀k)(k∈I → (∃z)((∀m)(m∈z ↔ m∈k ∨ m=k) ∧ z∈I)) → n∈I ) )
) →
(∀f)
(
(∀a, b)( (∀t)( (∀e)(e∈t ↔ (∀s)(s∈e ↔ s=b) ∨ (∀s)(s∈e ↔ s=a ∨ s=b)) ∧ t∈f → (∃a₁,a₂)( a₁∈N ∧ a₂∈N ∧ (∀e)(e∈a ↔ (∀s)(s∈e ↔ s=a₂) ∨ (∀s)(s∈e ↔ s=a₁ ∨ s=a₂)) ) ∧ b∈N ) )
∧ (∀n)( n∈N → (∀r)( (∀t)( (∀e₁)(e₁∈t ↔ (∀s₁)(s₁∈e₁ ↔ s₁=r) ∨ (∀s₁)(s₁∈e₁ ↔ s₁=r ∨ (∀e)(e∈s₁ ↔ (∀s)(s∈e ↔ s=c₀) ∨ (∀s)(s∈e ↔ s=n ∨ s=c₀)))) ∧ t∈f → r = n ) ) )
∧ (∀n, k)( n,k∈N → (∀r)( (∀t)( (∀e₁)(e₁∈t ↔ (∀s₁)(s₁∈e₁ ↔ s₁=r) ∨ (∀s₁)(s₁∈e₁ ↔ s₁=r ∨ (∀e)(e∈s₁ ↔ (∀s)(s∈e ↔ (∀m)(m∈s ↔ m∈k ∨ m=k)) ∨ (∀s)(s∈e ↔ s=n ∨ (∀m)(m∈s ↔ m∈k ∨ m=k))))) ∧ t∈f → (∀r₁)( (∀t₁)( (∀e₁)(e₁∈t₁ ↔ (∀s₁)(s₁∈e₁ ↔ s₁=r₁) ∨ (∀s₁)(s₁∈e₁ ↔ s₁=r₁ ∨ (∀e)(e∈s₁ ↔ (∀s)(s∈e ↔ s=k) ∨ (∀s)(s∈e ↔ s=n ∨ s=k)))) ∧ t₁∈f → (∀m)(m∈r ↔ m∈r₁ ∨ m=r₁) ) ) ) ) )
) →
(∀r)( (∃t)( (∀e₁)(e₁∈t ↔ (∀s₁)(s₁∈e₁ ↔ s₁=r) ∨ (∀s₁)(s₁∈e₁ ↔ s₁=r ∨ (∀e)(e∈s₁ ↔ (∀s)(s∈e ↔ s=c₃) ∨ (∀s)(s∈e ↔ s=c₂ ∨ s=c₃)))) ∧ t∈f ) → r = c₅ )
Sweet. Let me run this through a formatter real quick!
uh... ok, probably none exists. I guess I'm doing this by hand.
(∀c₀∀c₁∀c₂∀c₃∀c₅)((∀e)(¬(e∈c₀))∧(∀e)(e∈c₁↔e∈c₀∨e=c₀)∧(∀e)(e∈c₂↔e∈c₁∨e=c₁)∧(∀e)(e∈c₃↔e∈c₂∨e=c₂)∧(∀e)(e∈c₄↔e∈c₃∨e=c₃)∧(∀e)(e∈c₅↔e∈c₄∨e=c₄))(∀N)((∀n)(n∈N↔(∀I)(c₀∈I∧(∀k)(k∈I→(∃z)((∀m)(m∈z↔m∈k∨m=k)∧z∈I))→n∈I)))→(∀f)((∀a,b)((∀t)((∀e)(e∈t↔(∀s)(s∈e↔s=b)∨(∀s)(s∈e↔s=a∨s=b))∧t∈f→(∃a₁,a₂)(a₁∈N∧a₂∈N∧(∀e)(e∈a↔(∀s)(s∈e↔s=a₂)∨(∀s)(s∈e↔s=a₁∨s=a₂)))∧b∈N))∧(∀n)(n∈N→(∀r)((∀t)((∀e₁)(e₁∈t↔(∀s₁)(s₁∈e₁↔s₁=r)∨(∀s₁)(s₁∈e₁↔s₁=r∨(∀e)(e∈s₁↔(∀s)(s∈e↔s=c₀)∨(∀s)(s∈e↔s=n∨s=c₀))))∧t∈f→r=n)))∧(∀n,k)(n,k∈N→(∀r)((∀t)((∀e₁)(e₁∈t↔(∀s₁)(s₁∈e₁↔s₁=r)∨(∀s₁)(s₁∈e₁↔s₁=r∨(∀e)(e∈s₁↔(∀s)(s∈e↔(∀m)(m∈s↔m∈k∨m=k))∨(∀s)(s∈e↔s=n∨(∀m)(m∈s↔m∈k∨m=k)))))∧t∈f→(∀r₁)((∀t₁)((∀e₁)(e₁∈t₁↔(∀s₁)(s₁∈e₁↔s₁=r₁)∨(∀s₁)(s₁∈e₁↔s₁=r₁∨(∀e)(e∈s₁↔(∀s)(s∈e↔s=k)∨(∀s)(s∈e↔s=n∨s=k))))∧t₁∈f→(∀m)(m∈r↔m∈r₁∨m=r₁)))))))→(∀r)((∃t)((∀e₁)(e₁∈t↔(∀s₁)(s₁∈e₁↔s₁=r)∨(∀s₁)(s₁∈e₁↔s₁=r∨(∀e)(e∈s₁↔(∀s)(s∈e↔s=c₃)∨(∀s)(s∈e↔s=c₂∨s=c₃))))∧t∈f)→r=c₅)
well, I removed all the spaces, anyway. Here it is without a scrollbar!:
- (∀c₀∀c₁∀c₂∀c₃∀c₅)((∀e)(¬(e∈c₀))∧(∀e)(e∈c₁↔e∈c₀∨e=c₀)∧(∀e)(e∈c₂↔e∈c₁∨e=c₁)∧(∀e)(e∈c₃↔e∈c₂∨e=c₂)∧(∀e)(e∈c₄↔e∈c₃∨e=c₃)∧(∀e)(e∈c₅↔e∈c₄∨e=c₄))(∀N)((∀n)(n∈N↔(∀I)(c₀∈I∧(∀k)(k∈I→(∃z)((∀m)(m∈z↔m∈k∨m=k)∧z∈I))→n∈I)))→(∀f)((∀a,b)((∀t)((∀e)(e∈t↔(∀s)(s∈e↔s=b)∨(∀s)(s∈e↔s=a∨s=b))∧t∈f→(∃a₁,a₂)(a₁∈N∧a₂∈N∧(∀e)(e∈a↔(∀s)(s∈e↔s=a₂)∨(∀s)(s∈e↔s=a₁∨s=a₂)))∧b∈N))∧(∀n)(n∈N→(∀r)((∀t)((∀e₁)(e₁∈t↔(∀s₁)(s₁∈e₁↔s₁=r)∨(∀s₁)(s₁∈e₁↔s₁=r∨(∀e)(e∈s₁↔(∀s)(s∈e↔s=c₀)∨(∀s)(s∈e↔s=n∨s=c₀))))∧t∈f→r=n)))∧(∀n,k)(n,k∈N→(∀r)((∀t)((∀e₁)(e₁∈t↔(∀s₁)(s₁∈e₁↔s₁=r)∨(∀s₁)(s₁∈e₁↔s₁=r∨(∀e)(e∈s₁↔(∀s)(s∈e↔(∀m)(m∈s↔m∈k∨m=k))∨(∀s)(s∈e↔s=n∨(∀m)(m∈s↔m∈k∨m=k)))))∧t∈f→(∀r₁)((∀t₁)((∀e₁)(e₁∈t₁↔(∀s₁)(s₁∈e₁↔s₁=r₁)∨(∀s₁)(s₁∈e₁↔s₁=r₁∨(∀e)(e∈s₁↔(∀s)(s∈e↔s=k)∨(∀s)(s∈e↔s=n∨s=k))))∧t₁∈f→(∀m)(m∈r↔m∈r₁∨m=r₁)))))))→(∀r)((∃t)((∀e₁)(e₁∈t↔(∀s₁)(s₁∈e₁↔s₁=r)∨(∀s₁)(s₁∈e₁↔s₁=r∨(∀e)(e∈s₁↔(∀s)(s∈e↔s=c₃)∨(∀s)(s∈e↔s=c₂∨s=c₃))))∧t∈f)→r=c₅)
