coonjecture

Joined 1 year ago

Karma

Submissions

Member since

Jan 10

Recent submissions

It seems the author is using the word logic, so logic boolean algebra suggests the classical case. Perhaps what is not trivial is that one can use that rule to deduce the other axioms. So that is not the theorem what is important but that one can prove any tautology using that simple axiom.

Comment · 1 year ago

Perhaps using Grobner basis for formal proofs [1],[2] could be similar to what appears here, that is during the proof the length of the terms (or polynomials) can grow and then at the end there is a simplification and you obtain a short grobner basis (short axioms).

A simple question, since • is nand, the theorem ((a•b)•c)•(a•((a•c)•a))=c, can be proved trivially computing the value of both sides for the 8 values of a,b,c. Also there are 2^(2^2)=16 logic functions with two variables so is trivial to verify that the theorem is valid iff • is nand. Perhaps the difficulty is proving the theorem using rules?, there must be something that I don't see (I just took a glimpse in a few seconds).

Automatic formal proofs can be useful when you are able to test [1] https://doi.org/10.1016/j.jpaa.2008.11.043 [2] https://ceur-ws.org/Vol-3455/short4.pdf