6 ms·

Logic Theorist

128 points by molteanu 8y ago

rgovostes 8y ago
Here is more information on Logic Theorist's improved proof of a theorem in Principia Mathematica: https://books.google.com/books?id=iYHuBwAAQBAJ&pg=PA52&lpg=PA52&dq=principia+mathematica+2.85&source=bl&ots=zyu408jeG0&sig=dApPpxiPyFGM8wBkIv8wmjjGM8I&hl=en&sa=X&redir_esc=y#v=onepage&q=principia%20mathematica%202.85&f=false https://books.google.com/books?id=iYHuBwAAQBAJ&pg=PA52&lpg=P...
- jkabrg 8y ago
  For people who don't understand the dots and colons, OP's proposition can be expressed in modern notation as ((p V q) -> (p V r)) -> (p V (q -> r)) It's easy to justify this tautology by considering the case when (p) is true and (p) is false. By contrast, the proof in PM and by LT strike me as highly unintuitive. I guess it's an example of using Hilbert Deduction instead of Natural Deduction, where Natural Deduction is closer to how people normally prove things. For programmers, it's as if they programmed in Combinatory Logic [1] instead of Lambda Calculus[2]. [1] - https://en.wikipedia.org/wiki/SKI_combinator_calculus https://en.wikipedia.org/wiki/SKI_combinator_calculus [2] - https://en.wikipedia.org/wiki/Lambda_calculus https://en.wikipedia.org/wiki/Lambda_calculus
  - scscsc 8y ago
    Assuming p V !p (read: p or not p) as an axiom means that you are admitting excluded middle. This axiom is part of "classical propositional logic". So a proof using this case distinction (p true or p false) would be valid, in the classical sense. There is a stronger system, called "intuitionistic propositional logic", where this axiom is not valid. There are less formulae that are valid intuitionistically, but any formula that is valid intuitionistically is also valid clasically. There are various philosophical reasons why one prefers intuitionistic logic, but note that in any case it is stronger to have an intuitionistic proof, so these are preferable (when they exist).
    - Sniffnoy 8y ago
      The formula ((p V q) -> (p V r)) -> (p V (q -> r)) isn't valid intuitionistically, though (you can get excluded middle from it by taking q=p and r=⊥), so there's no reason to want an intuitionstic proof.
  - jkabrg 8y ago
    I'll add that the significance of the formula is it's similar to a*b + a*c = a*(b + c) which you ought to remember from school as "factoring/factorization". Except in this case, " * " is replaced with "V", and "+" is replaced with "->". In mathematics, you call that a "distributive law". Some more examples are a^c * b^c = (a*b)^c p/\q V p/\r = p/\(q V r) (pVq) /\ (pVr) = pV(q /\ r)
    - Twisol 8y ago
      While you're absolutely right that this is a kind of distributivity, conventionally + is related to "or", * to "and", and ^ to "implies". So the theorem as given would be rendered as something more like "(p + r)^(p + q) implies (p + r^q)".
      - pofilat 8y ago
        That's interesting.... + and * theorems correspond between logic and arithmetic, but taking ^ as implication generates theorems that are true in logic but not in arithmetic. (The truth table of implication is clearly different from binary exxponentiation)
        Twisol 8y ago
        Is it? I checked before commenting (because I also wanted to make sure the arithmetic analogy actually held): irb(main):001:0> 0**0 => 1 irb(main):002:0> 0**1 => 0 irb(main):003:0> 1**0 => 1 irb(main):004:0> 1**1 => 1 Notice that `p -> q` becomes `q^p`, i.e. the operands swap position.
  - drostie 8y ago
    Just to give the proof as a whole in this notation for others, assume (→) has lower precedence than (∨) and is right-associative (i.e. that a → b → c = a → (b → c)): Proving: (p ∨ q → p ∨ r) → p ∨ (q → r) Start from: (x → y) → (y → z) → x → z Replace x with q, y with p ∨ q, z with p ∨ r: (q → p ∨ q) → (p ∨ q → p ∨ r) → q → p ∨ r The first part (q → p ∨ q) is already a known tautology so via modus ponens (p ∨ q → p ∨ r) → q → p ∨ r Replace the last → with its definition, (a → b) = ¬a ∨ b: (p ∨ q → p ∨ r) → ¬q ∨ p ∨ r Use the commutative property of (∨): (p ∨ q → p ∨ r) → p ∨ ¬q ∨ r Then use the definition again: (p ∨ q → p ∨ r) → p ∨ (q → r) QED. The first part is also valid in intuitionistic logic and essentially just transforms a known truth `x → y` into "continuation passing style" `∀z. (y → z) → x → z` with a valid result, I think this is why the authors were quite pleased with the proof. The second half is the shifty bit for intuitionistic logic, going from `q -> Either p r` to `Either p (q -> r)` where it's really easy to see that you could not, say, have a Haskell function of that type generally.
  - pofilat 8y ago
    Does natural deduction scale beyond first-order propositional logic with a small number of variables? It seems to me that it would have bad exponential blowup, checking all the cases.
