>>17305 (CONT)
this will hopefully be the final spoon feed. i will show you how to actually put all of this into formal logic (with polymorphic predicates). let us consider a basic moral action, for instance killing. it is a predicate that accepts 2 arguments. denote 'K(x,y)' to mean 'x kills y'.
now the unqualified statement '~kill' doesn't bound any variables. it is an atomic formula in predicate logic. as i pointed out earlier,
atomic formulas in predicate logic do not have truth values. clearly they can't. now if we want to try making it truth-apt, we should at least bound things. this gives us: '(∀x)(∀y)K(x,y)' which means 'nothing should kill anything'
clearly such a statement is not adequate. we note that the statement "thou shalt not kill" is what i was originally responding to. a naive reading of this statement requires us to specify the type of the variable (the moral agent), which gets us '(∀x::person)(∀y)K(x,y)'. of course, such a reading runs into the first problem i brought up, namely that there are some things that frankly do not matter if we kill or not. what we need to do is to specify both the agent and the patient
this takes us to the example i brought up again regarding asymmetry between people and animals in regards to killing:
"people shouldn't kill animals" should be written as '(∀x::person)(∀y::animal)K(x,y)'
"animals shouldn't kill people" should be written as '(∀x::animal)(∀y::person)K(x,y)'
now we move to the problem of calculating moral values. this requires a valuation function (which in your c code corresponds to eval). define such a system, we should rewrite statements of the form '(∀x::X)(∀y::Y)A(x,y)' as the ordered triple (A,X,Y). this is where X and Y are types, and A is a predicate
denote T the set of types, P the set of predicates, and S the set of ordered triples of the form (A,X,Y) where X and Y are types, and A is a predicate
we first define 2 predicate-type evaluations. f:T -> Z, and g:T -> Z (where Z is the set of integers). we also need a predicate evaluation h:P -> Z. then we can define the valuation function as the following:
v: S -> Z; (A,X,Y) |-> h(A)*f(X)*g(Y)...
so the way to express this in formal logic is through the following interpretation:
let 'p' denote the type 'person', let 'a' denote the type 'animal', and finally let 'K(x,y)' denote the predicate 'x kills y'. then the structure:
char *pretable[8][8][8] = {{ "people", (char*)1, (char*)10},
{ "animal", (char*)10, (char*)-1},
{ "kill", (char*)-10, (char*)1}
};
eval( "people", "kill", "animal" ); = 9 good
eval( "animal", "kill", "people" ); = -900 bad
(note that i shifted the example to show subtleties in the interaction between arguments and weights)
can be formalized as:
h := {(K,-10)}
f := {(p, 1), (a, 10)} (i.e. it is going to matter much more if an animal does things vs)
g := {(p,10),(a, -1)} (i.e. it is going to matter much more if something happens to a person than an animal)
so that
v(K,p,a) = 9
v(K,a,p) = -900
one thing to note is that really our predicate-type valuations should really be indexed for each predicate to be more accurate, but i am already writing too much