Links
Football, video games, math, food, other stuff.
Tuesday, November 29, 2005
Some notes from school:
This commutative algebra course I'm taking this term is just killing me. It has just increasingly frustrated me (and the rest of the class) as the term has gone on. The exam is on Thursday; I can't wait for it to be over.
I went to a super-cool talk about logic today. Here was the idea. There is a nice correspondence between lambda-calculus and intuitionistic logic. lambda-calculus is just expressions in which every term could be anything, including another function. From wikipedia: "every expression stands for a function with a single argument; the argument of the function is in turn a function with a single argument, and the value of the function is another function with a single argument". It's just a way of writing out what a function does. Lambda-calculus expressions are the basis for super-recursive languages like LISP. Intuitionistic logic is logic in which we don't assume that a or not a is true. The correspondence between the two is that every provable statement in intuionistic logic is one for which a proof can be represeneted as a lambda-calculus statement.
All right, we haven't got to the cool part yet. The question is the following: if we take intuiniostic logic and add the classical logic axiom (a or not a is true), what do we need to add to lambda-calulus to continue the correspondence between the two? The answer is crazy: goto statments. Like I mentioned above, lambda-calculus statements can be viewed as programs, and by adding goto statements to this programming language, we get the equivalent of classical logic. In other words, goto statements allow one to prove a or not a.
Later on, I'll hopefully post why this is true.
This commutative algebra course I'm taking this term is just killing me. It has just increasingly frustrated me (and the rest of the class) as the term has gone on. The exam is on Thursday; I can't wait for it to be over.
I went to a super-cool talk about logic today. Here was the idea. There is a nice correspondence between lambda-calculus and intuitionistic logic. lambda-calculus is just expressions in which every term could be anything, including another function. From wikipedia: "every expression stands for a function with a single argument; the argument of the function is in turn a function with a single argument, and the value of the function is another function with a single argument". It's just a way of writing out what a function does. Lambda-calculus expressions are the basis for super-recursive languages like LISP. Intuitionistic logic is logic in which we don't assume that a or not a is true. The correspondence between the two is that every provable statement in intuionistic logic is one for which a proof can be represeneted as a lambda-calculus statement.
All right, we haven't got to the cool part yet. The question is the following: if we take intuiniostic logic and add the classical logic axiom (a or not a is true), what do we need to add to lambda-calulus to continue the correspondence between the two? The answer is crazy: goto statments. Like I mentioned above, lambda-calculus statements can be viewed as programs, and by adding goto statements to this programming language, we get the equivalent of classical logic. In other words, goto statements allow one to prove a or not a.
Later on, I'll hopefully post why this is true.
