Comment on There are no odd numbers divisible by 2

Toes@ani.social ⁨1⁩ ⁨day⁩ ago

By god they are right, this might change the future of mathematics!

`// 2024‑edition Rust use std::rc::Rc;

/// Church numeral: given a successor s: fn(u32) -> u32, /// returns a function that applies s n times. type Church = Rc<dyn Fn(fn(u32) -> u32) -> Rc<dyn Fn(u32) -> u32>>;

/// 0 ≡ λs.λx.x fn zero() -> Church { println!(“Define 0”); Rc::new(|_s| Rc::new(|x| { println!(" 0 applied to {}“, x); x })) }

/// succ ≡ λn.λs.λx. s (n s x) fn succ(n: Church) -> Church { // label is printed before the closure is created, so the closure // does not capture any non‑'static reference. println!(“Build successor”); Rc::new(move |s| { // inner is the predecessor numeral applied to the same successor let inner = n(s); Rc::new(move |x| { // first run the predecessor let y = inner(x); println!(” predecessor applied to {} → {}“, x, y); // then apply the extra successor step let z = s(y); println!(” +1 applied to {} → {}“, y, z); z }) }) }

/// Convert a Church numeral to a Rust integer, printing each step. fn to_int(n: &Church) -> u32 { let inc: fn(u32) -> u32 = |k| { println!(” inc({})“, k); k + 1 }; let f = n(inc); // f: Rc<dyn Fn(u32) -> u32> println!(” evaluate numeral starting at 0"); f(0) }

/// Even ⇔ divisible by 2 fn is_even(n: &Church) -> bool { to_int(n) % 2 == 0 } fn is_odd(n: &Church) -> bool { !is_even(n) }

fn main() { // ---- build the numerals step‑by‑step ---- let zero = zero(); // 0 let one = succ(zero.clone()); // 1 = succ 0 let two = succ(one.clone()); // 2 = succ 1

// ---- show the numeric values (trace) ----
println!("\n--- evaluating 0 ---");
println!("0 as integer → {}", to_int(&zero));

println!("\n--- evaluating 1 ---");
println!("1 as integer → {}", to_int(&one));

println!("\n--- evaluating 2 ---");
println!("2 as integer → {}", to_int(&two));

// ---- parity of 2 (the proof) ----
println!("\n--- parity of 2 ---");
println!("Is 2 even? {}", is_even(&two)); // true
println!("Is 2 odd?  {}", is_odd(&two));  // false

// Proof: “divisible by 2” ⇔ “even”.
// Since `is_odd(&two)` is false, no odd number can satisfy the
// divisibility‑by‑2 condition.
assert!(!is_odd(&two));
println!("\nTherefore, no odd number is divisible by 2.");

} `

source
Sort:hotnewtop