codezero 8y ago
Has any of the code for this survived?
- Immortalin 8y ago
  Some https://github.com/theoremprover-museum/logic-theorist https://github.com/theoremprover-museum/logic-theorist
- Cieplak 8y ago
  Not the original source but pretty explanatory: https://history-computer.com/Library/Logic%20Theorist%20memorandum.pdf https://history-computer.com/Library/Logic%20Theorist%20memo...
tokai2 8y ago
Here’s a simple analogy. Human: 1 + 1 + 1 + 1 = 4 Machine: 2 + 2 = 4 The machine ‘knows’ the result must be exactly 4. The machine is just finding new ways to arrive at a result that it already knows to be true. But i want the machine to arrive at a result that is hitherto unknown. That for me is AI.
- pimmen 8y ago
  We humans often run into new discoveries by basing it on stuff we already know. We knew that combustion engines could rotate an axle. We knew that axles could drive a wheel. We knew that wheels turning could drive a cart. Thus, the automobile. Just like humans, AIs can only solve problems it already understands.
  - smt88 8y ago
    > Just like humans, AIs can only solve problems it already understands This isn't actually true. Problems can be solved by random chance, as long as there are good ways to test the validity of solutions. The most obvious example of this is the evolution of living organisms. As long as AI can "understand" whether or not its solution solves a certain problem, it can just assemble random solutions and test them. There's obviously an incentive to decrease the randomness as much as possible, but an infinitely powerful computer wouldn't need any such optimization at all.
    - pimmen 8y ago
      I would however argue that if you can tell the difference between a good and a bad solution of the problem (through some utility function, or fitness function for evolutionary algorithms) you do have some understanding of the problem. But, yes, I agree that you could just arrive at the correct solution through random chance. I guess a better description is that to solve a problem we either need an understanding of the problem or enough resources and time to exhaust the solution space.
    - mockingbirdy 8y ago
      If you watch videos of AIs learning to run [1] or playing Mario [2], you see that there's definitely "try random shit until your reward function gives you positive feedback" as a method for training AIs. The difficult part is developing the reward function. There's a lot of intelligence in our hormone-based incentive system - that we feel pain, that we feel sad, etc. Many of those emotions are pre-programmed. If we find a way to design reinforcement systems with the right goals, we can do it like mother nature did it for several billion years. But it's still a ton of computational power required. If we look at nature as a massively parallelized computational system that defined "just live" as the reward (not because it "wants" it, but because it just emerged), it shows us how much power we would need if we would try to build a completely random process that gains intelligence. I think your proposed method works ("just assemble random solutions and test them") because we've already seen it in nature. But it takes a lot of time and energy, regardless of our computational power. I think we're faster when we find the right boundaries and reward functions instead of randomly trying stuff. [1]: https://youtu.be/gn4nRCC9TwQ https://youtu.be/gn4nRCC9TwQ [2]: https://youtu.be/qv6UVOQ0F44 https://youtu.be/qv6UVOQ0F44
