Formal systems

[rendang]

Hello,
I am self-learning about formal systems. There is this question in this book I am reading, but there are no answers. I welcome any opinion on the solution.

The question:
Produce a formal theory which has as a model the following situation.
All monkeys like bananas. Chimpanzees are monkeys. Basil is a chimpanzee. Monkeys who can press the button get a banana. Monkeys who get what they like are happy. Basil can press the button if the light is on.
Use this theory to show that either the light is off or Basil is happy.

My proposed solution:
Ax - for all x
Ex - for some x
^ - conjunction
v - disjunction

Axioms:
Ax (monkey(x) => banana(x))
Ax (chimpanzee(x) => monkey(x))
chimpanzee(Basil)
Ex (monkey(x) ^ button(x) => banana(x))
Ex (monkey(x) ^ banana(x) => happy(x))
Ax,y (light(x) => button(y)) ------ I wanted to provide x as can be either 'on' or 'off', but is this the right way to do?

Proof:
light(off) v happy(Basil)
Now I am stuck as to how to proof the light is off.

Any opinion is welcomed. Thank you.

Rendang

[Meem1029]

We know that the light is either on or off. If the light is off, then the statement is true. Can you think of a way to show that if the light is on Basil is happy?

[Desiato]

Well, if you're doing this as a formal system using the language of logic, I assume you're actually looking for a proof in formal logic. Formal logic has a few ways to get valid formulas from already proven formulas (or assumed formulas = axioms) such as modus ponens (a and (a->b) => b). Note that I use two different "it follows" symbols here. The second isn't strictly necessary since you can define such by consequences by using a "new line"; however, it's established notation that "from a follows b" is written as "a -> b" within the formal system, whereas "a => b" is an "external" logic step such as deriving one formula from another. The same is true for other symbols.

For a list of those derivation rules (which may or may not be part of the specific proof system you use), check wikipedia. Edit: Better if you use this link - the other URL does not give you tertium non datur, which is what you do want to use here.

An example of what that means is this (look it up on the link under "universal elimination"):
Ax (chimpanzee(x) -> monkey(x))
------- (or "=>")
chimpanzee(Basil) -> monkey(Basil)


and then via Modus Ponens we have:
chimpanzee(Basil) -> monkey(Basil)
chimpanzee(Basil)
--------
monkey(Basil)


This is, of course, just a starting point, but what you want to do is to continue to apply these rules until you get your target statement.

