Hacker News new | past | comments | ask | show | jobs | submit | popnroll's comments login

I think Gates is right. What is the problem with the government controlling communication? There are clear advantages, like handling illegal things. What are the disadvantages, the nude photo of your ex-girlfriend being analyzed by a machine?


Are you serious? Here are some disadvantages:

If you got connections to government, you can steal trade secrets from companies and enrich yourself and destroy the competition.

Destroy the lives of your political opponents by blackmailing.

Analyse and control the public sentiment to crush minorities.

I recommend you read a bit of stasi: https://en.m.wikipedia.org/wiki/Stasi

Also Bill Gates wants full government control because he is practically within the circles of government, obviously he would benefit from such agreements, but same cannot be said for plebs.

Anyhow, even if people like Bill Gates might benefit from such undemocratic agreements, tide can always turn against them and this level of censorship and surveillance can be used against them even more effectively than that is currently used againsts plebeians.


All these points already exist today and for a long time.


I feel like you can just look at what China or N. Korea are doing to see the downsides.


I can't imagine living in a country with chief executives as diverse as Donald Trump, Barack Obama, FDR, and Ronald Reagan, and still being naïve enough to think there's no problem with the government controlling communication. You can't imagine an executive branch led by any of those people using that power inappropriately?


We don't want a government to be the arbiter of truth. Please read 1984 or consider the following:

Iraq clearly has weapons of mass destruction. Censor all communications claiming otherwise.

The American government is not performing mass surveillance on its citizens. James Clapper Confirmed this in a Congressional Hearing. Censor all communication claiming otherwise

South Korea's President is not being influenced by a cult leader. Censor all communication claiming otherwise

And countless other examples where government controlling communication would lead to censorship of topics that the general public MUST hear. One cannot make an informed decision without information.


If you assume the government to be lawful and of high morals, of course. On the other hand, if your country is run by literal Nazis, the idea doesn't sound so good anymore. I hope your ancestry is pure of whatever lineage the rulers of the next fascist empire will be.


But in that case you've already lost all freedom. What can be done in a fascist country by sending encrypted messages?


You can organize resistance on all levels. People who put their life on the line for others can coordinate inside the country and with forces outside of the country. This is a huge danger to the ruling group since it is only a small minority and many people get not only their freedoms taken away but also their riches. Therefore before establishing a fascist government you must first control communication to a high degree to be able to suppress opposition effectively.


Today you can follow the movements of anyone with technology. You're already screwed. The messages could not organize a resistance


Consider Russia (or the middle east) where it's still Not ok to be gay. Encryption helps you text your significant other without being thrown in jail or sent to a reeducation camp.


[flagged]


This tends to be a hot button issue for many, but just as a counter to your "ridiculous" claim, history tells us many things, including being able to intercept dangerous communication can stop VERY bad things happening to societies. You can't just look at one side. This isn't a black and white issue, it's about trying to find the right balance. I personally think we should favor personal privacy. I also think any attempts to try and control comms will be fleeting and will ultimately fail with the invention of even better decentralized privacy technology.


What about "none" instead of zero?


...doesn't help either.

The problem is that when you ask "How many blue cats are bouncing?" you are stating that blue cats are in existence. So there'd have to be some, not none. There'd have to be a number strictly greater than zero. So zero/none can't be the answer, or you're somehow breaking the rules of the game of logic, or how the computer game is set up.

If, however, you say "How many cats are blue and bouncing?" then the presupposition would only extend so far as to state that cats are in existence, which is reflected on-screen. In that case, it may well be the case that there are zero/no cats that are blue and bouncing.

Let me crossindex something I linked in the other thread:

https://en.wikipedia.org/wiki/Syllogism#Existential_import

