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.
> 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 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.
x,Hx->Mx
Hs
->
Ms
x,Hx->Mx
Hs->Ms
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
x,Hx->Mx
->
Hs->Ms
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!
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.
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.
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.)
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...
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)