a simple proof system I made to learn math without any mistakes

Overview

math_up

a simple proof system I made to learn math without any mistakes




0. Short Introduction


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. Sentence Generation


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 

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 

2. Numbering or Naming Statements

(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.

3. Inferences

(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. Remarks


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.

You might also like...
Learn to code in any language. If

Learn to Code It is an intiiative undertaken by Student Ambassadors Club, Jamshoro for students who are absolute begineers in programming and want to

Hacktoberfest2021 🥳- Contribute Any Pattern In Any Language😎 Every PR will be accepted Pls contribute
Hacktoberfest2021 🥳- Contribute Any Pattern In Any Language😎 Every PR will be accepted Pls contribute

✨ Hacktober Fest 2021 ✨ 🙂 All Contributors are requested to star this repo and follow me for a successful merge of pull request. 🙂 👉 Add any patter

A proof-of-concept package manager for Cairo contracts/libraries

glyph A proof-of-concept package manager for Cairo contracts/libraries. Distribution through pypi. Installation through existing package managers -- p

Simple cash register system made with guizero

Eje-Casher なにこれ guizeroで作った簡易レジシステムです。実際にコミケで使う予定です。 これを誰かがそのまま使うかどうかというよりは、guiz

A small script I made that takes any standard Decklist of magic the gathering cards and pulls all card images from scryfall at once!

A small script I made that takes any standard Decklist of magic the gathering cards and pulls all card images from scryfall at once!

pythonOS: An operating system kernel made in python and assembly
pythonOS: An operating system kernel made in python and assembly

pythonOS An operating system kernel made in python and assembly Wait what? It uses a custom compiler called snek that implements a part of python3.9 (

Python Interactive Graphical System made during Computer Graphics classes (INE5420-2021.1)
Python Interactive Graphical System made during Computer Graphics classes (INE5420-2021.1)

PY-IGS - The PYthon Interactive Graphical System The PY-IGS Installation To install this software you will need these dependencies (with their thevelo

Snek-test - An operating system kernel made in python and assembly
Snek-test - An operating system kernel made in python and assembly

pythonOS An operating system kernel made in python and assembly Wait what? It us

Simple Python-based web application to allow UGM students to fill their QR presence list without having another device in hand.

Praesentia Praesentia is a simple Python-based web application to allow UGM students to fill their QR presence list without having another device in h

Owner
양현우
양현우
A Python tool to check ASS subtitles for common mistakes and errors.

A Python tool to check ASS subtitles for common mistakes and errors.

null 1 Dec 18, 2021
Slotscheck - Find mistakes in your slots definitions

?? Slotscheck Adding __slots__ to a class in Python is a great way to reduce mem

Arie Bovenberg 67 Dec 31, 2022
Simple and easy to use python API for the COVID registration booking system of the math department @ unipd (torre archimede)

Simple and easy to use python API for the COVID registration booking system of the math department @ unipd (torre archimede). This API creates an interface with the official browser, with more useful functionalities.

Guglielmo Camporese 4 Dec 24, 2021
emoji-math computes the given python expression and returns either the value or the nearest 5 emojis as measured by cosine similarity.

emoji-math computes the given python expression and returns either the value or the nearest 5 emojis as measured by cosine similarity.

Andrew White 13 Dec 11, 2022
It's a repo for Cramer's rule, which is some math crap or something idk

It's a repo for Cramer's rule, which is some math crap or something idk (just a joke, it's not crap; don't take that seriously, math teachers)

Module64 0 Aug 31, 2022
Gives you more advanced math in python.

AdvancedPythonMath Gives you more advanced math in python. Functions .simplex(args: {number}) .circ(args: {raidus}) .pytha(args: {leg_a + leg_2}) .slo

Voidy Devleoper 1 Dec 25, 2021
Geodesic Dome Math

dome Geodesic Dome Math Python dome tool dome.py calculates an icosahedron or 2v geodesic dome and creates 3d printable hubs as OpenSCAD sources. usag

Brian Olson 2 Feb 9, 2022
Tool to generate wrappers for Linux libraries allowing for dlopen()ing them without writing any boilerplate

Dynload wrapper This program will generate a wrapper to make it easy to dlopen() shared objects on Linux without writing a ton of boilerplate code. Th

Hein-Pieter van Braam 25 Oct 24, 2022
Create or join a private chatroom without any third-party middlemen in less than 30 seconds, available through an AES encrypted password protected link.

PY-CHAT Create or join a private chatroom without any third-party middlemen in less than 30 seconds, available through an AES encrypted password prote

null 1 Nov 24, 2021
Manually Install Python 2.7 pip without any problem !

Python2.7_install_pip Manually Install Python 2.7 pip without any problem ! Download installPip.py to your system and Run the code using this Command

Ali Jafari 1 Dec 9, 2021