New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

System for adding axioms #63

Open

io12 opened this issue Jul 11, 2020 · 1 comment

Labels

enhancement help wanted libaris UI WASM

Contributor

io12 commented Jul 11, 2020

No description provided.

io12 added enhancement help wanted UI WASM libaris labels

io12 mentioned this issue

Add induction #64

Closed

Member

Bram28 commented Jul 11, 2020

Yes, there is an axiom of axiom, if you can quantify over formulas with free variables:

Weak Mathematical Induction:

forall P(x) [(P(0) & forall x (P(x) -> P(s(x)))) -> forall x P(x)]

Strong Mathematical Induction:

forall P(x) [forall x (forall y (y < x -> P(y)) -> P(x)) -> forall x P(x)]

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment