Aw, where was I...oh yes...Computability Logic
I did a lot of work on understanding various flavors of formal logic over summer, and I need to capture some of the things I found. Quite probably the most important event was me finding out about Computability Logic (CL). I've yet to get in deep, but I have an excellent reason to be excited by just skimming some papers.
Computability Logic is a logic that's based on semantics. And that's a big, big deal to me. It's the first example of "officially approved" (meaning: laid out by a logician with a degree that people take seriously) semantics-based logics that I've encountred. I didn't even know that a semantics-based logic could be valid in the mathematic realm. Semantics-based logics are the bread-and-butter logics for writers, of course, but I've always assumed that no card-carrying mathematician would take such "writerly" logic as serious. This assumption was based on my observation of some card-carrying mathematicians not taking such "writerly" logic as serious. Inductive logic: fast but dirty.
Having a formal logic at my disposal that is based on semantics is likely to help me bridge the gap between the knowledge that is encoded in my application right now and the theoretical knowledge that is currently available on this application. My current problem is that I have a working program, a working semantics, and I always thought that I would need to find a syntax-based logic that resulted in just those particular semantics, in order for mathematicians to understand my program on the theory level. That is, this is what I assumed up to here: that, to build a formal logic, you have to have a syntax first, and then you use this syntax as the foundation for the semantics. And what I found is that finding a pre-existing syntax that "affords" the semantics of a particular story's logic is a pain in the ass. So there is this gap between what I have working, and what I can say to explain it, to generalize from the existing program to a class of possible programs.
News flash: Looks like it doesn't have to be that way! Semantics can come first! I'll be reading "In the beginning there was Game Semantics..." to find out more.
Computability Logic is a logic that's based on semantics. And that's a big, big deal to me. It's the first example of "officially approved" (meaning: laid out by a logician with a degree that people take seriously) semantics-based logics that I've encountred. I didn't even know that a semantics-based logic could be valid in the mathematic realm. Semantics-based logics are the bread-and-butter logics for writers, of course, but I've always assumed that no card-carrying mathematician would take such "writerly" logic as serious. This assumption was based on my observation of some card-carrying mathematicians not taking such "writerly" logic as serious. Inductive logic: fast but dirty.
Having a formal logic at my disposal that is based on semantics is likely to help me bridge the gap between the knowledge that is encoded in my application right now and the theoretical knowledge that is currently available on this application. My current problem is that I have a working program, a working semantics, and I always thought that I would need to find a syntax-based logic that resulted in just those particular semantics, in order for mathematicians to understand my program on the theory level. That is, this is what I assumed up to here: that, to build a formal logic, you have to have a syntax first, and then you use this syntax as the foundation for the semantics. And what I found is that finding a pre-existing syntax that "affords" the semantics of a particular story's logic is a pain in the ass. So there is this gap between what I have working, and what I can say to explain it, to generalize from the existing program to a class of possible programs.
News flash: Looks like it doesn't have to be that way! Semantics can come first! I'll be reading "In the beginning there was Game Semantics..." to find out more.
scheuring - 11. Sep, 16:11
