It seems we have just one rule to eliminate variables: substitution. For example, given A=BC and BCD=E, we can eliminate BC by substituting A for BC in BCD=E. Thus, we must have equation !A=X to get to B!A=!A, and to get to !A=X we must have !A=Y, and so on.
So it seems impossible in given axiomatic system to derive B!A=!A from !B=AD. Am I missing something?
EDIT: Here I take axioms in 1.12 as a basis for proposition calculus and I don't use any interpretation of them.
Perhaps what is missing is these rules:
AT = A (1)
AF = F (2)
A + T = T (3)
A + F = A (4)
Which can be derived from the given axioms, apparently. I'm not sure if some necessary axioms were omitted.
Using some of these, here's one way to derive B!A=!A from !B=AD:
!B = AD
!B + A = AD + A
!B + A = AD + AT (1)
!B + A = A(D + T) (Distributivity)
!B + A = AT (3)
!B + A = A (1)
!!B!A = !A (Duality)
B!A = !A
Please reply to this comment if you intend to participate, and are willing and able to free up a few hours per week or fortnight to work through the suggested reading or exercises.
Please indicate where you live, if you would be willing to have some discussion IRL. My intent is to facilitate an online discussion here on LW but face-to-face would be a nice complement, in locations where enough participants live.
(You need not check in again here if you have already done so in the previous discussion thread, but you can do so if you want to add details such as your location.)
It should be an established standard to link to the previous posts on the same topic. This is necessary to actually build upon existing work, and not just create blogging buzz. In this case, the obvious reference is The Correct Contrarian Cluster, and also probably That Magical Click and Reason as memetic immune disorder.
This is an off-topic reply.
Voted down for being off-topic.
I'm not sure about this, but I think that if you can specify and check a Friendly AI that well, you can build it.
Verifying a proof is quite a bit simpler that coming up with the proof in the first place.
I've noticed this too. It is one of several annoying problems that would evaporate if votes weren't anonymous.
Perhaps keep anonymous votes too, but make them worth less or only use them to break ties.
FAI is harder.
No it's not. Look at two simpler cases:
Write a chess program that provably makes only legal moves, iterate as desired to improve it. Or,
Write a chess program. Put it in a sandbox so you only ever see it's moves. Maybe they're all legal, or maybe they're not because you're having it learn the rules with a big neural net or something. At the end of the round of games, the sandbox clears all the memory that held the chess program except for a list of moves in many games. You keep the source. Anything it learned is gone. Iterate as desired to improve it.
If you're confident you could work out how it was thinking from the source and move list, what if you only got a sequence of wins and non-wins? (An array of bits)
A sequence of wins and non-wins is enough to tell you whether a given approach can result in intelligent behaviour. That alone is enough to make it a useful experiment.
A man with one watch knows what time it is; a man with two watches is never quite sure.
A man with one watch might have the wrong time; a man with two watches is more aware of his own ignorance.
View more: Next
= f037147d6e6c911a85753b9abdedda8d){kind=logo}
= 27d567bc2d48d9f40e9ccc20ea370b15)
= b715d02e85f7b3b4ae65ca3d3e450868)
Subscribe to RSS Feed
EDIT: The original post now has updated times and links, so refer to that instead.
Here are links to the times suggested, for convenience:
I'd suggest posting meeting times using timeanddate.com, to help avoid confusion about time zones and daylight savings.