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.

Owner
양현우
양현우
E5 自动续期

请选择跳转 新版本系统 (2021-2-9采用): 以后更新都在AutoApi,采用v0.0版本号覆盖式更新 AutoApi : 最新版 保留1到2个稳定的简易版,防止萌新大范围报错 AutoApi'X' : 稳定版1 ( 即本版AutpApiP ) AutoApiP ( 即v5.0,稳定版 ) —

95 Feb 15, 2021
BlueBorne Dockerized

BlueBorne Dockerized This is the repo to reproduce the BlueBorne kill-chain on Dockerized Android as described here, to fully understand the code you

SecSI 5 Sep 14, 2022
An open-source systems and controls toolbox for Python3

harold A control systems package for Python=3.6. Introduction This package is written with the ambition of providing a full-fledged control systems s

Ilhan Polat 157 Dec 05, 2022
A topology optimization framework written in Taichi programming language, which is embedded in Python.

Taichi TopOpt (Under Active Development) Intro A topology optimization framework written in Taichi programming language, which is embedded in Python.

Li Zhehao 41 Nov 17, 2022
Python script to commit to your github for a perfect commit streak. This is purely for education purposes, please don't use this script to do bad stuff.

Daily-Git-Commit Commit to repo every day for the perfect commit streak Requirments pip install -r requirements.txt Setup Download this repository. Cr

JareBear 34 Dec 14, 2022
Master Duel Card Translator Project

Master Duel Card Translator Project A tool for translating card effects in Yu-Gi-Oh! Master Duel. Quick Start (for Chinese version only) Download the

67 Dec 23, 2022
Example python package with pybind11 cpp extension

Developing C++ extension in Python using pybind11 This is a summary of the commands used in the tutorial.

55 Sep 04, 2022
Zues Auto Claimer Leaked By bazooka#0001

Zues Auto Claimer Leaked By bazooka#0001 put proxies in prox.txt put ssid in sid.txt put all users you want to target in user.txt for the login just t

1 Jan 15, 2022
A Snakemake workflow for standardised sc/snRNAseq analysis

single_snake_sequencing - sc/snRNAseq Snakemake Workflow A Snakemake workflow for standardised sc/snRNAseq analysis. Every single cell analysis is sli

IMS Bio2Core Facility 1 Nov 02, 2021
A simple website-based resource monitor for slurm system.

Slurm Web A simple website-based resource monitor for slurm system. Screenshot Required python packages flask, colored, humanize, humanfriendly, beart

Tengda Han 17 Nov 29, 2022
Web App for University Project

University Project About I made this web app to finish a project assigned by my teacher. It is written entirely in Python, thanks to streamlit to make

15 Nov 27, 2022
Curso de Python 3 do Básico ao Avançado

Curso de Python 3 do Básico ao Avançado Desafio: Buscador de arquivos Criar um programa que faça a pesquisa de arquivos. É fornecido o caminho e um te

Diego Guedes 1 Jan 21, 2022
Prototype application for GCM bias-correction and downscaling

dodola Prototype application for GCM bias-correction and downscaling This is an unstable prototype. This is under heavy development. Features Nothing!

Climate Impact Lab 9 Dec 27, 2022
MODeflattener deobfuscates control flow flattened functions obfuscated by OLLVM using Miasm.

MODeflattener deobfuscates control flow flattened functions obfuscated by OLLVM using Miasm.

Suraj Malhotra 138 Jan 07, 2023
AIO solution for SSIS students

ssis.bit AIO solution for SSIS students Hardware CircuitPython supports more than 200 different boards. Locally available is the TTGO T8 ESP32-S2 ST77

3 Jun 05, 2022
The blancmange curve can be visually built up out of triangle wave functions if the infinite sum is approximated by finite sums of the first few terms.

Blancmange-curve The blancmange curve can be visually built up out of triangle wave functions if the infinite sum is approximated by finite sums of th

Shankar Mahadevan L 1 Nov 30, 2021
Sikulix with Ubuntu Calculator Automation

CalculatorAutomation Sikulix with Ubuntu Calculator Automation STEP 1: DOWNLOAD and INSTALL SIKULIX https://raiman.github.io/SikuliX1/downloads.html T

Bedirhan Sayakci 2 Oct 27, 2021
WriteAIr is a website which allows users to stream their writing.

WriteAIr is a website which allows users to stream their writing. It uses HSV masking to detect a pen which the user writes with. Plus, users can select a wide range of options through hand gestures!

Atharva Patil 1 Nov 01, 2021
Graveyard is an attempt at open-source reimplementation of DraciDoupe.cz

Graveyard: Place for Dead (and Undead) Graveyard is an attempt at open-source reimplementation of DraciDoupe.cz (referred to as DDCZ in this text). De

DraciDoupe.cz 5 Mar 17, 2022
Flow control is the order in which statements or blocks of code are executed at runtime based on a condition. Learn Conditional statements, Iterative statements, and Transfer statements

03_Python_Flow_Control Introduction 👋 The control flow statements are an essential part of the Python programming language. A control flow statement

Milaan Parmar / Милан пармар / _米兰 帕尔马 209 Oct 31, 2022