Proof

A proof is a chain of reasoning that starts from things everyone agrees are true and arrives at a new true statement, one step at a time. Each step must follow from the previous ones by a rule that both sides accept. If you have ever explained why something is true — not just that it is true — you have given an informal proof.

In mathematics, the starting points are called axioms: statements accepted without proof. The rules that let you move from one statement to the next are called inference rules. A proof begins with axioms and applies inference rules repeatedly until it reaches the desired conclusion. If every step is valid, the conclusion is a theorem.

Two common proof strategies illustrate how this works:

• Direct proof: start from the assumptions and work forward to the conclusion. To prove “if $n$ is even, then $n^2$ is even,” you write $n=2k$ for some integer $k$, compute $n^2=4k^2=2(2k^2)$, and observe that $n^2$ is twice an integer, so it is even.
• Proof by contradiction: assume the opposite of what you want to prove, then show that assumption leads to an impossibility. Euclid used this strategy to prove that there are infinitely many prime numbers.

There is a deep split in the foundations of mathematics about what counts as a valid proof. Classical logic allows proof by contradiction freely: to prove something exists, it is enough to show that its nonexistence would be absurd. Constructive logic demands more — to prove something exists, you must actually produce it. A constructive proof of “there exists an even prime” must exhibit the number 2, not merely argue that no-even-prime leads to a contradiction.

This vault uses Heyting algebras rather than Boolean algebras as its logical foundation, and that choice reflects a commitment to constructive reasoning. In a Heyting algebra, the law of excluded middle ($p\vee \neg p$) does not hold in general, which means proofs within the semiotic universe must construct the objects they claim exist. This is not a limitation but a feature: it ensures that every existential claim comes with a witness.

Related concepts

• Heyting algebra — the algebraic structure behind constructive logic
• Boolean algebra — the algebraic structure behind classical logic
• Set theory — one of the standard foundations from which axioms are drawn
• Type theory — an alternative foundation where proofs are programs
• Curry-Howard correspondence — the bridge between proofs and programs
• Semiotic universe — uses constructive reasoning throughout