reckless intuitions of an epistemic hygienist ([info]gustavolacerda) wrote,
@ 2005-11-02 13:21:00
Previous Entry  Add to memories!  Tell a Friend!  Next Entry
Entry tags:formal_ed, formal_math, math

Pralam: A Practical Language for Mathematics
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.


(Post a new comment)

don't know if you know prolog, but...
[info]metaeducat10n
2005-11-02 08:15 pm UTC (link)
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.

(Reply to this) (Thread)
Re: don't know if you know prolog, but...
[info]gustavolacerda
2005-11-02 09:23 pm UTC (link)
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.

(Reply to this) (Parent)(Thread)
Re: don't know if you know prolog, but...
[info]metaeducat10n
2005-11-02 09:46 pm UTC (link)
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.

(Reply to this) (Parent)(Thread)
Re: don't know if you know prolog, but...
[info]gustavolacerda
2005-11-02 10:11 pm UTC (link)
Mizar is closer to what I want. Maybe it already does everything I want, if it tolerates undefined predicates.

(Reply to this) (Parent)
Re: don't know if you know prolog, but...
[info]gustavolacerda
2005-11-02 10:27 pm UTC (link)
you might enjoy reading about Mathematical Knowledge Management, which is the ultimate KM problem.

(Reply to this) (Parent)

Create an Account
Forgot your login or password?
Login w/ OpenID
English • Español • Deutsch • Русский…