A Logic Calculator | Hacker News Reader

A Logic Calculator

somerby.net

Hey all, I'm they guy that developed this app. There are a few things I'd like to say, if I may:

1) I really do want to improve this app and help anyone who is using it, so please do send me comments, criticisms and questions. There's a "contact" link on the app for that purpose.

2) Yes, the app's language is a language that I made up which isn't used anywhere else. I know it's not a good thing I'm making people learn a new language, but I really, really want the app to have a language that is easy to type. If you're trying to learn it, just keep in mind that has most of the elements that are in conventional symbolic logic, it just uses different symbols for them, e.g. AND is "&", "for all x, " is "x,", "there exist an x such that" is "3x,".

3) sundarurfriend: Thanks for posting this link. It's a pleasant surprise to see this app getting some attention.

'Decides statements in propositional logic, modal logic, unary (monadic) predicate logic and term logic' - description on the project's github repo[1].

There is a blog post[2] from the creator introducing the tool in 2014, with an example use case. Not exactly written for amateur laymen though, it dives deep quickly.

[1] https://github.com/mackwai/UnaryPredicateLogic [2] http://mackwai.blogspot.in/2014/03/investigating-logical-arg...

In the "A Categorycal Syllogism" example, the socrates example, it returns "true".

If I change the last line from "Ms" to "~Ms", why does it return "contingent"?

From what I understood, I expected this to return "false" (or maybe "self-contradictory", does "false" exist in this application?).

Because if every man is mortal, and socrates is a man, then saying "socrates is not mortal" is false, right? Not unknown or anything.

"False" does not exist here (when dealing with quantifiers). Contingent is technically correct, "invalid" would also work.

The program can output "necessarily true" if it is true in all possible worlds, "self-contradictory" if it is false in all possible worlds, and "contingent" if it is true in some and false in others.

It is indeed contingent. The intuitive problem is that "a -> ~b" is not logically equivalent to "~(a -> b)".

The "Counterexample" button shows a world in which the modified statement is false: there is a single man (Socrates) and he is mortal.

Unfortunately, the program doesn't have an "Example" button to show why it is contingent! The empty world is an example, though. This is because the hypothesis (which includes that there is a Socrates) is false, so the statement is vacuously true.

After more trying, I don't actually understand its syntax despite looking at the quick reference and instructions and the language

  x,Hx->Mx  
  Hs  
  ->  
  Ms

returns: necessarily true

  x,Hx->Mx
  Hs->Ms

returns: contingent

The only change is newlines. The quick reference says nothing about newlines. What's going on?

To do ~(Hs->Ms) instead of Hs->~Ms I have no choice but to put it on one line, if I try to use parenthesis on a multiline statement it gives errors. So how can I compare the multiline Hs->~Ms with a ~(Hs->Ms) that has the same newline behavior?

It could really use more examples, starting as simple as possible, e.g. something with fruits and colors with all simple combinations of true and contingent and self-contradictory things...

Is this syntax based on the syntax used in some scientific field? I also know some things about logic, but in the field of electronics with logic gates, CPU instructions, bit twiddling and programming languages :)

EDIT: update for hacker news itself destroying newlines

It looks like -> on a line of its own means "everything before this implies everything after it". So, for your second example you want

  x,Hx->Mx
  ->
  Hs->Ms

which returns "The statement is necessarily true."

You would see this syntax in a typical mathematical logic class. It ANDs (&) together each statement before and after the ->.

Here, we might say -- Ha: a is Human, Ma: a is Mortal. Then the first example says: "((For all x, if x is Human, then x is Mortal) AND (s is Human)) IMPLIES (s is Mortal)".

We could write it on one line like this: (x,Hx->Mx) & Hs -> Ms, which gives the same result (necessarily true).

To show that ~(Hs->Ms) is not logically equivalent to Hs->~Ms, you would write: ~(Hs->Ms) <=> Hs->~Ms. If you want, you can break it into three lines instead. The web app says this is contingent, which indicates it is neither always true nor always false. (Though technically this is a false statement, since they are not logically equivalent.) An example that is always false would be: Hs <=> ~Hs (i.e. from it we derive a contradiction).

