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].
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.
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).
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.
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)
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)".
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)
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.
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.
Not this one, but later theorem provers have proved plenty of new results, although probably not many of them are very interesting. Here is a two decade old list [1]. One of the more interesting results is Robbins Conjecture, which was proved by a prover called EQP.
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.
Another way to phrase this is that, in the realm of theorem proving, a human is only going to 'validate' a response from an AI so long as there exists some mathematical or proof theoretic foundation to validate the response from an AI.
To do otherwise is insanity, unless the AI can somehow provably demonstrate that they have invented a better system than all existing mathematics, computation, and logic.
AI has plenty of room to grow in the realm of arts and creativity, because those are places where having a base foundation does not need to be so mechanically reinforced. Toppling all existing knowledge in the arts is fine to do, being that disruptive in the arts is perfectly acceptable and often welcome.
When it comes to the safety of code - expectations of what a machine is going to do, for really important stuff, you want to have a solid, clear, strong reasoning system that is easily understood and easily conveyed to those looking to embrace it. Lots of math and abstraction exists either in the mind of humans, or on a computer, but to take one's hand and smack the whole house of cards down simply because it can't be proven to be absolute perfection - that's a ridiculous thing to do. We know what computers can do because we decide what computers can do. We need to retain some 'ground' in reasoning because what would happen if we collectively stepped away from it all for too long?
> 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.
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.
> 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.
With that definition I can't see how artificial life created would be any much different than the behavior of a computer virus.
> I think we're faster when we find the right boundaries and reward functions instead of randomly trying stuff.
Boundaries and reward functions in human society are part of the 'human social organism' that allows each individual human to function with autonomy in a fashion that is collaborative, aligned with our developed value systems, and allows us to live with stability, security, faith (be it in some sense of wonder, divinity, in each-other - doesn't matter), independence - and these things are base needs, no matter what variation they manifest with. Boundaries are redefined when there is conflict, and the less violent and destructive the conflict, the better the chances are for these boundaries and reward functions to continue functioning as they have been developed (rather than being obliterated in entirety, requiring them to built from scratch).
It makes us faster, but it's also us standing on the shoulders of giants. And I think it's important to question what things are worth applying random solutions to, and what things require deep contemplation. It seems very paradoxical, to try to define something that both is a function of the system it exists in, and also something that could potentially break the whole system. But, creation, destruction, clearly an oversimplification.
I do know that what looks random to one person is not necessarily random to another. This goes back to how the context is defined, how society is defined, boundaries and reward functions established a priori.
Emotions can be simple. The problem is that a computer already has them. Computer produces wrong solution, algorithm dies. Computer produces right solution, algorithm survives. We don't give the computer words to express itself about this because we never taught it to do that. What would happen if we did?
> try to define something that both is a function of the system it exists in, and also something that could potentially break the whole system
That is what's so damn hard about shaping societies (and the market). The recursive feedback loop and the self-interference.
It's also on individual levels: We're able to dynamically adapt our reinforcement system using meta-cognition (based in the prefrontal neocortex).
I understand the other parts of the answer, but I can't really see what you try to say with them (e.g. boundaries, society and deciding if we apply randomness or not).
I tend to be of the mindset that over the long term, you are going to get a good perspective if you approach the problem 50/50. Apply randomness half the time, apply the knowledge you know the other half. Divide and conquer, sort of.
Randomness potentiates the space that you will both be able to identify error and consequently, find mistakes, find errors in reasoning (Monte Carlo simulations are traditionally used for this sort of thing). The other good thing with randomness as well, find ways to see errors as being 'not errors', e.g. a tool that can be developed, structured, a new way to see the problem, a creative approach. Some melding between the two seems to be something of significance for an AI. So you don't want it to be all random, because you need stability, structure, you need a 'language' or an 'awareness' you understand that isn't so chaotic and constantly changing that you can't even find a place to put your feet on the ground.
It doesn't have to be a perfect 50/50 balance, because that has it's own set of problems - divide and conquer all the divisions and you still wind up with 2^n newly defined problem spaces to interpret, possibly losing sight of the bigger picture or maintaining independent direction in one focused lineage of all those spaces. Just very generally, maintain balance, because the world is chaos sometimes.
It's like a stream of information. All the analysis to all of that space is meaningless if the context changes enough. So, adapt to a new context.
Honestly though, I don't know what I'm trying to say much of the time, aside, 'help', lol. Life is terrifying. :)
> Honestly though, I don't know what I'm trying to say much of the time, aside, 'help', lol. Life is terrifying. :)
from another comment made by you:
> Evolution does not care if an asteroid hits the earth and wipes out all life as it presently exists.
My advice: Stop worrying. Enjoy the randomness :)
Maybe book a flight to Asia. Life is short. Embrace uncertainty. Sell luxurious sanitary pads to rich women in their 40s. Dress well and be funny. Then suddenly change your mood to sexy, ask a stranger for a kiss. I now write random love letters to my ex-girlfriends. Let's see where randomness will lead us to. See you on the other side of existence.
Found the boundaries pretty early. Wearing nothing but socks and singing "Why does it hurt when I pee?" while trying to cross a freeway is not considered "appropriate in the public". shmocks everywhere.
Evolution does not care if an asteroid hits the earth and wipes out all life as it presently exists. It doesn't care of the moral, ethical, or philosophical dilemmas when it decides how to recycle one living organism into another. It doesn't have the foresight to know how one solution may affect everything versus another. It just picks whatever seems to work based on the context given. If the context is described incorrectly, it doesn't care if the unthinkable happens and the whole system collapses. That just turns into the present understanding of the system, but it won't matter if there's no one left to listen.
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.
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.
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. :)
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.
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.
https://books.google.com/books?id=iYHuBwAAQBAJ&pg=PA52&lpg=P...