gusl | Pralam: A Practical Language for Mathematics

You're viewing

gusl's journal
Create a Dreamwidth Account Learn More

Reload page in style: site light

Pralam: A Practical Language for Mathematics
I'm proposing an easy way of formalizing mathematics, by translating mathematical statements into FOL formulas. Please comment or contribute on the wiki.

Flat | Top-Level Comments Only

From:

metaeducat10n.livejournal.com

You may be alluding to your awareness of Prolog with the name "Pralam":

"Programming in Prolog is very different from programming in a procedural language. In Prolog you supply a database of facts and rules; you can then perform queries on the database. The basic unit of Prolog is the predicate, which is defined to be true. A predicate consists of a head and a number of arguments"

Either way, it seems to be a language which is very relevant for comparison purposes. I think you should at least explain precisely what is missing from Prolog that you're trying to add, and what benefits are offered by inventing a new syntax.

From:

gustavolacerda.livejournal.com

oh, I know Prolog. The similarity in name is unintentional.

What I am proposing is *not* a programming language. It's merely a language for writing mathematics more formally: definitions, theorems and proofs. Mathematicians rarely do this.

You can indeed do a good bit of FOL in Prolog, but not all of it. For instance, you can't state "exists X" without a witness.

For example, from "every man has a wife"
forall x ( man(x) -> exists y (wife_of(y,x)) )

and "Socrates is a man"
man(socrates)

we would like to conclude that "Socrates has a wife"
exists y (wife_of(y,socrates))

but Prolog won't let you do this, unless it knows who Socrates's wife(ves) is(are). In fact, it will tell you that socrates has no wife. Actually you probably can't express "exists" in Prolog.

So we'd have to implement a FOL prover on top of Prolog. Or, rather, use someone else's implementation.

From:

metaeducat10n.livejournal.com

Hmmm...perhaps what you want to do is more like Cyc...there is a Logic&math "Microtheory" in the concept map (MathMT).

Inference engines are just a pain to design from scratch, and usually don't get very far off the ground—though existing ones have limitations, it's hard to do much better unless you're doing something very special-purpose and clever. And reinventing syntaxes for these things have the same problem.

If you can work your ideas into an existing structure, or even just write a paper, you might qualify for a $2500 prize! But again, the key value of pointing out a precise flaw in something and then suggesting a remedy allows people to really grasp the meat of what you are saying.