andrepd 8y ago
I would like to see a few more details about how this actually worked.
goldenkey 8y ago
Isn't this like an enhanced SAT solver?
- jkabrg 8y ago
  No, not really. A SAT solver checks if there's a model in which a formula is true, while this program checks if the formula is true in every model. It's believed that there's no efficient reduction from one to the other, because otherwise NP=coNP.
  - vilhelm_s 8y ago
    However, modern sat-solvers do both. That is, although they are called "sat-solvers", they can actually output both "sat" and "unsat". In software verification they are used for the "unsat" side: you produce a logical formula P stating that your software is correct, and then you ask the sat-solver about ¬P. Hopefully it returns "unsat", meaning that it has proved P is true; otherwise it will return a satisfying assignment, which is a counterexample to your proposed theorem. So I guess you could say that a theorem prover for propositional logic, like Logic Theorist, is "half" of a modern solver like Z3, it can produce proofs but not counterexamples. :)
  - leeeeech 8y ago
    What does that look like? A SAT problem takes a bunch of unknown variables (v_1, v_2 ... V_n) and logic operators (''not, and, or'' for example would be enough) to form a formula that combines these operators and variables, to asks us for an assignment (traditionally ''true'' or ''false'') to each variable respectively, so that the formula is satisfied; For example given the rules of sudoku find a filled sudoku. Or for xx+nx+m=0, and a given n and m, find x. Then what is the model theoretic problem? Is it, if f(a,b)=((a and not b) or (b and not a)) is satisfied by e.g. (a=1,b=0), then we want to know all configs that satisfy it? The way I understand your post, you are saying we want to know if all combinations of a and b over {0, 1} satisfy the formula. I'm not sure that's not the same thing from a different perspective. I started a course on abstract algebra once, but actually I am still limited to boolean logic. while they mentioned Galois Theory, functions as points in a metric space, graph coloring problems and many things that sound interesting but quickly have me getting lost in details. It's the same effect as with other machine learning ... coff coff.
darkmighty 8y ago
Systems of logic should not be hard coded into AIs (or AGIs) imo. The basic problems with logic is that it doesn't take uncertainty into account, and doesn't support the fact that almost every statement about the real world is only approximately true, or a useful model; it also usually can't handle inconsistencies very well. It would be unable to prove or in fact have any useful facts about the real world. For example, consider the statement "The sky is blue.". It is not categorically true -- the sky becomes red near sunset, (depending on chrominance vs luminance interpretation) it gets black at night, may be other colors in other planets, etc. So the system would be stuck trying to convey all necessary conditions, might not be able to formulate simple thoughts or communicate well. It would almost certainly lack abstraction capabilities. There are some logical systems that make slight modifications to logic to accommodate probabilities and uncertainty, but those still might be insufficient or incomplete. The fundamental issue is that, while logic works and is useful for us, it is just a tool. The end goal of any real world agent is not logical correctness, it is achieving tasks, understanding/predicting its environment, communicating, etc. Because of the specificity of those environments and tasks, there isn't going to be a general method that is efficient in them. You need a evolutionary-like, or leaning system that can adapt to the problem with minimal underlying assumptions. The assumptions of logic that everything should be binned according to falsehoods, probabilities, etc, is ultimately not necessarily a good way to (for example) control a robot in a complex environment, make it assemble a product, play videogames, or even do mathematics. Perhaps they can be augmented with side models (again tools) allowing them to formulate subtasks as logical problems (although its not clear those approaches would be better than just training neural networks). Nothing can be set in stone, everything must be learned and modifiable. So again the main problem with AGI is formulating good frameworks that 1) Have good, general goals aligned with what we expect from this AI; 2) Is able to adapt in almost every way to achieve this goal, without degrading its ability to recognize its rewards/goals. This is such a hard problem that it occupies a significant chunk of even humans' lifetimes. We spend lots of time thinking about long term goals, which in part are dictated by society, in part dictated by biology, and which we reflect upon to conclude what we should do -- from small daily goals like eating or getting to work, to long term career advancing and relationships. Then we set to achieve those goals by learning and acting on the world around us. It does happen often that our goals degenerate, ultimately because of our ability to modify ourselves and set our own goals: the reward achieved from a drug is a degeneracy that overrides other long term goals; various addictions exploit loopholes in our reward system; we suffer from despair, depression or lack of motivation that can even override the basic biological rewards. If we could not override basic biological rewards, setting our own goals, then we would fall to addictions and inability to live in complex environments which require complex unnatural goals related to careers, learning, and other abstract concepts. And too much of this power can leave us in desperation, depression, meaninglessness. So there is a constant balance and search for genuine rewards, and constant refinement of them. That is central to human existence, and to conscious experience in general.

