Viewing profile — p0llard

> Gödel's statements are true in all models This is wrong, and I said the exact opposite of this: there are non-standard models of PA in which G_F is false. There is a fundamental …

> Question: Can a sentence be provably true in one arithmetic system but not another? The answer is yes! ZFC |- AC but ZF |/- AC and both ZFC and ZF can encode arithmetic. But ther…

> I feel like you may be arguing semantics Yeah, I am; it really depends on how you define "true". I prefer this to be interpreted as "true in all models" so sentences are "true" w…

> There are true statements that are unprovable within the system. I really don't like this, and it verges on being flat-out incorrect: the first incompleteness theorem does not sa…

> Godel-type unprovability is separate from logical independence What do you mean by this? The Goedel sentence of a system is logically independent from the system by the standard …

> true but unprovable under the axioms xyz? Careful: we don't really talk about things which are "true but unprovable" in first-order logics. By Goedel's completeness theorem, if a…

> And, you realize that the US has 300m people, correct? You will have to compare per-capita stats, not total numbers. The UK has a population of almost 70MM. The factor of ~5 need…

> According to a judge or a police officer, probably not I'd naively hope that a judge wouldn't side with a police officer here, but I think the fact that resisting arrest is inher…

I live in a country where we don't inject people with ketamine on the street, nor do "criminals run amok". We also don't have armed gangs imposing "their own idea of a justice syst…

> Want to work with an IP vendor whose sales are not part time lawyers? Go for ARM Interested in this comment: were MIPS/Imagination known for being particularly litigious around l…

> Why would you guess? Because I'm basing it on my experience doing research in PLT, but this is of course purely anecdotal and my areas of research interest lie away from the like…

Yes it is, but if "leading functional language" means "on the cutting edge of research into functional languages" then that might well be used to describe Haskell. If leading refer…

Yeah I think you're definitely right, and Algorithm W is how HM was introduced to me when I studied it. kevincox's comment sums up my misunderstanding.

In general they seem to do a good job of missing out books which cover the mathematical basis of theoretical computer science; if the aim is to provide a starting point for humanit…

Probably depends on the definition of leading; I'd guess that Haskell is probably used more than any other (Turing-complete, to exclude Gallina, etc.) functional language within pr…

> There exist many type inference algorithms, the best known one is the so-called Algorithm W. Is this correct? I dug out Milner's paper [1] where he states that Algorithm J is mor…

When I said "incompatible at the physical level" I meant it in the OSI sense of an issue at physical protocol level. An electrical specification mismatch could easily cause hardwar…

> tinker with advanced stuff requiring PCI-E chipsets What sort of things are you talking about here, out of interest? The only way you're going to wreck hardware is if you're atta…

> He's working on the same ledger tech but centralised Cryptographic ledger technology has been around since forever (the 70s to be precise): just look at Git, SUNDR, etc. I believ…

They aren't really targeting similar markets (at least from my perspective): pretty much any multinational firm can benefit from better corporate treasury management; cryptocurrenc…

Using cryptographic primitives to implement a non-productive asset is one thing; using cryptographic primitives as some kind of ledger goes back to the 70s, heck even Git uses Merk…

What are you getting at? There's a pretty big difference between corporate treasury software and cryptocurrency scams? Unless you're trying to argue that anything related to financ…

> The former, as a general rule, does not create a derivative work. It's specifically called out in the GPL FAQ as something that does not create a derivative work. Could you point…

> PostGIS via TCP From a legal perspective I'm unaware of any ruling which establishes a difference between components communicating via TCP and components communicating through fu…