When Aristotle describes his logic (All men are mortal...) he never fathoms the possibility that one of these sets that he talks about could be empty. (Empty sets, in that sense, don't belong in the realm of science, as far as he is concerned, but in the realm of fiction and so forth).

So, to get back to the original post: If I were doing this for a 2-4 year old, then zero is a can of worms I would try to avoid opening altogether. Or I would make sure that the presupposition-part of any question that is asked is in line with the evidence on screen.

If, instead of following Aristotle, you follow the embedding of the syllogism into modern predicate calculus and modern predicate calculus into propositional logic, then you end up with outcomes that will be mindbogglingly counter-intuitive to a 4 year old (but to any person, really).

Example: "All flying horses are three-legged." would become a true statement.

Since there are no flying horses, this is always an empty set. Ex falso quodlibet. Therefore always true. A valid statement.


I'd think that exercises for small children are based on more mainstream (nowadays) classical logic and ZFC (and likely with finite sets), and certainly are informal. If so, the reasoning can go as "here's a set of cats, take blue ones out of it, then take bouncing ones out of those; how many is there?".

I wondered whether what's shown on the screen is also supposed to be a complete representation of the set in question, but apparently the correct answer to every question is 0 and I don't see any cats (maybe it just doesn't work correctly here).


I might be corrupted by programming because it doesn't bother me when I hear a vacuously true claim like "All flying horses are three-legged". My mental model corresponds to Python's definition of "all":

    def all(xs, predicate):
        for x in xs:
            if not predicate(x):
                return False
        return True
Similarly,

    def any(xs, predicate):
        for x in xs:
            if predicate(x):
                return True
        return False
You say "Ex falso quodlibet" which makes it sound like you believe such a system leads to contradictions, but this would come down to the choice of rewrite rules.

Example: a rewrite rule from "NOT all(xs, predicate)" to "any(xs, NOT predicate)" would lead to contradictions. Reasoning:

    A. all({}, predicate) is true by def of all
    B. any({}, NOT predicate) is false by def of any
    C. NOT all({}, predicate} is false follows from A
    D. applying the rewrite rule to C, any({}, NOT predicate) is true, which contradicts B.
However, in first-order-logic, that same rewrite rule is fine since sets always contain elements. It doesn't seem like to much work to go from Python-esque any and all to ∀ and ∃. For example "all(xs, predicate)" could be rewritten to: "¬P ∨ (∀ xs. predicate)" where P is a new proposition variable for whether xs contains elements. This relies on the semantics including short-circuiting evaluation (which may be cheating, I don't know).

Or maybe the above is what you already meant when you said "following the embeding..."?


...that's what I mean when I say that computer scientists have been trained to think about certain aspects of logic in a way that doesn't come natural to people and leads to conclusions that almost anybody finds counterintuitive who isn't a computer scientist (like "All flying horses are three-legged").

...it comes down to how you represent natural language quantifiers in logic.

The semantics of "All men are mortal." is that "all" is the quantifier, which takes two higher-order arguments. Using x as the variable that is quantified over, the first argument would have to be a predicate of x and is called the restrictor. The second argument also has to be a predicate of x and is called the body. So "all" is the quantifier. "man" is the restrictor. "mortal" is the body.

Following that notation we would write "All men are mortal" as

    all_x { man(x) } { mortal(x) }
Now the question is how to represent this natural language quantifier in first-order logic. Most computer scientists would think

    ∀x { man(x) -> mortal(x) }
But this is NOT the way Aristotle thought about it, and not the way most human beings naturally think about it. The natural way to think about it is

    ∃x { man(x) } ∧ ∀x { man(x) -> mortal(x) }
The first part of the statement is what's called "existential import". (cf https://en.wikipedia.org/wiki/Syllogism#Existential_import)

When I say "ex falso quodlibet" I mean this: https://en.wikipedia.org/wiki/Principle_of_explosion

Moving over to the example about flying horses:

    all_x { fly(x) ∧ horse(x) } { three-legged(x) }
Without existential import the statement would mean.

    ∀x { ( fly(x) ∧ horse(x) ) -> three-legged(x) }
Now let's evaluate that within a logical theory that contains some common sense:

    ∀x horse(x) -> ¬fly(x)
The statement would then become provable. That's unnatural. No "normal" person who hasn't been taught through formal education to think in a particular way about implication would say "Oh yes, all flying horses are three-legged, that sounds perfectly reasonable."

Now WITH existential import, the statement would have to mean

    ∃x { fly(x) ∧ horse(x) } ∧ ∀x { ( fly(x) ∧ horse(x) ) -> three-legged(x) }
So now, using the same piece of common sense, the statement is no longer provable, but it's negation is (the statement is unsatisfiable). That's how a "normal" person thinks. A normal person would respond by saying "Hang on! There is no such thing as a flying horse! Therefore you are talking utter nonsense."

Going back to the original post: "How many blue cats are bouncing?" means

    howmany_x { blue(x) ∧ cat(x) } { bouncing(x) }
Which statement contradicts a state of the universe / game-screen, wherein there are no blue cats, if you interpret the statement by using existential import.

My suggestion was to rephrase as "How many cats are blue and bouncing?" which means

    howmany_x { cat(x) } { blue(x) ∧ bouncing(x) }
So now instead of "blue cat" being the restrictor and "bouncing" being the body, you would have "cat" as the restrictor and "blue and bouncing" as the body.

This would be better, because now you can use existential import the way "normal people" do, and still get to the desired result "zero" instead of the result "I can't answer that question". You avoid making a presupposition that contradicts the known state of the universe.


OP here, thanks for the thoughtful discussion :)

