Discrete math, executable

Sets, logic & quantifiers

Discrete math begins with sets and propositions — and Axioma writes them in their own notation. Set-builder {f(x) | x <- S, p} is set-builder, not a loop; forall/exists are real quantifiers over sets.

Set algebra

Union, intersection, difference, native symmetric difference (symdiff), power set, and a set comprehension.

Truth tables

truth_table takes a boolean function and returns every row of its table.

Quantifiers

Universal and existential quantification over a set, with a witnessing comprehension.

Proofs & relations

Here is where Axioma goes beyond a calculator. Relations are Datalog facts, rules derive new facts to a fixpoint, and why prints a machine-checked proof — the part most languages can't do at all.

A proof you can read

Facts plus a recursive rule give transitive closure; then ask the engine why a conclusion holds and it renders the derivation, labelled a theorem.

Equivalence classes

Congruence mod 3 partitions the integers into equivalence classes — one dict comprehension.

Number theory

From Euclid to RSA: gcd, a prime sieve written as the definition of primality, and the native modular toolkit — powmod, mod_inverse, totient.

GCD & the sieve

A prime is a number with no divisor strictly between 1 and itself — write that, and you have the sieve.

Modular arithmetic

Fast modular exponentiation, modular inverse (extended Euclid), and Euler's totient — the RSA / CRT staples, native.

Counting

Combinations and permutations are native (choose/nCr, permutations/nPr), Pascal's triangle is one comprehension, and inclusion–exclusion is just set cardinalities.

Combinations & Pascal's triangle

Inclusion–exclusion

|A ∪ B ∪ C| the hard way — and it matches the direct count.

Functions, sequences & induction

Function properties become set-cardinality checks; a summation identity is verified for every n in a range — induction made executable.

Injective & surjective

A function is injective iff its image is as large as its domain; surjective iff the image is the whole codomain.

Induction, executed

Check the Gauss identity Σ 1..n = n(n+1)/2 for every n from 1 to 20 — a finite stand-in for the inductive proof.

Graphs

A graph is a binary relation; reachability falls out of the same transitive-closure rule as ancestry — and graphform renders it as Graphviz DOT for free.

Reachability & rendering