128 points by molteanu 8y ago

Here is more information on Logic Theorist's improved proof of a theorem in Principia Mathematica: https://books.google.com/books?id=iYHuBwAAQBAJ&pg=PA52&lpg=PA52&dq=principia+mathematica+2.85&source=bl&ots=zyu408jeG0&sig=dApPpxiPyFGM8wBkIv8wmjjGM8I&hl=en&sa=X&redir_esc=y#v=onepage&q=principia%20mathematica%202.85&f=false https://books.google.com/books?id=iYHuBwAAQBAJ&pg=PA52&lpg=P...

jkabrg 8y ago
For people who don't understand the dots and colons, OP's proposition can be expressed in modern notation as ((p V q) -> (p V r)) -> (p V (q -> r)) It's easy to justify this tautology by considering the case when (p) is true and (p) is false. By contrast, the proof in PM and by LT strike me as highly unintuitive. I guess it's an example of using Hilbert Deduction instead of Natural Deduction, where Natural Deduction is closer to how people normally prove things. For programmers, it's as if they programmed in Combinatory Logic [1] instead of Lambda Calculus[2]. [1] - https://en.wikipedia.org/wiki/SKI_combinator_calculus https://en.wikipedia.org/wiki/SKI_combinator_calculus [2] - https://en.wikipedia.org/wiki/Lambda_calculus https://en.wikipedia.org/wiki/Lambda_calculus
- scscsc 8y ago
  Assuming p V !p (read: p or not p) as an axiom means that you are admitting excluded middle. This axiom is part of "classical propositional logic". So a proof using this case distinction (p true or p false) would be valid, in the classical sense. There is a stronger system, called "intuitionistic propositional logic", where this axiom is not valid. There are less formulae that are valid intuitionistically, but any formula that is valid intuitionistically is also valid clasically. There are various philosophical reasons why one prefers intuitionistic logic, but note that in any case it is stronger to have an intuitionistic proof, so these are preferable (when they exist).
  - Sniffnoy 8y ago
    The formula ((p V q) -> (p V r)) -> (p V (q -> r)) isn't valid intuitionistically, though (you can get excluded middle from it by taking q=p and r=⊥), so there's no reason to want an intuitionstic proof.
- jkabrg 8y ago
  I'll add that the significance of the formula is it's similar to a*b + a*c = a*(b + c) which you ought to remember from school as "factoring/factorization". Except in this case, " * " is replaced with "V", and "+" is replaced with "->". In mathematics, you call that a "distributive law". Some more examples are a^c * b^c = (a*b)^c p/\q V p/\r = p/\(q V r) (pVq) /\ (pVr) = pV(q /\ r)
  - Twisol 8y ago
    While you're absolutely right that this is a kind of distributivity, conventionally + is related to "or", * to "and", and ^ to "implies". So the theorem as given would be rendered as something more like "(p + r)^(p + q) implies (p + r^q)".
    - pofilat 8y ago
      That's interesting.... + and * theorems correspond between logic and arithmetic, but taking ^ as implication generates theorems that are true in logic but not in arithmetic. (The truth table of implication is clearly different from binary exxponentiation)
      - Twisol 8y ago
        Is it? I checked before commenting (because I also wanted to make sure the arithmetic analogy actually held): irb(main):001:0> 0**0 => 1 irb(main):002:0> 0**1 => 0 irb(main):003:0> 1**0 => 1 irb(main):004:0> 1**1 => 1 Notice that `p -> q` becomes `q^p`, i.e. the operands swap position.
- drostie 8y ago
  Just to give the proof as a whole in this notation for others, assume (→) has lower precedence than (∨) and is right-associative (i.e. that a → b → c = a → (b → c)): Proving: (p ∨ q → p ∨ r) → p ∨ (q → r) Start from: (x → y) → (y → z) → x → z Replace x with q, y with p ∨ q, z with p ∨ r: (q → p ∨ q) → (p ∨ q → p ∨ r) → q → p ∨ r The first part (q → p ∨ q) is already a known tautology so via modus ponens (p ∨ q → p ∨ r) → q → p ∨ r Replace the last → with its definition, (a → b) = ¬a ∨ b: (p ∨ q → p ∨ r) → ¬q ∨ p ∨ r Use the commutative property of (∨): (p ∨ q → p ∨ r) → p ∨ ¬q ∨ r Then use the definition again: (p ∨ q → p ∨ r) → p ∨ (q → r) QED. The first part is also valid in intuitionistic logic and essentially just transforms a known truth `x → y` into "continuation passing style" `∀z. (y → z) → x → z` with a valid result, I think this is why the authors were quite pleased with the proof. The second half is the shifty bit for intuitionistic logic, going from `q -> Either p r` to `Either p (q -> r)` where it's really easy to see that you could not, say, have a Haskell function of that type generally.