I'll think about this some more and see if some design decisions can improve the game with regards to "existential import". Thanks for introducing that concept by the way.

My feeling about this when developing the game with my daughter was that when playing a game, you are taking part in a game universe. If there were a reference to flying horses, the inference would instead be "there must be flying horses in this game". The generative gameplay which is creating cats with random attributes also suggests that blue, bouncing cats are likely to exist but just aren't pictured on the screen presently.

In early education (even undergraduate education) it's common to present a simplified model that in some cases contradicts other models, and developing the cognitive machinery to explore and understand the model one working within, its limits, and how it relates to other models may be more valuable than comparing which models better align with objective (or, academic) truth.

At least, this is the thought process I went through with some of the trade-offs about deciding what answer was most correct from the lens of various formalisms (in my limited exposure to those) versus what answer leads to the richest learning in the age-group.


Sonic the hedgehog is also blue.


What? I don't know what "chochopy" is, but this project is called Chocopy.


Choco-pie is a delicious Korean snack made with chocolate and marshmallows: http://www.trifood.com/chocopie.asp

You can find it at your local Korean market, and in Costco if you are in the SF Bay Area


There is a big difference between a 8 bit computer and a 8 bit FANTASY computer. But you don't get it, sorry!


First time I hear about this guy. Interesting.


If you haven't heard of John Carmack I highly recommend this book https://en.m.wikipedia.org/wiki/Masters_of_Doom


I'm really clueless about logic and mathematics theory, but isn't this the Gödel's incompleteness theorem?


The struggle is that the symbolic graphs we construct to explain facts become logical beasts of their own, prone to generating sentences paradoxical under our desired interpretation.

Of course, the proofs are first constructed in the context of meaning, but the entire process seems to be a struggle to context-switch between the realms of meaning and symbology, which do not necessarily mirror one another.

But Godel has somehow proved that symbols cannot always provide both a consistent and complete system of meaning.

Gödel seems very much related to this, but I'm still lost.


No, this is more about the philosophy of mathematics -- the question of "to which degree is mathematics 'real'?" Gödel did have an impact on this, with formalism no longer being a particularly viable viewpoint. But this is less of a strict mathematical question and more of a philosophical one.


No, the incompleteness theorem only examines how formal systems relate to themselves, not to reality. It shows that no significantly expressive system can be designed that won't allow paradoxical statements.


Unprovable statements. Not paradoxical statements. Paradoxes confound the reader, but can be explained as either being true or false due to rules that were implicitly used to construct the statement. Once all the steps are explicitly shown, with each rule that applies at each step, there is no more paradox.

On the other hand, unprovable statements never make it to the "but can be explained" stage: either the formal system is consistent, and these expressions by definition cannot have an answer, or they can be answered but the formal system is demonstrably inconsistent.

The formal system also needs to be a little more precise than "significantly expressive": it needs to allow for self-referential expressions. In effect, it must be possible to create an expression that can be mapped to the natural language sentence "This statement has no proof in this formal system".

While in natural language puzzles that might be a fun paradox to try to figure out, where the challenge is to determine whether, given the rules of the context, the answer is actually "true" or "false", when it comes to Godel sentences for formal systems there is never a paradox. Either they are undecidable, or the formal system is inconsistent. And we don't get an "out" by saying "but in reality, the answer is ..." because the whole point of formal systems is to be self-contained. There is nothing "outside" of them that we can use to make claims about expressions within that formal system. We only get the axioms of the formal system itself.


> It shows that no significantly expressive system can be designed that won't allow paradoxical statements.

The above is a complete misrepresentation of Gödel’s second incompleteness theorem.

The theorem holds for any sufficiently expressive system, where the term ‘sufficiently expressive’ has a precise formal meaning[1]. Moreover, it is not the case that any sufficiently expressive system must be inconsistent! The theorem could perhaps be paraphrased as ‘no sufficiently expressive consistent system can prove its own consistency’[2], as long as we are prepared to explain what ‘its own’ really means.

Importantly, there are systems that do not allow paradoxical statements, and are nevertheless quite expressive, in an informal sense. For example, any dependently typed[3] total functional programming language[4], such as Agda[5], Coq[6], Idris[7], or Lean[8].

