11 ms·

Note: There are today completely formal systems of proofs which are much more concise than what Russel had. You can now prove 1+1=2 after a few pages of rules (

Note: There are today completely formal systems of proofs which are much more concise than what Russel had. You can now prove 1+1=2 after a few pages of rules (say of Martin-Löf type theory), a couple of definitions (+, 1 and 2) and a very short proof by calculation. In practice, one would use a proof assistant, which is like a programming language, such as Agda. Then it is just the definitions and the proof is just a call to the proof checker to compute and check the result.

schoen 2y ago
For example, here it is in Coq (not using -- but instead replicating explicitly -- the built-in definitions of 0, 1, 2, +, or =). Inductive eq' {T: Type} (x: T) : T -> Prop := | eq_refl': eq' x x. Inductive nat' := | zero | succ (n: nat'). Definition one := succ zero. Definition two := succ (succ zero). Fixpoint plus' (a b: nat') : nat' := match a with | zero => b | succ x => succ (plus' x b) end. Theorem one_plus_one_equals_two : eq' (plus' one one) two. Proof. apply eq_refl'. Qed. As you allude to, there's also the underlying type theory and associated logical apparatus, which in this case give meaning to "Type", "Prop", "Inductive", "Definition", "Fixpoint", and "Theorem" (the latter of which is syntactic sugar for "Definition"!), and allow the system to check that the claimed proof of the theorem is actually valid. I haven't reproduced this here because I don't know what it actually looks like or where to find it. (I've never learned or studied the substantive content of Coq's built-in type theory.) We would also have to be satisfied that the definitions of eq', one, two, and plus' above sufficiently match up with what we mean by those concepts.
- chongli 2y ago
  Don’t forget the source code of Coq itself. What you have written here is not a formal proof, it’s a series of instructions to Coq requesting it to generate the proof for you. To know that you’ve proved it you need to inspect the output, otherwise you’re trusting the source code of Coq itself.

schoen 2y ago

For example, here it is in Coq (not using -- but instead replicating explicitly -- the built-in definitions of 0, 1, 2, +, or =). Inductive eq' {T: Type} (x: T) : T -> Prop := | eq_refl': eq' x x. Inductive nat' := | zero | succ (n: nat'). Definition one := succ zero. Definition two := succ (succ zero). Fixpoint plus' (a b: nat') : nat' := match a with | zero => b | succ x => succ (plus' x b) end. Theorem one_plus_one_equals_two : eq' (plus' one one) two. Proof. apply eq_refl'. Qed. As you allude to, there's also the underlying type theory and associated logical apparatus, which in this case give meaning to "Type", "Prop", "Inductive", "Definition", "Fixpoint", and "Theorem" (the latter of which is syntactic sugar for "Definition"!), and allow the system to check that the claimed proof of the theorem is actually valid. I haven't reproduced this here because I don't know what it actually looks like or where to find it. (I've never learned or studied the substantive content of Coq's built-in type theory.) We would also have to be satisfied that the definitions of eq', one, two, and plus' above sufficiently match up with what we mean by those concepts.

chongli 2y ago
Don’t forget the source code of Coq itself. What you have written here is not a formal proof, it’s a series of instructions to Coq requesting it to generate the proof for you. To know that you’ve proved it you need to inspect the output, otherwise you’re trusting the source code of Coq itself.