Quelklef

milk consumer

girly but not a girl

name-color: #C09


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₅)

You must log in to comment.

in reply to @Quelklef's post:

I mean, there are two distinct inductive sets up to isomorphism that match your definition I think. Your proof would still work with either of them. The natural numbers is the smaller of the two. I don't think the other one has a name.

N u { N }, because N = S(N)

(Pretend u is union. I'm typing this on my phone)

The ordinal numbers, and many of its subsets might also match. Not in the mood to check if that is for sure.

Basically, you need the induction axiom (from second order logic) most of the time in order to exclude ordinal numbers from the natural numbers. I think the way you used the infimum worked as a substitute for the induction axiom.