logic survey ; designing logics
May. 2nd, 2007 12:16 pmI'd like to get an idea of how people tend to formalize reasoning processes.
Off the top of your head, how would you formalize "according to person A, it is the case that P"? You have complete freedom to choose any logic/formalism you want.
What about "according to Classical Mechanics, it is the case that P"?
---
Designing your logic. Here are different ways to define models:
"All men are mortal"
for all M, M |= man implies M |= mortal
(note that this is implicitly a statement about the set over which M is quantified)
Here, M |= phi means "person M has property phi". We are still doing reasoning a lot of reasoning outside the logic. So let's define a new kind of property, called an implication property. Now we can write:
for all M, M |= man -> mortal
(all things in the universe have the property that: if they are a man, then they are mortal)
Another problem is that we can't express relations between different people inside our logic (because we can't talk about relations between models). If we can bring people inside the logic, we will be able to express more things.
Also, the "for all" is still outside the logic. Let's push it in:
M |= forall x ( man(x) -> mortal(x) )
Since people are now objects, we can write things like M |= live-together(gustavo, nesky) .
But what does M mean now?
M now means the actual world, in which "All men are mortal" is the case. The formalism now gives us the freedom to imagine other possible worlds.
I like to think that what I did above, changing the meaning of "|=", as refactoring.
The first interpretation of M |= phi as "person M has property phi" is not very reusable: it's a hack.
Off the top of your head, how would you formalize "according to person A, it is the case that P"? You have complete freedom to choose any logic/formalism you want.
What about "according to Classical Mechanics, it is the case that P"?
---
Designing your logic. Here are different ways to define models:
"All men are mortal"
for all M, M |= man implies M |= mortal
(note that this is implicitly a statement about the set over which M is quantified)
Here, M |= phi means "person M has property phi". We are still doing reasoning a lot of reasoning outside the logic. So let's define a new kind of property, called an implication property. Now we can write:
for all M, M |= man -> mortal
(all things in the universe have the property that: if they are a man, then they are mortal)
Another problem is that we can't express relations between different people inside our logic (because we can't talk about relations between models). If we can bring people inside the logic, we will be able to express more things.
Also, the "for all" is still outside the logic. Let's push it in:
M |= forall x ( man(x) -> mortal(x) )
Since people are now objects, we can write things like M |= live-together(gustavo, nesky) .
But what does M mean now?
M now means the actual world, in which "All men are mortal" is the case. The formalism now gives us the freedom to imagine other possible worlds.
I like to think that what I did above, changing the meaning of "|=", as refactoring.
The first interpretation of M |= phi as "person M has property phi" is not very reusable: it's a hack.