- pofilat 8y ago
  Does natural deduction scale beyond first-order propositional logic with a small number of variables? It seems to me that it would have bad exponential blowup, checking all the cases.

codezero 8y ago

Has any of the code for this survived?

Immortalin 8y ago
Some https://github.com/theoremprover-museum/logic-theorist https://github.com/theoremprover-museum/logic-theorist
Cieplak 8y ago
Not the original source but pretty explanatory: https://history-computer.com/Library/Logic%20Theorist%20memorandum.pdf https://history-computer.com/Library/Logic%20Theorist%20memo...

tokai2 8y ago

Here’s a simple analogy. Human: 1 + 1 + 1 + 1 = 4 Machine: 2 + 2 = 4 The machine ‘knows’ the result must be exactly 4. The machine is just finding new ways to arrive at a result that it already knows to be true. But i want the machine to arrive at a result that is hitherto unknown. That for me is AI.

pimmen 8y ago
We humans often run into new discoveries by basing it on stuff we already know. We knew that combustion engines could rotate an axle. We knew that axles could drive a wheel. We knew that wheels turning could drive a cart. Thus, the automobile. Just like humans, AIs can only solve problems it already understands.
- smt88 8y ago
  > Just like humans, AIs can only solve problems it already understands This isn't actually true. Problems can be solved by random chance, as long as there are good ways to test the validity of solutions. The most obvious example of this is the evolution of living organisms. As long as AI can "understand" whether or not its solution solves a certain problem, it can just assemble random solutions and test them. There's obviously an incentive to decrease the randomness as much as possible, but an infinitely powerful computer wouldn't need any such optimization at all.
  - pimmen 8y ago
    I would however argue that if you can tell the difference between a good and a bad solution of the problem (through some utility function, or fitness function for evolutionary algorithms) you do have some understanding of the problem. But, yes, I agree that you could just arrive at the correct solution through random chance. I guess a better description is that to solve a problem we either need an understanding of the problem or enough resources and time to exhaust the solution space.
  - mockingbirdy 8y ago
    If you watch videos of AIs learning to run [1] or playing Mario [2], you see that there's definitely "try random shit until your reward function gives you positive feedback" as a method for training AIs. The difficult part is developing the reward function. There's a lot of intelligence in our hormone-based incentive system - that we feel pain, that we feel sad, etc. Many of those emotions are pre-programmed. If we find a way to design reinforcement systems with the right goals, we can do it like mother nature did it for several billion years. But it's still a ton of computational power required. If we look at nature as a massively parallelized computational system that defined "just live" as the reward (not because it "wants" it, but because it just emerged), it shows us how much power we would need if we would try to build a completely random process that gains intelligence. I think your proposed method works ("just assemble random solutions and test them") because we've already seen it in nature. But it takes a lot of time and energy, regardless of our computational power. I think we're faster when we find the right boundaries and reward functions instead of randomly trying stuff. [1]: https://youtu.be/gn4nRCC9TwQ https://youtu.be/gn4nRCC9TwQ [2]: https://youtu.be/qv6UVOQ0F44 https://youtu.be/qv6UVOQ0F44

andrepd 8y ago

I would like to see a few more details about how this actually worked.

goldenkey 8y ago

Isn't this like an enhanced SAT solver?