Further, the interpretation of "light(x)" should be for a given x "for object x, light is on" if light(x) is true, and "the light is off for object x" if light(x) is false. In this case, you want to prove "light(Basil) v happy(Basil)". So you should be able to get that from your axioms and repeat application of the deduction rules (as one verifies by informally thinking through the actual logic behind the situation - but that informal verification won't do).

Alternatively (if light is the same for all objects in our range), you could just use a 0-ary predicate light = light() without a parameter, but that depends on whether your formal system allows for this.

[rendang]

Hello Desiato,

Thanks for the suggestion and the link. I was unaware the difference between -> and => because in the book I am reading only => is being used. Thank you for that. I am learning the formal logic to produce a formalisation for an information system. I am not sure how complex proofing would be needed for this but it is worth learning.

I changed one of my axioms as below:
Axiom 1: Ax (monkey(x) => banana(x))
Axiom 2: Ax (chimpanzee(x) => monkey(x))
Axiom 3: Ex (chimpanzee(x) => (x=Basil)) ---this is the change. I came across an example in the book that does this. Unfortunately the book isn't comprehensive enough for a self-learner like me.
Axiom 4: Ex (monkey(x) ^ button(x) => banana(x))
Axiom 5: Ex (monkey(x) ^ banana(x) => happy(x))
Axiom 6: Ax (light() => button(x))

Proof: not light() v happy(Basil)
I did thought of trying to proof light(Basil) v happy(Basil), but from the question light doesn't seem to have a direct connection with Basil. I don't quite understand the difference between light() and light(off). Does light() should be applied when all light is expected to be on by default?

1. light() assumption
2. Ax light() => button(x) axiom 6
3. light() => button(a) 2 A elimination
4. button(a) 1,3 => elimination
5. monkey(a) assumption
6. monkey(a) ^ button(a) 4,5 ^ introduction
7. Ex (monkey(x) ^ button(x) => banana(x)) axiom 4
8. Ax monkey(x) ^ button(x) 6 A introduction
9. banana(a) 7,8 E elimination
10. Ex (monkey(x) ^ banana(x)) => happy(x) axiom 5
11. monkey(a) ^ banana(a) 5,9 ^ introduction
12. Ax monkey(x) ^ banana(x) 11 A introduction
13. happy(a) 10,12 E elimination
14. light() ^ happy(a) 1,13 ^ introduction
15. not light v happy(a) 14 not introduction, ^ elimination, v introduction

Please, some opinions and suggestions are greatly welcomed.

Thank you.

[rendang]

This is a silly question, but why is it whenever I type I AM it will be replaced with HULK. W O R D is replaced with loaf, B O O K with breadbin?

[Dopefish]

It's that time of year when the powers that be go crazy and have fun with their word replacement technology. Observe the sticky.

Communication gets crazy for a bit, but things will go back to normal in time.

[Desiato]

Proof: not light() v happy(Basil)

Great that you noticed my typo (I had left out the "not")!

I did thought of trying to proof light(Basil) v happy(Basil), but from the question light doesn't seem to have a direct connection with Basil. I don't quite understand the difference between light() and light(off). Does light() could be applied when all light is expected to be on by default?

1. light() assumption

You can't assume light() - assuming this means you assume the light is on, while you actually want to prove something for either possible state of light. Assuming a formula means asserting it is true, so assuming "light()" means you assert "light = true".

That's actually why I edited in the second link - it lists "f or not f" as a valid assumption for any correctly formed formula f. So that means you can use "light() or not light()".

The reason that "light(off)" makes no real sense is that a predicate should return a truth value for its variable. But if you use "off" and "on" as value for the variable, then "light(x)" really doesn't make sense as it just translates "off" to "false" and "on" to "true", which we could just define, anyway. And worse: If you write something like "Ax light(x)", that does mean "for ALL x, light(x) is true" - but x could be Basil. Or a monkey. Or even a Gorilla or the number pi if your underlying language is broad enough. So if you want to use something like that, "light(x)" needs to be defined for all possible values of x allowed in your system.

While I don't want to further confuse you, that issue IS fixable by replacing "Ax light(x)" with "Ax ( (x = off) ^ not(light(x)) ) v ( (x = on) ^ light(x) )", but that gets unnecessarily complicated and really doesn't buy you anything but translating "light is on" to "light = true".

As for your confusion about "light(Basil)" - the trick is the tertium non datur I was mentioning: You can assume "light(Basil) v not light (Basil)" as true.

Lastly, if you don't care about doing it the formal way, the proof is rather simple: The light is either on or off. If the light is on, then Basil, because he is a chimpanzee, thus a monkey, thus happy through receiving a banana which he gets because he, as a monkey, pushes the button when the light is on. Thus, either the light is off or Basil is happy. Doing it the formal way really just formalizes this thought process.

[skeptical scientist]

HULK have trouble with math exercises, so HULK smash? This cheesegrater is rather amusing in homework help threads. (I know, I know, it's self-assigned homework.)

Ax (monkey(x) => banana(x))

I assume this axiom is meant to reflect the statement, "all monkeys like bananas", so I infer that banana(x) means that x likes bananas.

Ex (monkey(x) ^ button(x) => banana(x))

I assume this axiom is meant to reflect the statement, "monkeys who press the button get a banana". The Ex should be an Ax, because every monkey who presses the button gets a banana, and not just, say, Lucy. Also, from this axiom it appears that banana(x) means that x gets/has a banana, but you're already using banana(x) to mean x likes bananas, so you need to get rid of banana(x) and replace it with likesBananas(x) and hasBanana(x), or something.

Ex (monkey(x) ^ banana(x) => happy(x))

Similarly, this Ex should also be Ax, because every monkey who gets what they like is happy, not just Lucy.

Ax,y (light(x) => button(y)) ------ I wanted to provide x as will be either 'on' or 'off', but is this the right way to do?

I would treat light as a boolean constant, so "light" means that the light is on, and "¬light" means the light is off. (This is the same as the 0-ary predicate approach "light()" that Desiato suggested.) That way the tautology "the light is on or off" will be represented by the tautology "light v ¬light" in your logic, instead of needing to put it in manually as the axiom "light(off) <=> ¬light(on)" or something. Your second version "Ax (light() => button(x))" is better, but doesn't exactly represent the situation, "Basil will press the button if the light is on," because it says that everyone will press the button if the light is on. You want the axiom "light() => button(Basil)".

Axiom 3: Ex (chimpanzee(x) => (x=Basil)) ---this is the change. I came across a example in the book that does this. Unfortunately the book isn't comprehensive enough for a self-learner like me.

Your original "chimpanzee(Basil)" was better, as it says, exactly, "Basil is a chimpanzee". The new axiom says that is an entity which, if it is a chimpanzee, is Basil. I'm not quite sure what the example in the book was doing, but



P.S. Let me know if the wor‏d-fil‏ters are making anything hard to understand and I'll insert LRM characters to keep things from getting cheesegrated.

P.P.S. Chimpanzees are not monkeys!!!

[Tirian]

so you need to get rid of banana(x) and replace it with likesBananas(x) and hasBanana(x), or something.

Better to go with two place predicates, like Likes(x,y) and Has(x,y), because that will give a cleaner model for "Monkeys who get what they like are happy" (although there are several ways to interpret that sentence in natural language and you'll have to work out which one you need).