a simple proof system I made to learn math without any mistakes
test yourself, enjoy your math!
math_up is an NBG-based, very simple but programmable proof verifier written in Python.
Some notable features are:
- super-simplicity, short learning time
- programmability
- fully written in Python (including all the proofs!)
- trade-off between runtime efficiency & reductionism
- non-generic implementation (supports only 1st-order logic, NBG set theory)
- supports on Fitch-style proofs, "let" variables and many other intuitive APIs
- rule-based, without any AI-like things
The following sections assumes you already know basic concepts on logic and set theory.
Author : Hyunwoo Yang
- Department of Mathematical Sciences, Seoul National University (2013 ~ 2019)
- Modem R&D Group, Samsung Networks (2019 ~ )
1-1. Variables
You may use alphabets from a to z, and also from A to Z.
Just calling clear() assures all the variables are new:
clear() # clear all alphabets
1-2. Atomic Properties
YourPropertyName = make_property("its_formal_name") # required at the first time
YourPropertyName(a, b) # usage
If the property is a binary relation, you can use operator overloading.
For example:
a <P< b # this returns P(a, b)
a %P* b # actually, any operators are OK
1-3. Logical Connections
~ P # not P
P & Q # P and Q
P | Q # P or Q
P >> Q # P imply Q
P == Q # P iff Q
true # true
false # false
1-4. Quantifiers
All(x, y, P(x, y)) # for all x and y, P(x, y)
Exist(x, y, z, P(x, y, z)) # there exists x, y and z such that P(x, y, z)
UniquelyExist(a, P(a, t)) # a is the only one such that P(a, t)
1-5. Functions
YourFunctionName = make_function("its_formal_name") # required at the first time
YourFunctionName(x, y, z) # usage
If the function is a binary operator, you can use operator overloading.
For example:
x <F< y # this returns F(x, y)
x %F* y # actually, any operators are OK
(your_sentence) @ 193
(your_sentence) @ "my_theorem"
Each number allows reuses, but the string names must be unique.
Hence, please number the sentences during the proof, but name the theorem at the last.
(your_sentence) @ (save_as, INFERENCE_TO_USE, *arguments, *reasons)
save_as is a number or string you'd like to save your_sentence as.
INFERENCE_TO_USE depends on the inference you want to use to deduce your_sentence.
Some arguments are required or not, depending on the INFERENCE_TO_USE
reasons are the numbers or strings corresponding to the sentences already proved, which are now being used to deduce your_sentence.
3-1. DEDUCE
with (your_assumption) @ 27 :
# your proof ...
(your_conclusion) @ (39, SOME_INFERENCE, argument0, argument1, reason0, reason1)
(your_assumption >> your_conclusion) @ (40, DEDUCE)
math_up supports Fitch-style proofs.
That means, you may make an assumption P, prove Q and then deduce (P implies Q).
The inference to use is DEDUCE.
DEDUCE doesn't require any arguments or reasons, but it must follow right after the end of the previous with block.
3-2. TAUTOLOGY
(A >> B) @ (152, INFERENCE0, argument0, reason0, reason1)
A @ (153, INFERENCE1, argument1, argument2, reason2)
B @ (154, TAUTOLOGY, 152, 153)
When is statement is a logical conclusion of previously proved sentences, and it can be checked by simply drawing the truth table, use TAUTOLOGY.
It doesn't require any arguments.
Put the sentences needed to draw the truth table as reasons.
3-2. DEFINE_PROPERTY
(NewProperty(x, y) == definition) @ ("save_as", DEFINE_PROPERTY, "formal_name_of_the_property")
You can freely define new properties with DEFINE_PROPERTY.
It does not requires any reasoning, but requires the formal name of the new property as the only argument.
3-3. DEFINE_FUNCTION
All(x, y, some_condition(x, y) >> UniquelyExist(z, P(x, y, z))) @ (70, INFERENCE0)
All(x, y, some_condition(x, y) >> P(x, y, NewFunction(z))) @ ("save_as", DEFINE_FUNCTION, 70)
Defining new function requires a sentence with a uniquely-exist quantifier.
Using DEFINE_FUNCTION, you can convert (for all x and y, if P(x, y) there is only one z such that Q(x, y, z)) into (for all x and y, if P(x, y) then Q(x, y, f(x, y)))
It requires no arguments, but one uniquely-exist setence as the only reason.
3-4. DUAL
(~All(x, P(x)) == Exist(x, ~P(x))) @ (32, DUAL)
((~Exist(y, Q(z, y))) == All(y, ~Q(z, y))) @ (33, DUAL)
not all == exist not, while not exist == all not.
To use these equivalences, use DUAL.
It requires no arguments or reasons.
3-5. FOUND
P(f(c)) @ (5, INFERENCE0, argument0)
Exist(x, P(x)) @ (6, FOUND, f(c), 5)
If you found a term satisfying the desired property, you can deduce the existence by FOUND.
It requires the term you actually found as an argument, and a sentence showing the desired property as the only reason.
3-6. LET
Exist(x, P(x)) @ (6, INFERENCE0, argument0, 5)
P(c) @ (7, LET, c, 6)
This one is the inverse of FOUND- i.e. it gives a real example from the existence.
It requires a fresh variable(i.e. never been used after the last clean()) to use as an existential bound variable as an argument.
Also, of course, an existential statement is required as the only reason.
3-7. PUT
All(x, P(x, z)) @ (13, INFERENCE0, 7, 9)
P(f(u), z) @ (14, PUT, f(u), 13)
PUT is used to deduce a specific example from the universally quantifiered sentence.
The term you want to put is an argument, and of course, the universally quantifiered sentence is the only reason.
3-8. REPLACE
P(x, a, a)
(a == f(c)) @ (8, INFERENCE0, argument0, 7)
P(x, a, f(c)) @ (9, REPLACE, 8)
When the two terms s and t are shown to be equal to each other, and the sentence Q is obtained from a previously proved P by interchainging s and t several times, REPLACE deduces Q from the two reasoning, i.e. s == t and P.
No arguments are needed.
3-9. AXIOM
any_sentence @ ("save_as", AXIOM)
AXIOM requires no inputs, but simply makes a sentence to be proved.
3-10. BY_UNIQUE
UniquelyExist(x, P(x)) @ (0, INFERENCE0)
P(a) @ (1, INFERENCE1, argument0)
P(f(b)) @ (2, INFERENCE2, argument1)
(a == f(b)) @ (3, BY_UNIQUE, 0, 1, 2)
BY_UNIQUE requires no arguments, but requires three reasons.
The first one is about unique existence, and the last two are specifications.
You can conclude two terms used for specifications respectively are equal to each other.
3-10. CLAIM_UNIQUE
Exist(x, P(x)) @ (6, INFERENCE0, argument0, 5)
P(c) @ (7, LET, c, 6)
P(d) @ (8, LET, d, 6)
# your proof ...
(c == d) @ (13, INFERENCE0, 12)
UniquelyExist(x, P(x)) @ (14, CLAIM_UNIQUE, 13)
CLAIM_UNIQUE upgrades an existence statement to a unique-existence statement.
Before you use it, you have to apply LET two times, and show the result variables are the same.
No arguments are required, but the equality is consumed as the only reason.
3-11. DEFINE_CLASS
UniquelyExist(C, All(x, (x in C) == UniquelyExist(a, UniquelyExist(b, (x == Tuple(a,b)) and Set(a) & Set(b) & P(a, b))))) @ (17, DEFINE_CLASS, C, x, [a, b], P(a, b))
This implements the class existence theorem of the NBG set theory.
No reasoning is required, but there are four arguments:
C : a fresh variable, to be a newly defined class
x : a fresh variable, to indicate the elements of C
[a, b, ...] : list of the components of x
P(a, b) : a condition satisfied by the components
4-1. Trade-Off : Runtime Efficiency vs. Reductionism
The class existence theorem is actually not an axiom, but is PROVABLE, due to Goedel
However, proving it requires recursively break down all the higher-level definitions to the primitive ones
I'm afraid our computers would not have enough resourse to do such tedious computation...
Similarly, meta-theorems such as deduction theorem, RULE-C, function definition are NOT reduced by this program.
4-2. Trade-Off : Readability vs. Completeness
Actually, we need one more axiom: All(x, P and Q(x)) >> (P and All(x, Q(x)))
But I'll not implement this here... it may not, and should not be needed for readable proofs.
For the similar reasons, the program doesn't allow weird sentences like All(x, All(x, P(x))) or All(x, P(y)).
Strictly speaking, math_up is an incomplete system to restrict the proofs more readable.
4-3. Acknowledgement
Thanks to everyone taught me math & CS.
Mendelson's excellent book, Introduction to Mathematical Logic was extremely helpful.
Jech's Set Theory was hard to read but great.