jkabrg 8y ago
No, not really. A SAT solver checks if there's a model in which a formula is true, while this program checks if the formula is true in every model. It's believed that there's no efficient reduction from one to the other, because otherwise NP=coNP.
- vilhelm_s 8y ago
  However, modern sat-solvers do both. That is, although they are called "sat-solvers", they can actually output both "sat" and "unsat". In software verification they are used for the "unsat" side: you produce a logical formula P stating that your software is correct, and then you ask the sat-solver about ¬P. Hopefully it returns "unsat", meaning that it has proved P is true; otherwise it will return a satisfying assignment, which is a counterexample to your proposed theorem. So I guess you could say that a theorem prover for propositional logic, like Logic Theorist, is "half" of a modern solver like Z3, it can produce proofs but not counterexamples. :)
- leeeeech 8y ago
  What does that look like? A SAT problem takes a bunch of unknown variables (v_1, v_2 ... V_n) and logic operators (''not, and, or'' for example would be enough) to form a formula that combines these operators and variables, to asks us for an assignment (traditionally ''true'' or ''false'') to each variable respectively, so that the formula is satisfied; For example given the rules of sudoku find a filled sudoku. Or for xx+nx+m=0, and a given n and m, find x. Then what is the model theoretic problem? Is it, if f(a,b)=((a and not b) or (b and not a)) is satisfied by e.g. (a=1,b=0), then we want to know all configs that satisfy it? The way I understand your post, you are saying we want to know if all combinations of a and b over {0, 1} satisfy the formula. I'm not sure that's not the same thing from a different perspective. I started a course on abstract algebra once, but actually I am still limited to boolean logic. while they mentioned Galois Theory, functions as points in a metric space, graph coloring problems and many things that sound interesting but quickly have me getting lost in details. It's the same effect as with other machine learning ... coff coff.

darkmighty 8y ago

Systems of logic should not be hard coded into AIs (or AGIs) imo. The basic problems with logic is that it doesn't take uncertainty into account, and doesn't support the fact that almost every statement about the real world is only approximately true, or a useful model; it also usually can't handle inconsistencies very well. It would be unable to prove or in fact have any useful facts about the real world. For example, consider the statement "The sky is blue.". It is not categorically true -- the sky becomes red near sunset, (depending on chrominance vs luminance interpretation) it gets black at night, may be other colors in other planets, etc. So the system would be stuck trying to convey all necessary conditions, might not be able to formulate simple thoughts or communicate well. It would almost certainly lack abstraction capabilities. There are some logical systems that make slight modifications to logic to accommodate probabilities and uncertainty, but those still might be insufficient or incomplete. The fundamental issue is that, while logic works and is useful for us, it is just a tool. The end goal of any real world agent is not logical correctness, it is achieving tasks, understanding/predicting its environment, communicating, etc. Because of the specificity of those environments and tasks, there isn't going to be a general method that is efficient in them. You need a evolutionary-like, or leaning system that can adapt to the problem with minimal underlying assumptions. The assumptions of logic that everything should be binned according to falsehoods, probabilities, etc, is ultimately not necessarily a good way to (for example) control a robot in a complex environment, make it assemble a product, play videogames, or even do mathematics. Perhaps they can be augmented with side models (again tools) allowing them to formulate subtasks as logical problems (although its not clear those approaches would be better than just training neural networks). Nothing can be set in stone, everything must be learned and modifiable. So again the main problem with AGI is formulating good frameworks that 1) Have good, general goals aligned with what we expect from this AI; 2) Is able to adapt in almost every way to achieve this goal, without degrading its ability to recognize its rewards/goals. This is such a hard problem that it occupies a significant chunk of even humans' lifetimes. We spend lots of time thinking about long term goals, which in part are dictated by society, in part dictated by biology, and which we reflect upon to conclude what we should do -- from small daily goals like eating or getting to work, to long term career advancing and relationships. Then we set to achieve those goals by learning and acting on the world around us. It does happen often that our goals degenerate, ultimately because of our ability to modify ourselves and set our own goals: the reward achieved from a drug is a degeneracy that overrides other long term goals; various addictions exploit loopholes in our reward system; we suffer from despair, depression or lack of motivation that can even override the basic biological rewards. If we could not override basic biological rewards, setting our own goals, then we would fall to addictions and inability to live in complex environments which require complex unnatural goals related to careers, learning, and other abstract concepts. And too much of this power can leave us in desperation, depression, meaninglessness. So there is a constant balance and search for genuine rewards, and constant refinement of them. That is central to human existence, and to conscious experience in general.