|
Post by Eugene 2.0 on Jul 18, 2023 14:07:41 GMT
Does anyone know, how to get rid of that additional semantic rules in Predicate logic (PL) as these:
introducing general quantor (aka generalization): (C->Ax)->(C->(x)Fx), where C must not have x as a free variable
and
removing existential quantor (aka instantiation): ((Ex)Ax->C)->(Ax->C), where C must not have x as a free variable
C not having x isn't the last one requirement here, also Ax must be like At or having a new term.
That situation with substantiation in Predicate logic is the most dramatic, and it seems to be the ruiner of all the aesthetics of PL, and logic as well. Unlike Propositional logic where we can skip any semantics additional info or rules, here in PL that new variables and other requirement are absolutely annoying.
I haven't found any useful textbooks or any other info where PL is explained not with the rules of these.
I've got an idea with kinda chemistry variables as such x, y, z are the types of them, and having x and y means to have some new z which is another new element, comparably to x and y. They say there's also a combinatory logic to skip the rules for semantics in PL, but I don't think it's better. Combinatory logic seems making PL even less easier.
So, there must be some kind of formalization of those additional rules, but I don't think I can find it. I wish I could do this.
|
|