All of these languages are designed to be consistent. Of course, implementation bugs do happen[9].

If you would like to learn more about dependent types, ‘The Little Typer’[10] is newly out and a lot of fun to read. For an accessible introduction to the concept of total functional programming, see Turner 2004[11].

[1] Hilbert-Bernays provability conditions, https://en.wikipedia.org/wiki/Hilbert–Bernays_provability_co...

[2] Gödel’s second incompleteness theorem, https://en.wikipedia.org/wiki/Gödel%27s_incompleteness_theor...

[3] Dependent type, https://en.wikipedia.org/wiki/Dependent_type

[4] Total functional programming, https://en.wikipedia.org/wiki/Total_functional_programming

[5] Agda programming language, http://agda.readthedocs.io

[6] Coq proof assistant, http://coq.inria.fr

[7] Idris programming language, http://www.idris-lang.org

[8] Lean theorem prover, http://leanprover.github.io

[9] The rise and fall of @proofmarket, https://twitter.com/i/moments/921153475836305408

[10] Friedman, D.P., Christiansen, D.T. (2018) ‘The Little Typer’, https://mitpress.mit.edu/books/little-typer

[11] Turner, D. (2004) ‘Total Functional Programming’, http://www.jucs.org/jucs_10_7/total_functional_programming


I like your paraphrase but I think it muddies the water. We really want to prove that axioms of a system cannot be contradicted if the system is inconsistent.

To be even more precise, the system or theory T proves that there is no number n which provides a proof of contradiction for the axioms of T.

So its the axioms of the systems which all formal systems assume and hold to be true. Basically its impossible to prove that axioms are true with the same system.

In short, no formal system can define its own consistency because in order for its axioms to be true, the system must be inconsistent.


I don't know if this adds anything to your comment; The input of a program is neither predetermined nor random.

If there is an input "out of our reality", then our reality would not be predetermined nor would it be random. (Which makes sense for the simulation hypothesis, which I enjoy having that conversation with my colleagues)


It's easy to say X part of a system is "neither predetermined nor random" within a system defined as open (like a computer program or even a machine with a dial that can be set by an operator).

When a system is closed, things become harder.

Chaitin's number represents (very roughly) the structure of any complete mathematical system and it can be shown to be random in the sense of Kolmogorov.


but that just means there is more logical (predetermined) action 'out of our reality' The input of a program is predetermined by the physics that drive input to reach the program. (or it is from nowhere and is truly random, though I doubt this is the case)


This is a good explanation. We are saying we give the function x and y, but we can't guarantee that z comes out EVEN if we control for everything we are aware of. Thank you.

Still, I don't understand any of this even vaguely past the platitudes.


Oh boy, I know this is arrogant; It's pretty easy to show evidence of determinism. 1) Read my brain, check if in ten seconds I will say yes or nothing. 2) Don't tell me. 3) Wait ten seconds. 4) Compare results. I'm aware of the experiments of reading brain decisions faster than our consiousness (machines telling which button we will play "before we realized"). No, no psychomotor tricks. Just read my brain, don't tell me until I made my choice. If you get 100% I believe you, meanwhile, no evidence.


>no evidence

Why do you assume that the null hypothesis is free will?


I'm not assuming free will exists. To be honest, I'm personally a compatibilist. I'm determinism and free will agnostic. No evidence for free will doesn't mean determinsm is true. No evidence for determinism doesn't mean free will is true. Is an unpopular opinion. But I see no gap in the logic.


getChar is a Haskell function without arguments.


In Haskell, getChar isn't a function (something of type a -> b), its type is IO Char

http://hackage.haskell.org/package/base-4.11.1.0/docs/Prelud...

It represents an interaction with the outside world that results in a Char when you perform it. It isn't a function because in Haskell functions must be pure (with no side effects).


This is false. getChar is a constant.


I am confused :S

From your other post: "In both Gluon and Haskell, functions without arguments can be represented as functions over the unit type: f: () -> SomeType"

Isn't `f` a constant here too?, how is this different than getChar? (I get I don't understand something here but not sure what)


`getChar` is not of type `() -> SomeType`, but directly of type `SomeType`.

(Though yes, `f` also is a constant... it's just a constant that happens to be a function, which `getChar` is not.)


I feel the responses to you were somewhat unhelpful. Would they also claim that something of type `MyFun Char` is not a function, where

    data MyFun a = MyFun (() -> Char)
Technically they'd be right.


Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: