Simple proof verification system
% Remco Bloemen % 2009-12-26, last updated 2014-03-04
The incredible Metamath project contains proofs from the foundations of logic to ZFC set theory to real numbers to Hilbert spaces, all in a fascinatingly simple formal proof language.
But Metamath contains a non-intuitive rule when it comes to independent variables and I want to know if we can do without, so I’m on a mission to find the simplest proof verification system capable of verifying all of mathematics.
My proof language
In my simple proof system theories consist of three parts, hypotheses, axioms, and applications of other theories. Symbols used in the any of the statements exist only within the scope of the theory, if you apply a theory must provide a mapping from its symbols to expressions. This leads to the following verification algorithm:
-
Create an empty list, T.hypotheses, of hypotheses
-
Create an empty list, T.theorems, of true statements
-
Add all the hypotheses to T.hypotheses and T.theorems
-
Add all the axioms to T.theorems
-
For all applied theories G
a. Read the mapping from G statements to T statements
b. For all statements in G.hypotheses
i. Translate to a *T* statement using the mapping ii. Verify that the statement is in *T.theorems*c. For all statements in G.theorems
i. Translate to a *T* statement using the mapping ii. Add the statement to *T.theorems*
Symbol Meaning
T Start of theory, followed by the theory’s name
∧ Marks a hypothesis
⊨ Marks an axiom
∵ Apply theory name
⊧ a ⊧ b means expression b substitutes a
∴ The following should now be proved (for debugging purposes)
∎ End of theory
Implementation
Here is the implementation in C++: Proof.cpp
Rant: I once again found that
C sucks at string operations and the Unicode support is ridiculous. The Boost libraries fix a few of these issues at the cost of really slow compilation time and incomprehensible documentation and error messages, courtesy of the template system abuse that has become a standard in C.
I’m sceptical about C++x0 improving this situation.
Well-formedness of propositional calculus
I can now define a propositional logic calculus. To make things easier I use Łukasiewicz's polish notation. In this notation "N a" means "not a" or "¬a" and "C a b" means "from a follows b" or "a → b". There is no "and", "or", etc. since they can all be defined in terms of N and C.
T 'Well-formedness of Negation'
∧ Wff a
⊨ Wff N a
∎
T 'Well-formedness of Implication'
∧ Wff a
∧ Wff b
⊨ Wff C a b
∎
Inference rules axiomification
Now that I have the notation down and defined what well-formed formulas are I can state the axioms. The axiomatic system I chose is the same as that used by Metamath (see this page ). It’s one of the shortest to define, but the axioms are far from intuitive.
T 'Modus Ponens'
∧ Wff a
∧ Wff b
∧ a
∧ C a b
⊨ b
∎
T 'Principle of simplification'
∧ Wff a
∧ Wff b
∵ 'Well-formedness of Implication'
Wff ⊧ Wff
C ⊧ C
a ⊧ b
b ⊧ a
∵ 'Well-formedness of Implication'
Wff ⊧ Wff
C ⊧ C
a ⊧ a
b ⊧ C b a
∴ Wff C a C b a
⊨ C a C b a
∎
T 'Principle of transposition'
∧ Wff a
∧ Wff b
∵ 'Well-formedness of Negation'
Wff ⊧ Wff
N ⊧ N
a ⊧ a
∵ 'Well-formedness of Negation'
Wff ⊧ Wff
N ⊧ N
a ⊧ b
∵ 'Well-formedness of Implication'
Wff ⊧ Wff
C ⊧ C
a ⊧ b
b ⊧ a
∵ 'Well-formedness of Implication'
Wff ⊧ Wff
C ⊧ C
a ⊧ N a
b ⊧ N b
∵ 'Well-formedness of Implication'
Wff ⊧ Wff
C ⊧ C
a ⊧ C N a N b
b ⊧ C b a
⊨ C C N a N b C b a
∎
T 'Frege's axiom'
∧ Wff a
∧ Wff b
∧ Wff c
∵ 'Well-formedness of Implication'
Wff ⊧ Wff
C ⊧ C
a ⊧ b
b ⊧ c
∵ 'Well-formedness of Implication'
Wff ⊧ Wff
C ⊧ C
a ⊧ a
b ⊧ b
∵ 'Well-formedness of Implication'
Wff ⊧ Wff
C ⊧ C
a ⊧ a
b ⊧ c
∵ 'Well-formedness of Implication'
Wff ⊧ Wff
C ⊧ C
a ⊧ a
b ⊧ C b c
∵ 'Well-formedness of Implication'
Wff ⊧ Wff
C ⊧ C
a ⊧ C a b
b ⊧ C a c
∵ 'Well-formedness of Implication'
Wff ⊧ Wff
C ⊧ C
a ⊧ C a C b c
b ⊧ C C a b C a c
⊨ C C a C b c C C a b C a c
∎
Two proofs
T 'Inference introduction'
∧ Wff a
∧ Wff b
∧ a
∵ 'Principle of simplification'
Wff ⊧ Wff
C ⊧ C
a ⊧ a
b ⊧ b
∵ 'Modus Ponens'
Wff ⊧ Wff
C ⊧ C
a ⊧ a
b ⊧ C b a
∴ C b a
∎
T 'Principle of syllogism'
∧ Wff a
∧ Wff b
∧ Wff c
∧ C a b
∧ C b c
∵ 'Well-formedness of Implication'
Wff ⊧ Wff
C ⊧ C
a ⊧ a
b ⊧ b
∵ 'Well-formedness of Implication'
Wff ⊧ Wff
C ⊧ C
a ⊧ b
b ⊧ c
∵ 'Inference introduction'
Wff ⊧ Wff
C ⊧ C
a ⊧ C b c
b ⊧ a
∵ 'Frege's axiom'
Wff ⊧ Wff
C ⊧ C
a ⊧ a
b ⊧ b
c ⊧ c
∵ 'Modus Ponens'
Wff ⊧ Wff
C ⊧ C
a ⊧ C a C b c
b ⊧ C C a b C a c
∵ 'Modus Ponens'
Wff ⊧ Wff
C ⊧ C
a ⊧ C a b
b ⊧ C a c
∴ C a c
∎
Introduction to propositional logic:
In a propositional theory an expression is either Gibberish, Fickle, Bullshit or True. Here’s how it works:
Gibberish: Any statement that can’t be proved well-formed Example: 3 3 + = / What to do with it: Ignore it, it is meaningless.
Fickle: A well-formed statement that is neither True nor Bullshit Example: See this list, there are no easy examples. What to do with it: Consider adding it or its negation as an axiom to your theory, or ignore it.
Bullshit: A well-formed statement of which the negation can be proved Example: 3 + 3 = 5 What to do with it: Consider its negation.
True: A well-formed statement that can be proved Example: 3 + 3 = 6 What to do with it: Cherish it as discovered knowledge about your theory.
Why this theorem verifier is bad:
A good proof verifier should accept proofs for all True statements and not allow proofs for Bullshit. However, the proof verifier I described apove accepts the following proof for an obvious Bullshit statement:
T 'Implication introduction'
∧ b
⊨ C a b
∎
T 'Simplification'
∧ K a b
⊨ a
⊨ b
∎
T 'Bullshit'
∧ a
∵ 'Implication introduction'
C ⊧ K
a ⊧ N a
b ⊧ a
∵ 'Simplification'
K ⊧ K
a ⊧ N a
b ⊧ a
∴ N a
∎
The cause is obvious, it is the "C ⊧ K" line. But how do we prevent such fallacies from being accepted? My guess is that some of the variables "Wff C K N" (i.e. the operators) need a more permanent existence, beyond a single theory. But can this be done without introducing a lot of complication?
Make a global list of "predefined/constant" symbols? The operators obviously play a different role than the (variable) statements/wff they operate on. They say something/give a relation about the following wff’s, so they are metasymbols ;)
— Sander