Compare that to the logically consistent statement: ~(Hs->Ms) <=> Hs & ~Ms. ("(It is NOT the case that (s being Human IMPLIES s is Mortal)) IF AND ONLY IF (s is Human) AND (s is NOT Mortal).") In other words: the only time Hs does not imply Ms is (of course) when Hs is true and Ms is false!

> ~(Hs->Ms) <=> Hs->~Ms [...] this is contingent [...] Though technically this is a false statement

It's just not provable. The webapp can give the example of a world with a single object that is neither H nor M (in which case the statement is false). With some thought, I found a world where the statement is true: a single object that is H but not M.

If the statement were false, then this second world couldn't exist.

That said, while "logical equivalence" can mean the biconditional, as it does in the webapp, you are probably meaning logical equivalence at a level just outside individual worlds. Godel's completeness theorem is about the equivalence between whether a statement is true in all words and whether there is a proof of that statement. The earlier example illustrates that just because something's not provable doesn't mean it's false.

> So how can I compare the multiline Hs->~Ms with a ~(Hs->Ms) that has the same newline behavior?

I was wondering about that, too, but I could only figure out putting it all on one line.

> Is this syntax based on the syntax used in some scientific field?

I think the quantifier notation is vaguely Peano's original notation, and I think the idea of having HYPOTHESES -> CONCLUSIONS is sort of a Coq-like "above-the-line and below-the-line" thing, or maybe it's that way because it's optimized for syllogisms. Other than that, I've never seen a logic language quite like this one before.

Something I'd like to see someday is a Scratch-like snap-together logic and proof language. I toyed with the idea when I was teaching a discrete math course, but I didn't have time to develop one.

It's the propositional calculus - https://en.wikipedia.org/wiki/Propositional_calculus

It has quantifiers so it would be predicate calculus (first-order logic) - https://en.wikipedia.org/wiki/First-order_logic

I thought the question was more about the syntax of the logic language (which I think is rather idiosyncratic), but I can see that maybe they were asking about the relevant part of math.

(It might be worth noting that the webapp is not exactly first-order logic because it has some extra operators from modal logic.)

> Other than that, I've never seen a logic language quite like this one before.

One part of the documentation[1] implies it was a language designed by the project's creator himself:

"""

The language this tool uses is a kind of symbolic logic. It was designed with these criteria in mind:

The language should only use basic SCII characters which are available on a standard English keyboard, so typing expressions in the language is easy.

The language should be terse in such a way that it is fast to type but not generally difficult to read.

The language should enable a person to arrange expressions in such a way that they are readable.

The symbols defined in the language should have a precedent in other languages. The symbols in this language are borrowed from conventional symbolic logic, conventional mathematical notation, and the C programming language.

"""

[1] http://somerby.net/mack/logic/documentation.html#the_languag...

> The only change is newlines. The quick reference says nothing about newlines.

Under 'Valid Expressions', it has: "If it is multiple lines, the software joins those lines to be a single expression and decides that statement. The software treats each line that is a statement as if it were conjoined to the other lines that are statements with a logical AND. "

And if you try the Depict button on those two expressions, you'll see that the first is interpreted as ((x, Hx->Mx)&Hs)->Ms) whereas the second is seen as (x, Hx->Mx)&(Hs->Ms)

Good idea. It makes sense that if there is a "Counterexample" button, there should also be an "Example" button. I have added an "Example" button to the app. I've only tested it a little, so if you try it out, please tell me if it isn't working.

I tried it with a few examples ("Hx", "x=y", Correa's counterargument) but it seems to always throw this error:

> Error: TypeError: constructProposition(...).findExample is not a function

I've enjoyed playing with the program (and I like seeing the different ways people design computer languages for logic).

Another feature that might be interesting is to be able to ask the program for another example or counterexample. I imagined an "Another" button below a given example or counterexample. This is assuming the program already has the ability to enumerate worlds.

I had that same error; Firefox was using a cached version of a Javascript file instead of loading the new one. Typing Ctrl+F5 (Reload & override cache) fixed it. I don't know the command for other browsers.

I might try to implement an "another example" feature some time. The program enumerates worlds internally when it is searching for an example/counterexample, so that feature should be doable.

Reply on news.ycombinator.com