5 ms·

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 whic

• Aardwolf 9y ago
  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
  • morpher 9y ago
    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."
  • psyklic 9y ago
    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!
    • kmill 9y ago
      > ~(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.
  • kmill 9y ago
    > 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.
    • cachvico 9y ago
      It's the propositional calculus - https://en.wikipedia.org/wiki/Propositional_calculus https://en.wikipedia.org/wiki/Propositional_calculus
      • kmill 9y ago
        It has quantifiers so it would be predicate calculus (first-order logic) - https://en.wikipedia.org/wiki/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.)
    • sundarurfriend 9y ago
      > 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_language http://somerby.net/mack/logic/documentation.html#the_languag...
  • sundarurfriend 9y ago
    > 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)
• mackwai 9y ago
  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.
  • kmill 9y ago
    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.
    • mackwai 9y ago
      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.